Type unification, structs and implicits

Stream: lean4

[cognivore]

Dear all, I'm writing a generic stream library to power a generic megaparsec clone.

My path of dropping the openness ambition took me from multiparameter typeclasses with associated types and associated instances all the way down to having a really closed system where I just offer one stream iterator type per taxonomy of streams and stream-like things, which is highly polymorphic. I don't want to sacrifice polymorphism for a number of reasons, not least of which is that I want to have the same user code to be able to be launched against real world and against some testing monads. So yes, I want my stuff to be polymorphic, but I'm okay for my stuff to be closed, i.e. non-extendable by the user.

However, even my least ambitious attempt failed the moment I've started introducing constraints. Here is a clean, representative example of what I mean: https://github.com/yatima-inc/straume/blob/cognivore/generic-programming-in-lean-is-pain/Straume/WonkyConstraint.lean#L24

[cognivore]

Ideally, I would like to be able to just say def flipTakeN := fun n x => takeN x n and def take1 := flipTakeN 1 or def take1 := fun x => takeN x 1.

Note that takeN implementation is replaced by a dummy implementation, just to be sure that there is an implementation for that type.

[Arthur Paulino]

Note: the link above takes you to a self-contained code, ready to be copied and pasted to a clean Lean file

[cognivore]

I made it even shorter!

[Sebastian Ullrich]

You say that you don't want to sacrifice polymorphism, but do you definitely need universe polymorphism as well? It's always easier to assume everything is in Type if that works for all your use cases.

[cognivore]

That's a tough one! While working on Megaparsec, I sacrificed universe polymorphism, and then there was a higher universe object that I couldn't work into the system without bringing it back. Sadly I don't remember particular details, but I think it was some associated type port.

[cognivore]

I was considering sacrificing it yesterday, when I hit this block, but after that experience, I'm kind of scared :)

[cognivore]

Thanks for encouraging to explore it, I'll try and see if it helps.

[Sebastian Ullrich]

The current bind constrains you to a single universe anyway, though see also the concurrent thread https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/universe.20polymorphic.20IO

[cognivore]

Thank you!

[Arthur Paulino]

@Sebastian Ullrich thanks for "un #xy ing" the question, kinda! However I think the original question still holds: why doesn't @cognivore's example typecheck?

[Arthur Paulino]

Sorry I was thanking you for your answers but I didn't mean to ask that question directly to you. Anyone's insights are welcome :pray: