Option to Except

Stream: lean4

[Marcus Rossel]

Is there a terse way to handle the following situation in do-notation?:

example (o : Option Nat) : Except String Nat :=
  match o with
  | none => throw "error"
  | some o => sorry -- do something with o

I was hoping something like this (pseudo notation) would be possible:

example (o : Option Nat) : Except String Nat :=
  let o ← o | "error"

[Henrik Böving]

let some x := foo | throw "error"

Maybe?

[Marcus Rossel]

Yes, that works! What is this |-syntax called?

[Kevin Buzzard]

"pipe"?

[Marcus Rossel]

Kevin Buzzard said:

"pipe"?

:D I meant that more in a conceptual manner. Like if := is the syntax for an assignment, then | is the syntax for _?

[Henrik Böving]

Marcus Rossel said:

Yes, that works! What is this |-syntax called?

Dont know an official name for it. I would call it let matching or something like that based on the if-let naming

[Kyle Miller]

In the code there's the variable elseSeq in a few places, so maybe the whole thing could be called a "let-else" with the | ... the "else sequence"?

[Kyle Miller]

You can actually put multiple do-elements after the | by the way, hence elseSeq refers to this part of the syntax.

[Joachim Breitner]

“inline alternative” maybe?

[Adam Topaz]

I think alternative is definitely something in the name. You need a docs#Alternative instance

[Kyle Miller]

@Adam Topaz You don't seem to need an Alternative instance to use these else sequences.

def Id' (α : Type) := α

instance : Monad Id' where
  pure x := x
  bind x f := f x

def foo (x? : Option Nat) : Id' Nat := do
  let some x := x? | return 0
  return x

[Adam Topaz]

Oh!

[Adam Topaz]

Is anything actually needed for |?

[Kyle Miller]

Nope, it gets translated into a match expression. let patt := x | a; b is match x with | patt => b; _ => a

[Adam Topaz]

Oh wait. I was confused. There must be some instance on Option, presumably Alternative. This syntax also works for Except.

[David Thrane Christiansen]

If I were to name it, I'd call it a "fallback", which seems to not conflict with existing terminology