Porting monads

Stream: mathlib4

[Arien Malec]

Since Lean4 prefers return to pure, how should we handle in porting?

[Arien Malec]

(Or maybe I don't understand the reference "we prefer return to pure).

[Arien Malec]

Is this in the context of a do?

[Adam Topaz]

It seems that return just works even without do. I don't know whether the "preference" in the reference refers only to do blocks.

def foo : IO Nat := return 0
def bar : IO Nat := pure 0
example : foo = bar := rfl

[Arien Malec]

The actual Monad definition still spells pure as pure....

[Adam Topaz]

Where is the return vs. pure convention mentioned?

[David Renshaw]

https://leanprover.github.io/lean4/doc/lean3changes.html#style-changes

[David Renshaw]

pure and return are not always interchangeable.

[David Renshaw]

I think the manual is just saying that if you can do either return or pure, then you should do return.

[David Renshaw]

Here's an example of return jumping out of an inner do block: https://github.com/leanprover-community/mathlib4/blob/56284fa8920a42b4cadf77a94aa7ab167bebbb4f/Mathlib/Tactic/SplitIfs.lean#L55

[Arien Malec]

I’ll create a PR for the manual to clarify.

[David Renshaw]

I believe that kind of jumping-out-of-a-do-block is not possible in Haskell.

[Scott Morrison]

Jumping out of a do block is pretty fun. :-)

[Mario Carneiro]

I don't agree with that convention to prefer return over pure (that's only in the lean 4 core repo I think). Certainly when translating from lean 3 monad code you should always use pure

[Mario Carneiro]

return can cause issues when you do something like

let x <- match foo with
| .a => return 0
| .b z => bar z
return (<- bar x)

if you meant the first return to be a pure then you've accidentally skipped the rest of the do block

[Mario Carneiro]

obviously this is sometimes useful if that's what you wanted to do, but it makes it more important to use return deliberately and call it out when doing so (it is nicely highlighted as a keyword, so it calls attention to itself more than pure), so using return at the end of a do block weakens the signal here

[Mario Carneiro]

one exception to this in my personal style is when using return to start a do block, since return x outside a do block means the same as do pure x (and in particular you can use <- foo inside x, so it is a concise way to write <$> expressions without the sigils).

[David Renshaw]

I don't agree with that convention to prefer return over pure

I think I'm with you on this.

[David Renshaw]

At least, the Rust programmer in me wants to avoid using return unless it is strictly needed.

[Jannis Limperg]

Mario Carneiro said:

obviously this is sometimes useful if that's what you wanted to do, but it makes it more important to use return deliberately and call it out when doing so (it is nicely highlighted as a keyword, so it calls attention to itself more than pure), so using return at the end of a do block weakens the signal here

I was also concerned about this, but adopted the Lean 4 convention anyway and it hasn't bitten me so far. The few times where I mistakenly wrote return instead of pure, Lean saved me with an "unreachable do element" error. Then again, the only benefit of using return everywhere is that it saves you a $ or <|.

[Mario Carneiro]

note in the example I gave, you won't get that error because it's in a match and the other branches are not early returning

[Mario Carneiro]

you still might get a type error if the do block has a different return type than the type of x, but it's fundamentally not something lean can catch since it's a valid thing to want to do

[Jannis Limperg]

Yes, of course. I'm just saying it hasn't been an issue empirically (but also no big benefit).