Alternative and do-notation

Stream: lean4

[Wrenna Robson]

Let's say I'm working in a monad with an Alternative instance. How do I use this with do-notation - intuitively it feels like I need some clear way of notating a branch or a case split which I would assume is done via match or match-style notation, but I'm not sure if there's a better way.

[Aaron Liu]

Just use <|> I would think

[Wrenna Robson]

Yeah I guess what I'm asking is that I am not sure I quite understand how to use <|> in a neat way.

[Wrenna Robson]

Like you then need to write two program flows effectively.

[Aaron Liu]

  let foo := do ...
  let onFailure := do ...
  foo <|> onFailure

[Wrenna Robson]

Aha!

[Wrenna Robson]

Thanks.

[Kyle Miller]

Sometimes I feel like there should be a neater notation for this than infix, since formatting can get awkward if you want to write it inline as (do ...) <|> (do ...).

Examples in core:

• https://github.com/leanprover/lean4/blob/232a0495b0b11e6817adfed89b1e913bbbc34157/src/Lean/PrettyPrinter/Delaborator/Builtins.lean#L461-L464
• https://github.com/leanprover/lean4/blob/232a0495b0b11e6817adfed89b1e913bbbc34157/src/Lean/Structure.lean#L349-L355

For example, perhaps this could be notation:

do
  stmt1
  stmt2
  first
  | stmt1a
    stmt2a
    stmt3a
  | stmt1b
    stmt2b

I doubt it comes up enough for the added complexity to be worth it, but it doesn't hurt thinking about it.

[Wrenna Robson]

Something like that was what I was thinking about yes

[Kyle Miller]

Maybe it wouldn't hurt to have an RFC, if someone is interested in writing it.

I'd expect to see:

• some realistic examples where using <|> is awkward and first would read clearer
• a mention that first is already a tactic with an analogous meaning so the parallelism strengthens Lean's design
• a justification for why it is ok to reserve first as a keyword (note that tactics do not reserve keywords), which would involve looking for any uses of first in declarations in core, batteries, mathlib, and other downstream libraries, and evaluating the impact

No guarantees this proposal would go anywhere, but a strong RFC would give it the best chance.

[Eric Wieser]

Another spelling choice is

run_meta do
  List.firstM id <| [
    do
      failure,
    do
      pure 1]

[Eric Wieser]

Which is a little less annoying to line-wrap than (do ...) <|> (do ...)

[Eric Wieser]

I guess the key distinction is that the proposed first would allow modifying mut lets, break, continue, and return

[Kyle Miller]

Yeah, that's a good point, and it would need to be evaluated in the RFC. The mut and control flow integration would be an important feature here.

(If there's a plan to make it possible to run combinators in a way that links them into the current do then there might be no need for first, also worth mentioning.)

[Notification Bot]

13 messages were moved from this topic to #lean4 > Applicative and do-notation by Eric Wieser.

[Notification Bot]

5 messages were moved from this topic to #general > Showing branching side-by-side by Eric Wieser.