# 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.

defdivide (divide:Float → Float → Except String Floatxx:Floaty:y:FloatFloat):Float:TypeExceptExcept:Type → Type → TypeStringString:TypeFloat := ifFloat:Typey ==y:Float0 then0:Floatthrowthrow:{ε : outParam Type} → {m : Type → Type} → [self : MonadExcept ε m] → {α : Type} → ε → m α"can't divide by zero" else"can't divide by zero":Stringpure (pure:{f : Type → Type} → [self : Pure f] → {α : Type} → α → f αx /x:Floaty)y:Floatdividedivide:Float → Float → Except String Float55:Float2 -- Except.ok 2.5000002:Floatdividedivide:Float → Float → Except String Float55:Float0 -- Except.error "can't divide by zero"0:Float

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:

deftest :=test:Except String Floatdividedivide:Float → Float → Except String Float55:Float00:Floattest -- Except String Floattest: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:

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

## Chaining

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

:

defsquare (square:Float → Except String Floatx :x:FloatFloat) :Float:TypeExceptExcept:Type → Type → TypeStringString:TypeFloat := ifFloat:Typex >=x:Float100 then100:Floatthrowthrow:{ε : outParam Type} → {m : Type → Type} → [self : MonadExcept ε m] → {α : Type} → ε → m α"it's absolutely huge" else"it's absolutely huge":Stringpure (pure:{f : Type → Type} → [self : Pure f] → {α : Type} → α → f αx *x:Floatx)x:Floatdividedivide:Float → Float → Except String Float66:Float2 >>=2:Floatsquare -- Except.ok 9.000000square:Float → Except String Floatdividedivide:Float → Float → Except String Float66:Float0 >>=0:Floatsquare -- Except.error "can't divide by zero"square:Float → Except String Floatdividedivide:Float → Float → Except String Float100100:Float1 >>=1:Floatsquare -- Except.error "it's absolutely huge" defsquare:Float → Except String FloatchainUsingDoNotation := do letchainUsingDoNotation:Except String Floatr ←r:Floatdividedivide:Float → Float → Except String Float66:Float00:Floatsquaresquare:Float → Except String Floatrr:FloatchainUsingDoNotation -- Except.error "can't divide by zero"chainUsingDoNotation:Except String Float

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.919} → {α : Type ?u.918} → ε → Except ε α

Except.error `err`**: **ε

err => `Except.error`**: **{ε : Type u_1} → {α : Type u_3} → ε → Except ε α

Except.error `err`**: **ε

err
| `Except.ok`**: **{ε : Type ?u.945} → {α : Type ?u.944} → α → 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:

deftestCatch := try lettestCatch:Except String Stringr ←r:Floatdividedivide:Float → Float → Except String Float88:Float0 -- 'r' is type Float0:Floatpure (pure:{f : Type → Type} → [self : Pure f] → {α : Type} → α → f αtoStringtoString:{α : Type} → [self : ToString α] → α → Stringr) catchr:Floate =>e:Stringpure s!"Caught exception: {pure:{f : Type → Type} → [self : Pure f] → {α : Type} → α → f αe}"e:StringtestCatch -- Except String StringtestCatch: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:

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

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:

deftestUnwrap :testUnwrap:StringString :=String:TypeId.run do letId.run:{α : Type} → Id α → αr ←r:Except String Floatdividedivide:Float → Float → Except String Float88:Float0 -- r is type Except String Float match0:Floatr with |r:Except String Float.ok.ok:{ε α : Type} → α → Except ε αa =>a:FloattoStringtoString:{α : Type} → [self : ToString α] → α → Stringa -- 'a' is type Float |a:Float.error.error:{ε α : Type} → ε → Except ε αe => s!"Caught exception: {e:Stringe}"e:StringtestUnwrap -- StringtestUnwrap:StringtestUnwrap -- "Caught exception: can't divide by zero"testUnwrap:String

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:

defvalidateList (validateList:List Nat → Nat → Except String Unitx :x:List NatListList:Type → TypeNat) (Nat:Typemax :max:NatNat):Nat:TypeExceptExcept:Type → Type → TypeStringString:TypeUnit := doUnit:Typex.x:List NatforM funforM:{m : Type → Type} → [inst : Monad m] → {α : Type} → List α → (α → m PUnit) → m PUnita => do ifa:Nata >a:Natmax thenmax:Natthrowthrow:{ε : outParam Type} → {m : Type → Type} → [self : MonadExcept ε m] → {α : Type} → ε → m α"illegal value found in list""illegal value found in list":StringvalidateList [validateList:List Nat → Nat → Except String Unit1,1:Nat2,2:Nat5,5:Nat3,3:Nat8]8:Nat10 -- Except.ok ()10:NatvalidateList [validateList:List Nat → Nat → Except String Unit1,1:Nat2,2:Nat5,5:Nat3,3:Nat8]8:Nat5 -- Except.error "illegal value found in list"5:Nat

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.