More personal type confusion in tutorial

Stream: new members

[Garrison Venn]

In section 6.2 in Functional Programming in Lean the following statement is made:

monadLift (x >>= f : m α) is the same as (monadLift x : m α) >>= fun y => monadLift (f y)

should this not be:

monadLift (x >>= f : m α) is the same as (monadLift x : n β) >>= fun y => monadLift (f y)?

My underlying thought would be that:

x : m β
f : β → m α
monadLift : m β → n β

I ask these questions because if this is just a typo that is fine. However since I'm still struggling to learn Lean, I can't tell when I see these kind of expressions if I am misunderstanding the type concepts. So I start asking an LLM, getting it to agree after a while, and end up still not knowing--since getting it to agree means nothing. :rolling_on_the_floor_laughing:

[Damiano Testa]

Honestly, I do not understand much of this, but I know that this typechecks:

variable {β α} {m n} [Monad m] [Monad n] [MonadLift m n] {x : m β} (f : β → m α)
example : monadLift (x >>= f) = (monadLift x : n β) >>= fun y => monadLift (f y) := sorry

I don't even know if this is one of the two alternatives that you ask about, though...

[Garrison Venn]

Ok cool you verified at least that my interpretation is correct, and that the text may be incorrect :slight_smile: . More importantly you gave me a way to use Lean to type check, though I don't know what variable is yet. So thanks :+1: :+1:

I seem to be finding typos in the tutorial (I think), and wonder if there is some link where I can submit them where incorrect noise will be ignored. Just writing this here in case someone else sees this.

[Damiano Testa]

Ah, variable ... means that what appears in ... will be added as an assumption, as needed in the following declarations.

[Damiano Testa]

There are some subtleties for what counts as "as needed", but essentially you can simply copy paste those variables as assumptions of the two examples and remove variable, if you prefer.

[Damiano Testa]

I'll ping @David Thrane Christiansen, in case he is interested in this thread.

[Garrison Venn]

Actually I was thinking more about:

monadLift (x >>= f : m α) is the same as (monadLift x : m α) >>= fun y => monadLift (f y)

One way to interpret this--ignoring possible transitive logical errors which I don't currently see, is that the statement could be correct if α = β, and m = n (using the previous notations). In this case the above contract is quite constrained in addition to the lift not really being a lift. I don't have enough Lean proof understanding to refute this given that the contract adherence seems voluntary. Regardless my point is that in a pedagogical setting the above statement could be misleading; is it a typo or is the monadLift distributive law highly constrained.

[Aaron Liu]

90% sure this is a typo

[Kevin Buzzard]

#backticks btw @Garrison Venn

[David Thrane Christiansen]

Thanks for the ping! I was away from the computer due to holidays.

Here's a bit more context:

monadLift should distribute over bind so that monadLift (x >>= f : m α) is the same as (monadLift x : m α) >>= fun y => monadLift (f y).

I think there is an issue of parenthesization, and it should be:

monadLift should distribute over bind so that monadLift (x >>= f : m α) is the same as monadLift (x : m α) >>= fun y => monadLift (f y).

With more type annotations, this could be:

monadLift should distribute over bind so that (monadLift (x >>= f : m α) : n α) is the same as (monadLift (x : m α) : n α) >>= fun (y : α) => (monadLift (f y : m β) : n β).

but in the context of the text that's describing monad transformers it should really be

monadLift should distribute over bind so that (monadLift (x >>= f : m α) : T m α) is the same as (monadLift (x : m α) : T m α) >>= fun (y : α) => (monadLift (f y : m β) : T m β).

I think it's otherwise correct as written. Does this make sense? Would the more-annotated version have been more helpful for you?

[Aaron Liu]

it's not correct without the additional parentheses

[Garrison Venn]

Thanks for the clarifications @David Thrane Christiansen . The added parentheses definitely helps on the rhs, but on the lhs I'm still seeing some confusion on my part.

Take: monadLift (x >>= f : m α)

Adding parentheses for more clarity this would be:

monadLift ((x >>= f) : m α)

This means the bind returns m α. In turn this means that we must add another type, call it β and f must be typed as:

f : β → m α

Therefore the typed version of x is forced by the bind requirements to be:

x : m β

The rhs has:

monadLift (x : m α) >>= fun y => monadLift (f y)

Therefore I would get:

m α = m β

Sorry for any misinterpretation, the automatic Lean coercions still throw me off. Still learning. :slight_smile:

[Aaron Liu]

oh yeah that's also a thing

[David Thrane Christiansen]

You're totally right, I made a mistake there. Coercions aren't intended to be used there, and I totally get why you'd jump to them. The only one who says sorry when intro docs are wrong is the author of them, not the reader - thank you!

It should be:

monadLift should distribute over bind so that (monadLift (x >>= f : m β) : T m β) is the same as (monadLift (x : m α) : T m α) >>= fun (y : α) => (monadLift (f y : m β) : T m β).

I'll fix it soon!

[David Thrane Christiansen]

https://github.com/leanprover/fp-lean/issues/251

[Garrison Venn]

@David Thrane Christiansen Well at least it seems you taught me correctly. :slight_smile:

[David Thrane Christiansen]

I'd sure rather it be without that stress, though. Thanks for the good question and feedback!