or-else in monadic assignment

Stream: new members

[Eric Wieser]

If I write

example : tactic (option nat) :=
do
  t ← foo <|> return none,
  bar,
  return (some 1)

this means "set t to foo, or set it to none if foo fails, then run bar then baz". I can understand why it means this, but it's not the behavior I'm looking for.

How do I write "set t to foo. If this fails, then exit the monad and produce none. Otherwise, continue with bar then baz"

[Eric Wieser]

That is, I'm looking for how to translate this python:

try:
    t = foo()
except:
    return None
bar()
return some(1)

but only know how to write

try:
    t = foo()
except:
    t = None
bar()
return some(1)

[Yakov Pechersky]

example : tactic (option nat) :=
(do
  t ← foo,
  bar,
  return (some 1)) <|> return none

?

[Yakov Pechersky]

What's the type of foo? How many such exits do you expect to have in your control flow?

[Eric Wieser]

Right, but that code is

try:
    t = foo()
    bar()
    return some(1)
except:
    return none

which also squashes errors from bar, which I don't want to do

[Eric Wieser]

Let's say that foo is tactic nat

[Yakov Pechersky]

Do you want a different error value if bar fails?

[Eric Wieser]

I want the error from bar to propagate

[Mario Carneiro]

I think you are looking for t ← foo | return none,

[Mario Carneiro]

Actually I think that only works on failed pattern matches, so you might have to rewrite it to some t <- try_core foo | return none, if you want to catch errors in foo

[Eric Wieser]

docs#tactic.try_core sounds like what I was looking for

[Eric Wieser]

What does pattern matching desugar to in ← assignment?

[Mario Carneiro]

It's a pattern match with a wildcard case

[Mario Carneiro]

i.e.

o <- try_core foo,
match o with
| some t := do <rest of the do block>
| _ := return none
end

[Mario Carneiro]

In the case of an alternative monad (like tactic) you can also leave off the | ... part, and it will use failure as the else case

[Eric Wieser]

Can you pattern match with multiple non-wildcard cases?

[Eric Wieser]

Or is the | syntax exclusively for "one case + default"?

[Eric Wieser]

And I guess my other question - where is this syntax documented?

[Ruben Van de Velde]

I would have guessed https://leanprover.github.io/reference/programming.html#monads

[Mario Carneiro]

There is no syntax for binding anything, so I would guess it's only for one pattern plus "anything else"

[kana]

yeah, such syntax from idris/agda will be great

do pattern1 <- a
     | pattern2 := b
     | pattern3 := c, -- should be total
   e

=

a >>= fun x,
  match x with
  | pattern1 := e
  | pattern2 := b
  | pattern3 := c
  end

like

variable get_name : io (option string)

def main := do
  some a ← get_name | none := io.put_str_ln "fail on first name",
  some b ← get_name | none := io.put_str_ln "fail on second name",
  io.put_str_ln (a ++ b)

[Eric Wieser]

I think some of the ->s in your example were intended to be :=?

[kana]

Yes, fixed

[Mario Carneiro]

I don't think this is worth investigating in lean 3, and lean 4 do blocks are so different that it's not clear to me whether this even applies anymore

[Eric Wieser]

Agreed, the only thing that might be worth doing is documenting that this syntax exists somewhere

[Eric Wieser]

Done in https://github.com/leanprover-community/leanprover-community.github.io/pull/174

[kana]

Oh, there are no way to match in else clause? Why the feature is so specialized?

[Mario Carneiro]

If you want a match, use match. I think of this feature as more like rust's if let, which gives you two branches, one if a given pattern matches and one for everything else