Universe polymorphism, type classes and normal forms.

Stream: lean4

[Joe Hendrix]

Has there been any tooling built so far to lift generic lemmas over classes such as Functor and Monad to more specific instances?

I'm wondering particular in the case (such as List and Option) where the more specific type method has more universe polymorpism than the class method. e.g., List.bind and Option.bind allows the universes of α and β to vary while Bind.bind does not.

This is related the standard library in that it'd be great to write some lemmas at the class level and still have them automatically used on code that uses the class specific version of operator.

[Eric Wieser]

There are various threads about redesigning functor to be universe polymorphic

[Eric Wieser]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Changing.20the.20functor.20typeclasses had a lean 3 prototype, https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/universe.20polymorphic.20IO has extended discussion

[Joe Hendrix]

Thanks. I've read the universe polymorphic IO discussion. I should have cited that. It looks like that effort stalled out. After a little bit of experimentation on my own, I felt HMonad is going to be difficult.

Possible approaches to this I can think of:

1. Generalize typeclasses like Functor, Monad to support more polymorphism.
2. Restrict the universe polymorphism of class instance specific definitions.
3. Build some sort of lift capability to lift theorems from the class to the type-specific instances.
4. Generalize key tactics like simp to understand these operations are the same. This might be solvable with rewriting modulo congruence closure, but the universe polymorpism makes me uncertain.

I was thinking about doing some analysis to see how many problems option (2) created, but wanted to see if there's other options I should try first.

[Eric Wieser]

I think there's a compromise for 1 where we write polymorphic typeclasses for the notations, but not the lemmas

[Eric Wieser]

Which at least means we only have one way to spell things

[Joe Hendrix]

One downside is tht it's not just lemmas, but also default methods. Monad doesn't have lemmas, but I found it tricky to generalize just because of the implementation of seq in terms of bind.

I suspect option 2 is the most practical since one could hopefully lift the operation to the max universe, but it doesn't feel very elegant.

[Eric Wieser]

What do you mean by "class-specific"?

[Eric Wieser]

Are you using class to mean something different to class?

[Joe Hendrix]

@Eric Wieser Sorry, yes that was confusing - I meant the opposite. :) I meant not having multiple universe variables in instance specific methods such as Option.bind.

[Eric Wieser]

I think that would be pretty annoying for mathlib, as it would break all sorts of things downstream