error handling with result

Stream: lean4

[Joseph O]

I want to have a function that returns a result, instead of panicking, yet after looking through the mathlib4 docs and the lean4 repo, I couldn't find much use with it. Would someone mind giving an example of using the Result type?

[Xubai Wang]

Do you mean EStateM.Result ? The basic approach is through pattern matching, as they are just plain inductive. You can also use the try ... catch e => and throw syntax sugar in do blocks (try searching for try in lean source) , which is implemented using the type class MonadExceptOf.

All three of Result.ok a, pure a, return a will turn a : A into a Result A. And since IO is just a special case of EStateM, any of the IO functions can be an example.

[Xubai Wang]

Also note that there is top levelExcept in Lean, which plays the same role as Result in rust.

docs4#EStateM.Result
docs4#MonadExceptOf
docs4#Except

[Joseph O]

Xubai Wang said:

Also note that there is top levelExcept in Lean, which plays the same role as Result in rust.

docs4#EStateM.Result
docs4#MonadExceptOf
docs4#Except

I think except is what I am looking for. I didn’t plan on using monads for this.

[Joseph O]

How could I use except as a function return type? How do I return the error?

[Xubai Wang]

def foo (n : Nat) : Except String Nat :=
  if n > 0 then
    Except.ok n
  else
    Except.error "n must be positive"

def foo' (n : Nat) : Except String Nat :=
  if n > 0 then
    pure n
  else
    throw "n must be positive"

where pure and throw are type class function rather than keywords.

[Joseph O]

Thanks!

[Joseph O]

Which should I use? the first or the second?

[Xubai Wang]

Whichever you like. They are actually the same. As there is

instance : Monad (Except ε) where
  pure := Except.pure -- which is Except.ok
  bind := Except.bind
  map  := Except.map

instance (ε) : MonadExceptOf ε (Except ε) where
  throw    := Except.error
  tryCatch := Except.tryCatch