try, catch, else

Stream: lean4

[Eric Wieser]

Python has an extended version of try/catch (there, except) which has an else clause:

try:
   x = foo()
except Exception as e:
   bar()
else:
   baz(x)

which has semantics:

• foo crashes -> run bar. If bar crashes, propagate the error
• foo succeeds -> run baz. If baz crashes, propagate the error

For what I can tell, Lean only offers

import Lean
open Lean Meta

variable (foo1 foo2 : MetaM Nat)
variable (bar : MetaM Int)
variable (baz : Nat → Nat → MetaM Int)

example : MetaM Int := do
  try
    let x ← foo1
    let y ← foo2
    baz x y
  catch _ =>
    bar

which has the wrong semantics when baz fails of also catching that error.

[Eric Wieser]

I can write this as a workaround:

example : MetaM Int := do
  let ret ← try
      let x ← foo1
      let y ← foo2
      pure <| Sum.inl (x, y)
    catch _ =>
      pure <| Sum.inr (← bar)
  match ret with
  | .inl (x, y) => baz x y
  | .inr r => return r

but it's a lot less clear

[Eric Wieser]

(I previously asked this here)

[James Gallicchio]

I thought we had finally?

[Eric Wieser]

finally runs even if an error does happen, and so does not have access to local variables within the try

[Eric Wieser]

Ah, this works:

import Lean
open Lean Meta

def foo1 : MetaM Nat := return 1
def foo2 (fail : Bool) : MetaM Nat := if fail then failure else return 10
def bar : MetaM Int := do
  trace[debug] "ran bar"
  return 2
def baz (x y : Nat) : MetaM Int := do
  trace[debug] "ran baz"
  return x + y

/--
Would like to write as
try
  let x ← foo1
  let y ← foo2 false
catch _ =>
  bar
else
  baz x y
-/
def test : MetaM Int := do
  (← try
      let x ← foo1
      let y ← foo2 false
      return do
        baz x y
    catch _ =>
      return do
        bar)

set_option trace.debug true
#eval test

[Eric Wieser]

The trick is to enter a nested do block inside the try, but call it from the outside

[Eric Wieser]

But this of course means that you can't do a return inside the try block; so this would need to be handled as part of the do elaborator

[Mac Malone]

@Eric Wieser When it comes to mirroring Python logic, it should be noted that the Lean try/catch and Python try/except do not already have the same semantics:

Lean

-- error: catch2
#eval show IO Unit from do
  try
    throw <| IO.userError "try"
  catch _ =>
    throw <| IO.userError "catch1"
  catch _ =>
    throw <| IO.userError "catch2"

Python

# error: catch1
try:
    raise RuntimeError("try")
except Exception:
    raise RuntimeError("catch1")
except Exception:
    raise RuntimeError("catch2")

The difference here being that the Lean try/catch is cumulative whereas the Python try/except is disjoint. Thus, if Python-style try/else where implemented in Lean, there is design decision on whether it should succeed if the just try was error free or if the all the catch satements were also error free. The later would appear to be more consistent with the current design.

[Eric Wieser]

I guess the Lean way to spell disjoint catches is

  try
    throw <| IO.userError "try"
  catch
    | (.userError s) =>
      throw <| IO.userError "catch1"
    | _ =>
      throw <| IO.userError "catch2"

[Eric Wieser]

I think it would be reasonable to just ban multiple catches if else is used

[Mauricio Collares]

Eric Wieser said:

finally runs even if an error does happen, and so does not have access to local variables within the try

Not sure I follow; control blocks do not create new lexical scopes in Python, and therefore local variables inside the try are local to the function you're in, and will be accessible in the finally block. Of course, if an exception is raised before assigning to a new variable inside the try block, it won't be defined in the finally block (unlike JS, say, where let bindings are hoisted).

[Mac Malone]

Eric Wieser said:

I guess the Lean way to spell disjoint catches is

That only works if the exception types are homongenous. There is no way I know of to express a heterogenous disjoint try/catch in Lean. For example, consider:

-- catchIO
#eval show IO (Except Nat Unit) from ExceptT.run do
  try
    throw 0
  catch n : Nat =>
    throwThe IO.Error <| .userError "catchNat"
  catch e : IO.Error =>
    throwThe IO.Error <| .userError "catchIO"

[Mac Malone]

Here is a quick-and-dirty example of a cumulative try/catch/else in Lean:

import Lean.Parser.Do

open Lean Parser Term

syntax doElseTerm :=
 Term.binderIdent (" : " term)?

syntax doElse :=
  ppDedent(ppLine) ("else " atomic(doElseTerm darrow)?) doSeq

syntax (name := doTryElse) (priority := high)
"try" doSeq (doCatch <|> doCatchMatch)* (doElse)? (doFinally)?  : doElem

instance : Coe (TSyntax ``Term.hole) Term where
  coe x := Unhygienic.run do withRef x `($x:hole)

instance : Coe (TSyntax [identKind, ``Term.hole]) Term where
  coe x := match x with | `($x:ident) => x | `($x:hole) => x | _ => unreachable!

instance : Coe (TSyntax ``doTry) (TSyntax ``doSeq) where
  coe x := Unhygienic.run do withRef x `(doSeq|$x:doTry)

macro_rules
| `(doTryElse|try $x:doSeq else%$ref $[$a? =>]? $y:doSeq) => do
  let a : Term ← do
    if let some a := a? then
      let `(doElseTerm|$a $[: $ty?]?) := a
        | Macro.throwUnsupported
      if let some ty := ty? then `(($a : $ty)) else pure a
    else
      withRef ref `(_)
  `(doElem|match (← observing do $x) with | .ok $a => $y | .error e => throw e)
| `(doTryElse|try $x:doSeq $catches* $[$els?:doElse]? $[$fin?]?) => do
  let mut x : TSyntax ``doSeq := x
  x := ← `(doTry|try $x:doSeq $catches*)
  if let some els := els? then x := ← `(doSeq|try $x:doSeq $els:doElse)
  if let some fin := fin? then x := ← `(doTry|try $x:doSeq $fin:doFinally)
  `(doElem|do $x)

def foo : IO Int := pure 1
def bar : IO Int := pure 2
def baz (x : Int) : IO Int := return x + 10

-- 11
#eval show IO Int from do
  try
    foo
  catch _ =>
    bar
  else x =>
    baz x

[Eric Wieser]

Doesn't that else run if foo fails?

[Eric Wieser]

And does this work for accessing local variables within the try like the ones in my example?