Try Catch

Stream: new members

[Philipp]

In the Lean Manual about the Except Monad: https://lean-lang.org/lean4/doc/monads/except.lean.html, there is an example for try catch:

def testCatch :=
  try
    let r ← divide 8 0  -- 'r' is type Float
    pure (toString r)
  catch e =>
    pure s!"Caught exception: {e}"

#check testCatch -- Except String String

Why does this return Except String String? My thought is that if let r ← divide 8 0throws an exception, we execute the catch block that returns a string - and the try block also returns a string (toString r).
So I guess the Except comes from the pure, but we cannot raise an Exception from this function, so why do we need the pure and can't just return a String?

[Ruben Van de Velde]

Have you tried removing the two pures and seeing what happens?

[Philipp]

Is there a Lean playground that works on mobile? :sweat_smile:

[Kevin Buzzard]

I think the lean playground https://live.lean-lang.org/ works fine on mobile? (and exposes the fact that your code isn't a #mwe )

[Philipp]

oh wow yes it does - it just gave me a hard time copy/paste-ing from the lean manual. That's also why I didn't fully write an mwe, sorry. Here is the tediously re-formatted definition of divide:

def divide ( x y: Float): Except String Float :=
  if y == 0 then
    throw "can't divide by zero"
  else
    pure (x / y)

Anyways, I removed the pure and added : String to testCatch as return type. Now it says invalid do notation, expected type is not a monad application, on the try.

But why do I need a monad here? Isn't try/catch a way to unwrap/recover from an exception?

[Kyle Miller]

@Philipp If you're familiar with try/catch in imperative programming languages, the difference is that functional programming languages avoid implicit state and nonlocal control flow, and instead they tend to use monads to make the state and nonlocal control flow more explicit.

A language like Python can be modeled as there being a pervasive monad that handles global mutable variables, how IO operations are sequenced, and how exceptions trigger try/except blocks. This "Python monad" cannot be turned off, and so, for example, you can't be sure that a given function doesn't have any side effects without carefully auditing the code. With Lean, by looking at which monad is being used, you know exactly the range of possible effects -- for example, no monad means "this function will never raise an exception".

Plus, in Lean you can implement exactly how try/catch evaluates. The Except monad gives an implementation for try/catch, it's not something provided by the core Language itself.

(The Lean language does provide a way to create a runtime error using panic!, but that's more for assertion violations, which are not recoverable, and so I wouldn't consider that to be an exception.)

[Kyle Miller]

I think this is what hooks in the try/catch implementation for Except: https://github.com/leanprover/lean4/blob/b614ff1d12bc38f39077f9ce9f2d48b42c003ad0/src/Init/Prelude.lean#L2989-L2991

That refers to another definition (Except.tryCatch), which makes it so the way try x catch e => y works is that it evaluates x, sees if it evaluates to an error, and if so evaluates y instead.

[Kyle Miller]

I'm not sure if the manual explains Except before that chapter, so I'll just add that Except String Float is a type that has two kinds of values, either Except.error s with s a string, or Except.ok x with x a float. It's called "except", but unlike say Python that doesn't mean it does fancy things like have runtime support for stack unwinding.

[Philipp]

Hmm I understand State/Reader Monads and State in general, but I would expect that tryCatch would have a definition that is more like

def tryCatch (e : Except a b) (handle : b -> a) : a :=
  match a with
  | Except.ok a => a
  | Except.err b => handle b

(probably wrong syntax but I hope you get the gist)

The question is why do we want to carry information about the Except around after it is caught?

e.g. in Java I think methods need to be marked with throws ... if they can throw an exception. If such a method is called in try/catch then the caller does not need to be marked throws.

[Philipp]

In the example from the Manual, #eval testCatch evaluates to Except.ok "Caught exception: can't divide by zero", and from the code (especially the return type of catch) we know that it can never return Except.error. So why keep the result wrapped in Except

[Kyle Miller]

What if the catch clause wants to throw an exception?

[Henrik Böving]

The notion that is implemented in the try catch notation is more general than this. It allows you to e.g. re-raise exceptions. Or for example if you are in an IO monad you can do some IO, catch its errors and then handle that IO error by e.g. closing a file descriptor, doing some logging etc.

[Philipp]

If the catch clause wants to throw an error, we have to return Except; but why can't we drop it if it's guaranteed not to

[Kyle Miller]

Yeah, to generalize what I said, "what if the catch clause wants to have side-effects"? This is the common case.

[Henrik Böving]

With your type signature above this would mean you woud have to provide an (Except (Except a b) c) which is not a type that you really want to deal with I believe

[Henrik Böving]

The current implementation does also not prevent you from doing what you are interested in. You can implement the behavior you want by doing exactly what you did, pattern matching on the result.

[Philipp]

In that case I would use

def testCatch :=
  match $ divide 8 0
  | Except.ok r =>  pure (toString r)  -- 'r' is type Float
  | Except.err e =>  pure s!"Caught exception: {e}"

I guess?

[Henrik Böving]

You would use this for what?

[Kyle Miller]

If you do want to resolve everything to a String like that, then there's no need for pure (there's no monad)

def testCatch :=
  match divide 8 0 with
  | Except.ok r =>  toString r
  | Except.error e => s!"Caught exception: {e}"

[Kyle Miller]

There's also a feature where you can write this more succinctly as

def testCatch :=
  match divide 8 0 with
  | .ok r => toString r
  | .error e => s!"Caught exception: {e}"

[Kyle Miller]

@Henrik Böving This testCatch example is from the Lean manual. Maybe it's not fair to ask Philipp to justify the design here :-)

[Kyle Miller]

@Philipp Speaking of the manual, just a bit further down testUnwrap is an example of removing that Except String. I'm not sure Id.run and all that is a good illustration though -- what we have here with a direct match seems more idiomatic.

[Philipp]

Oh sorry I forgot to delete the pure's. The .ok / .error is pretty cool! Thanks!

So what I like about try/catch is that it's a do block so I can call multiple methods that might throw an exception:

def foo (n : Nat) : Except String Nat :=
  if n == 0 then .error "n is zero" else pure $ n^2

def bar (n : Nat) : Except String Float :=
  if n.toFloat.isNaN then Except.error "Float is NaN" else pure n.toFloat

def testCatch :=
  try
    let n ← foo 2
    let r ← bar n
    pure r.toString
  catch e =>
    pure s!"Something went wrong: {e}"

If either foo or bar throw an exception (return Exception.error) we end up in the catch block. With match this would become something like this?

def testMatch :=
  match Id.run do
    let n ← foo 2
    let r ← bar n
    pure r.toString
  with
  | .ok a => a
  | .error e => s!"Something went wrong: {e}"

(doesn't compile, n here is type Except String Nat and not Nat - I guess Id.run doesn't do what I thought it does).

So I could drop the do notation and write

def testMatch :=
  match foo 2 >>= bar >>= λx => pure x.toString
  with
  | .ok a => a
  | .error e => s!"Something went wrong: {e}"

but that is uhm way less readable.

[Kyle Miller]

Henrik's question is good one though: under what circumstances is turning Except String String into String a good design?

[Kyle Miller]

If there's a good reason for it, I might organize it something like

def Except.run (e : Except ε α) (handle : ε → α) : α :=
  match e with
  | .ok x => x
  | .error e => handle e

def testMatch := Except.run
  (do
    let n ← foo 2
    let r ← bar n
    pure r.toString)
  (handle := fun e => s!"Something went wrong: {e}")

[Philipp]

Hmm yes, maybe that is not a great idea.
What IS a good use for try / catch then?