Except

The Except Monad adds exception handling behavior to your functions. Exception handling in other languages like Python or Java is done with a built in throw method that you can use anywhere. In Lean you can only throw an exception when your function is executing in the context of an Except monad.

def 
divide: Float → Float → Except String Float
divide (
x: Float
x 
y: Float
y: 
Float: Type
Float): 
Except: Type → Type → Type
Except 
String: Type
String 
Float: Type
Float :=
  if 
y: Float
y == 
0: Float
0 then
    
throw: {ε : outParam Type} → {m : Type → Type} → [self : MonadExcept ε m] → {α : Type} → ε → m α
throw 
"can't divide by zero": String
"can't divide by zero"
  else
    
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure (
x: Float
x / 
y: Float
y)

#eval
Except.ok 2.500000 
divide: Float → Float → Except String Float
divide 
5: Float
5 
2: Float
2  -- Except.ok 2.500000
#eval
Except.error "can't divide by zero" 
divide: Float → Float → Except String Float
divide 
5: Float
5 
0: Float
0  -- Except.error "can't divide by zero"

Just as the read operation was available from the ReaderM monad and the get and set operations came with the StateM monad, here you can see a throw operation is provided by the Except monad.

So in Lean, throw is not available everywhere like it is in most imperative programming languages. You have to declare your function can throw by changing the type signature to Except String Float. This creates a function that might return an error of type String or it might return a value of type Float in the non-error case.

Once your function is monadic you also need to use the pure constructor of the Except monad to convert the pure non-monadic value x / y into the required Except object. See Applicatives for details on pure.

Now this return typing would get tedious if you had to include it everywhere that you call this function, however, Lean type inference can clean this up. For example, you can define a test function that calls the divide function and you don't need to say anything here about the fact that it might throw an error, because that is inferred:

def 
test: Except String Float
test := 
divide: Float → Float → Except String Float
divide 
5: Float
5 
0: Float
0

#check
test : Except String Float 
test: Except String Float
test     -- Except String Float

Notice the Lean compiler infers the required Except String Float type information for you. And now you can run this test and get the expected exception:

#eval
Except.error "can't divide by zero" 
test: Except String Float
test      -- Except.error "can't divide by zero"

Chaining

Now as before you can build a chain of monadic actions that can be composed together using bind (>>=):

def 
square: Float → Except String Float
square (
x: Float
x : 
Float: Type
Float) : 
Except: Type → Type → Type
Except 
String: Type
String 
Float: Type
Float :=
  if 
x: Float
x >= 
100: Float
100 then
    
throw: {ε : outParam Type} → {m : Type → Type} → [self : MonadExcept ε m] → {α : Type} → ε → m α
throw 
"it's absolutely huge": String
"it's absolutely huge"
  else
    
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure (
x: Float
x * 
x: Float
x)

#eval
Except.ok 9.000000 
divide: Float → Float → Except String Float
divide 
6: Float
6 
2: Float
2 >>= 
square: Float → Except String Float
square  -- Except.ok 9.000000
#eval
Except.error "can't divide by zero" 
divide: Float → Float → Except String Float
divide 
6: Float
6 
0: Float
0 >>= 
square: Float → Except String Float
square  -- Except.error "can't divide by zero"
#eval
Except.error "it's absolutely huge" 
divide: Float → Float → Except String Float
divide 
100: Float
100 
1: Float
1 >>= 
square: Float → Except String Float
square  -- Except.error "it's absolutely huge"

def 
chainUsingDoNotation: Except String Float
chainUsingDoNotation := do
  let 
r: Float
r ← 
divide: Float → Float → Except String Float
divide 
6: Float
6 
0: Float
0
  
square: Float → Except String Float
square 
r: Float
r

#eval
Except.error "can't divide by zero" 
chainUsingDoNotation: Except String Float
chainUsingDoNotation  -- Except.error "can't divide by zero"

Notice in the second divide 6 0 the exception from that division was nicely propagated along to the final result and the square function was ignored in that case. You can see why the square function was ignored if you look at the implementation of Except.bind:

def 
bind: {ε : Type u_1} → {α : Type u_2} → {β : Type u_3} → Except ε α → (α → Except ε β) → Except ε β
bind (
ma: Except ε α
ma : 
Except: Type u_1 → Type u_2 → Type (max u_1 u_2)
Except 
ε: Type u_1
ε 
α: Type u_2
α) (
f: α → Except ε β
f : 
α: Type u_2
α → 
Except: Type u_1 → Type u_3 → Type (max u_1 u_3)
Except 
ε: Type u_1
ε 
β: Type u_3
β) : 
Except: Type u_1 → Type u_3 → Type (max u_1 u_3)
Except 
ε: Type u_1
ε 
β: Type u_3
β :=
  match 
ma: Except ε α
ma with
  | 
Except.error: {ε : Type ?u.2428} → {α : Type ?u.2427} → ε → Except ε α
Except.error 
err: ε
err => 
Except.error: {ε : Type u_1} → {α : Type u_3} → ε → Except ε α
Except.error 
err: ε
err
  | 
Except.ok: {ε : Type ?u.2454} → {α : Type ?u.2453} → α → Except ε α
Except.ok 
v: α
v      => 
f: α → Except ε β
f 
v: α
v

Specifically notice that it only calls the next function f v in the Except.ok, and in the error case it simply passes the same error along.

Remember also that you can chain the actions with implicit binding by using the do notation as you see in the chainUsingDoNotation function above.

Try/Catch

Now with all good exception handling you also want to be able to catch exceptions so your program can continue on or do some error recovery task, which you can do like this:

def 
testCatch: Except String String
testCatch :=
  try
    let 
r: Float
r ← 
divide: Float → Float → Except String Float
divide 
8: Float
8 
0: Float
0  -- 'r' is type Float
    
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure (
toString: {α : Type} → [self : ToString α] → α → String
toString 
r: Float
r)
  catch 
e: String
e =>
    
pure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α
pure s!"Caught exception: {
e: String
e}"

#check
testCatch : Except String String 
testCatch: Except String String
testCatch -- Except String String

Note that the type inferred by Lean for this function is Except String String so unlike the test function earlier, this time Lean type inference has figured out that since the pure value (toString r) is of type String, then this function must have type Except String String so you don't have to explicitly state this. You can always hover your mouse over testCatch or use #check testCatch to query Lean interactively to figure out what type inference has decided. Lean type inference makes life easy for you, so it's good to use it when you can.

You can now see the try/catch working in this eval:

#eval
Except.ok "Caught exception: can't divide by zero" 
testCatch: Except String String
testCatch -- Except.ok "Caught exception: can't divide by zero"

Notice the Caught exception: wrapped message is returned, and that it is returned as an Except.ok value, meaning testCatch eliminated the error result as expected.

So you've interleaved a new concept into your functions (exception handling) and the compiler is still able to type check everything just as well as it does for pure functions and it's been able to infer some things along the way to make it even easier to manage.

Now you might be wondering why testCatch doesn't infer the return type String? Lean does this as a convenience since you could have a rethrow in or after the catch block. If you really want to stop the Except type from bubbling up you can unwrap it like this:

def 
testUnwrap: String
testUnwrap : 
String: Type
String := 
Id.run: {α : Type} → Id α → α
Id.run do
  let 
r: Except String Float
r ← 
divide: Float → Float → Except String Float
divide 
8: Float
8 
0: Float
0 -- r is type Except String Float
  match 
r: Except String Float
r with
  | 
.ok: {ε α : Type} → α → Except ε α
.ok 
a: Float
a => 
toString: {α : Type} → [self : ToString α] → α → String
toString 
a: Float
a -- 'a' is type Float
  | 
.error: {ε α : Type} → ε → Except ε α
.error 
e: String
e => s!"Caught exception: {
e: String
e}"

#check
testUnwrap : String 
testUnwrap: String
testUnwrap -- String
#eval
"Caught exception: can't divide by zero" 
testUnwrap: String
testUnwrap -- "Caught exception: can't divide by zero"

The Id.run function is a helper function that executes the do block and returns the result where Id is the identity monad. So Id.run do is a pattern you can use to execute monads in a function that is not itself monadic. This works for all monads except IO which, as stated earlier, you cannot invent out of thin air, you must use the IO monad given to your main function.

Monadic functions

You can also write functions that are designed to operate in the context of a monad. These functions typically end in upper case M like List.forM used below:

def 
validateList: List Nat → Nat → Except String Unit
validateList (
x: List Nat
x : 
List: Type → Type
List 
Nat: Type
Nat) (
max: Nat
max : 
Nat: Type
Nat): 
Except: Type → Type → Type
Except 
String: Type
String 
Unit: Type
Unit := do
  
x: List Nat
x.
forM: {m : Type → Type} → [inst : Monad m] → {α : Type} → List α → (α → m PUnit) → m PUnit
forM fun 
a: Nat
a => do
    if 
a: Nat
a > 
max: Nat
max then 
throw: {ε : outParam Type} → {m : Type → Type} → [self : MonadExcept ε m] → {α : Type} → ε → m α
throw 
"illegal value found in list": String
"illegal value found in list"

#eval
Except.ok () 
validateList: List Nat → Nat → Except String Unit
validateList [
1: Nat
1, 
2: Nat
2, 
5: Nat
5, 
3: Nat
3, 
8: Nat
8] 
10: Nat
10 -- Except.ok ()
#eval
Except.error "illegal value found in list" 
validateList: List Nat → Nat → Except String Unit
validateList [
1: Nat
1, 
2: Nat
2, 
5: Nat
5, 
3: Nat
3, 
8: Nat
8] 
5: Nat
5 -- Except.error "illegal value found in list"

Notice here that the List.forM function passes the monadic context through to the inner function so it can use the throw function from the Except monad.

The List.forM function is defined like this where [Monad m] means "in the context of a monad m":

def 
forM: {m : Type u_1 → Type u_2} → {α : Type u_3} → [inst : Monad m] → List α → (α → m PUnit) → m PUnit
forM [
Monad: (Type u_1 → Type u_2) → Type (max (u_1 + 1) u_2)
Monad 
m: Type u_1 → Type u_2
m] (
as: List α
as : 
List: Type u_3 → Type u_3
List 
α: Type u_3
α) (
f: α → m PUnit
f : 
α: Type u_3
α → 
m: Type u_1 → Type u_2
m 
PUnit: Type u_1
PUnit) : 
m: Type u_1 → Type u_2
m 
PUnit: Type u_1
PUnit :=
  match 
as: List α
as with
  | []      => 
pure: {f : Type u_1 → Type u_2} → [self : Pure f] → {α : Type u_1} → α → f α
pure 
⟨⟩: PUnit
⟨⟩
  | 
a: α
a :: 
as: List α
as => do 
f: α → m PUnit
f 
a: α
a; 
List.forM: {m : Type u_1 → Type u_2} → [inst : Monad m] → {α : Type u_3} → List α → (α → m PUnit) → m PUnit
List.forM 
as: List α
as 
f: α → m PUnit
f

Summary

Now that you know all these different monad constructs, you might be wondering how you can combine them. What if there was some part of your state that you wanted to be able to modify (using the State monad), but you also needed exception handling. How can you get multiple monadic capabilities in the same function. To learn the answer, head to Monad Transformers.