Zulip Chat Archive

Stream: lean4

Topic: Type unification, structs and implicits


cognivore (Jul 14 2022 at 13:05):

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 (Jul 14 2022 at 13:07):

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 (Jul 14 2022 at 13:13):

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

cognivore (Jul 14 2022 at 13:17):

I made it even shorter!

Sebastian Ullrich (Jul 14 2022 at 13:18):

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 (Jul 14 2022 at 13:19):

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 (Jul 14 2022 at 13:20):

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

cognivore (Jul 14 2022 at 13:20):

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

Sebastian Ullrich (Jul 14 2022 at 13:25):

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 (Jul 14 2022 at 13:27):

Thank you!

Arthur Paulino (Jul 14 2022 at 13:30):

@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 (Jul 14 2022 at 13:37):

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:


Last updated: Dec 20 2023 at 11:08 UTC