SeqLeft and SeqRight

Stream: lean4

[Chris Lovett]

Lean's Applicative adds 2 new operators that Haskell doesn't seem to have, namely, SeqLeft and SeqRight. Has anyone written a nice tutorial on what these are exactly? I see them used heavily in Parsec, but when I try and show trivial examples, it is hard to convey the usefulness:

#eval [2,2,2] *> [4, 6] -- [4, 6, 4, 6, 4, 6]
#eval [4, 6] <* [2,2,2] -- [4, 4, 4, 6, 6, 6]

Does anyone have any better trivial examples of the usefulness of *> and *< ?

[Mario Carneiro]

It's a version of the "discard" operation. Rather than keeping both results, only the one pointed to is kept, but both are run in the order specified. a *> b is just do let _ <- a; b and a <* b is do let x <- a; let _ <- b; return x

[Mario Carneiro]

it's very useful for parsers since you can do things like (·,·) <$> tk "(" *> parseExpr <*> tk "," *> parseExpr <* tk ")" for parsing a pair

[Mario Carneiro]

or just tk "(" *> parseExpr <* tk ")" for a parenthesized expression

[Mauricio Collares]

Haskell does have them, by the way: https://hackage.haskell.org/package/base-4.17.0.0/docs/Control-Applicative.html#v:-42--62-

[Chris Lovett]

Ah, thanks, should that definition of a *> b be do let _ <- a; let x <- b; return x ? I'm worried that "<-" was missing on b in your version or was that deliberate?

[Chris Lovett]

I added something along the lines that you suggested here:
https://github.com/leanprover/lean4/blob/8d20458d79231a04d5086e47a8aaa63a6c1495db/doc/monads/applicatives.md

[Mario Carneiro]

That's the same thing, but you can write it that way if it helps to emphasize the symmetry

[Chris Lovett]

I've added now part 3, monads.md with an open question of how to explain the Lean Monad Identity law, if we have one that is easy to explain...

[Mario Carneiro]

The left identity rule is bind_pure, and the right identity is pure_bind

[Mario Carneiro]

(note that haskell's return is lean's pure)

[Mario Carneiro]

also note that https://mmhaskell.com/monads/tutorial has a typo, the left identity law should say m >>= return = m

[Chris Lovett]

You rock! I was indeed wondering why the left identity rule in the Haskell book didn't have an equality :-)