Zulip Chat Archive

Stream: new members

Topic: or-else in monadic assignment


view this post on Zulip 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"

view this post on Zulip 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)

view this post on Zulip Yakov Pechersky (Feb 28 2021 at 18:30):

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

?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 28 2021 at 18:38):

Let's say that foo is tactic nat

view this post on Zulip Yakov Pechersky (Feb 28 2021 at 18:41):

Do you want a different error value if bar fails?

view this post on Zulip Eric Wieser (Feb 28 2021 at 18:43):

I want the error from bar to propagate

view this post on Zulip Mario Carneiro (Mar 01 2021 at 08:24):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 01 2021 at 08:31):

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

view this post on Zulip Eric Wieser (Mar 01 2021 at 08:38):

What does pattern matching desugar to in assignment?

view this post on Zulip Mario Carneiro (Mar 01 2021 at 08:44):

It's a pattern match with a wildcard case

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 01 2021 at 09:01):

Can you pattern match with multiple non-wildcard cases?

view this post on Zulip Eric Wieser (Mar 01 2021 at 09:01):

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

view this post on Zulip Eric Wieser (Mar 01 2021 at 09:11):

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

view this post on Zulip Ruben Van de Velde (Mar 01 2021 at 09:21):

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

view this post on Zulip 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"

view this post on Zulip 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)

view this post on Zulip Eric Wieser (Mar 01 2021 at 12:50):

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

view this post on Zulip kana (Mar 01 2021 at 12:51):

Yes, fixed

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 01 2021 at 14:24):

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

view this post on Zulip Eric Wieser (Mar 01 2021 at 15:45):

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

view this post on Zulip kana (Mar 01 2021 at 17:38):

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

view this post on Zulip 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