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.2407} → {α : Type ?u.2406} → ε → Except ε α
Except.error err: ε
err => Except.error: {ε : Type u_1} → {α : Type u_3} → ε → Except ε α
Except.error err: ε
err
| Except.ok: {ε : Type ?u.2433} → {α : Type ?u.2432} → α → 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.