## Stream: new members

### Topic: or-else in monadic assignment

#### Eric Wieser (Feb 28 2021 at 18:27):

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 (Feb 28 2021 at 18:28):

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 (Feb 28 2021 at 18:30):

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


?

#### Yakov Pechersky (Feb 28 2021 at 18:34):

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

#### Eric Wieser (Feb 28 2021 at 18:37):

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 (Feb 28 2021 at 18:38):

Let's say that foo is tactic nat

#### Yakov Pechersky (Feb 28 2021 at 18:41):

Do you want a different error value if bar fails?

#### Eric Wieser (Feb 28 2021 at 18:43):

I want the error from bar to propagate

#### Mario Carneiro (Mar 01 2021 at 08:24):

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

#### Mario Carneiro (Mar 01 2021 at 08:26):

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 (Mar 01 2021 at 08:31):

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

#### Eric Wieser (Mar 01 2021 at 08:38):

What does pattern matching desugar to in ← assignment?

#### Mario Carneiro (Mar 01 2021 at 08:44):

It's a pattern match with a wildcard case

#### Mario Carneiro (Mar 01 2021 at 08:44):

i.e.

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


#### Mario Carneiro (Mar 01 2021 at 08:46):

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 (Mar 01 2021 at 09:01):

Can you pattern match with multiple non-wildcard cases?

#### Eric Wieser (Mar 01 2021 at 09:01):

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

#### Eric Wieser (Mar 01 2021 at 09:11):

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

#### Mario Carneiro (Mar 01 2021 at 11:47):

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

#### kana (Mar 01 2021 at 12:46):

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 (Mar 01 2021 at 12:50):

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

Yes, fixed

#### Mario Carneiro (Mar 01 2021 at 14:23):

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 (Mar 01 2021 at 14:24):

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

#### kana (Mar 01 2021 at 17:38):

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

#### Mario Carneiro (Mar 02 2021 at 02:54):

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

Last updated: May 16 2021 at 05:21 UTC