# A Monad Construction Kit

`ReaderT`

is far from the only useful monad transformer.
This section describes a number of additional transformers.
Each monad transformer consists of the following:

- A definition or datatype
`T`

that takes a monad as an argument. It should have a type like`(Type u → Type v) → Type u → Type v`

, though it may accept additional arguments prior to the monad. - A
`Monad`

instance for`T m`

that relies on an instance of`Monad m`

. This enables the transformed monad to be used as a monad. - A
`MonadLift`

instance that translates actions of type`m α`

into actions of type`T m α`

, for arbitrary monads`m`

. This enables actions from the underlying monad to be used in the transformed monad.

Furthermore, the `Monad`

instance for the transformer should obey the contract for `Monad`

, at least if the underlying `Monad`

instance does.
In addition, `monadLift (pure x)`

should be equivalent to `pure x`

in the transformed monad, and `monadLift`

should distribute over `bind`

so that `monadLift (x >>= f)`

is the same as `monadLift x >>= fun y => monadLift (f y)`

.

Many monad transformers additionally define type classes in the style of `MonadReader`

that describe the actual effects available in the monad.
This can provide more flexibility: it allows programs to be written that rely only on an interface, and don't constrain the underlying monad to be implemented by a given transformer.
The type classes are a way for programs to express their requirements, and monad transformers are a convenient way to meet these requirements.

## Failure with `OptionT`

Failure, represented by the `Option`

monad, and exceptions, represented by the `Except`

monad, both have corresponding transformers.
In the case of `Option`

, failure can be added to a monad by having it contain values of type `Option α`

where it would otherwise contain values of type `α`

.
For example, `IO (Option α)`

represents `IO`

actions that don't always return a value of type `α`

.
This suggests the definition of the monad transformer `OptionT`

:

```
def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
m (Option α)
```

As an example of `OptionT`

in action, consider a program that asks the user questions.
The function `getSomeInput`

asks for a line of input and removes whitespace from both ends.
If the resulting trimmed input is non-empty, then it is returned, but the function fails if there are no non-whitespace characters:

```
def getSomeInput : OptionT IO String := do
let input ← (← IO.getStdin).getLine
let trimmed := input.trim
if trimmed == "" then
failure
else pure trimmed
```

This particular application tracks users with their name and their favorite species of beetle:

```
structure UserInfo where
name : String
favoriteBeetle : String
```

Asking the user for input is no more verbose than a function that uses only `IO`

would be:

```
def getUserInfo : OptionT IO UserInfo := do
IO.println "What is your name?"
let name ← getSomeInput
IO.println "What is your favorite species of beetle?"
let beetle ← getSomeInput
pure ⟨name, beetle⟩
```

However, because the function runs in an `OptionT IO`

context rather than just in `IO`

, failure in the first call to `getSomeInput`

causes the whole `getUserInfo`

to fail, with control never reaching the question about beetles.
The main function, `interact`

, invokes `getUserInfo`

in a purely `IO`

context, which allows it to check whether the call succeeded or failed by matching on the inner `Option`

:

```
def interact : IO Unit := do
match ← getUserInfo with
| none => IO.eprintln "Missing info"
| some ⟨name, beetle⟩ => IO.println s!"Hello {name}, whose favorite beetle is {beetle}."
```

### The Monad Instance

Writing the monad instance reveals a difficulty.
Based on the types, `pure`

should use `pure`

from the underlying monad `m`

together with `some`

.
Just as `bind`

for `Option`

branches on the first argument, propagating `none`

, `bind`

for `OptionT`

should run the monadic action that makes up the first argument, branch on the result, and then propagate `none`

.
Following this sketch yields the following definition, which Lean does not accept:

```
instance [Monad m] : Monad (OptionT m) where
pure x := pure (some x)
bind action next := do
match (← action) with
| none => pure none
| some v => next v
```

The error message shows a cryptic type mismatch:

```
application type mismatch
pure (some x)
argument
some x
has type
Option α✝ : Type ?u.25
but is expected to have type
α✝ : Type ?u.25
```

The problem here is that Lean is selecting the wrong `Monad`

instance for the surrounding use of `pure`

.
Similar errors occur for the definition of `bind`

.
One solution is to use type annotations to guide Lean to the correct `Monad`

instance:

```
instance [Monad m] : Monad (OptionT m) where
pure x := (pure (some x) : m (Option _))
bind action next := (do
match (← action) with
| none => pure none
| some v => next v : m (Option _))
```

While this solution works, it is inelegant and the code becomes a bit noisy.

An alternative solution is to define functions whose type signatures guide Lean to the correct instances.
In fact, `OptionT`

could have been defined as a structure:

```
structure OptionT (m : Type u → Type v) (α : Type u) : Type v where
run : m (Option α)
```

This would solve the problem, because the constructor `OptionT.mk`

and the field accessor `OptionT.run`

would guide type class inference to the correct instances.
The downside to doing this is that structure values would need to be allocated and deallocated repeatedly when running code that uses it, while the direct definition is a compile-time-only feature.
The best of both worlds can be achieved by defining functions that serve the same role as `OptionT.mk`

and `OptionT.run`

, but that work with the direct definition:

```
def OptionT.mk (x : m (Option α)) : OptionT m α := x
def OptionT.run (x : OptionT m α) : m (Option α) := x
```

Both functions return their inputs unchanged, but they indicate the boundary between code that is intended to present the interface of `OptionT`

and code that is intended to present the interface of the underlying monad `m`

.
Using these helpers, the `Monad`

instance becomes more readable:

```
instance [Monad m] : Monad (OptionT m) where
pure x := OptionT.mk (pure (some x))
bind action next := OptionT.mk do
match ← action with
| none => pure none
| some v => next v
```

Here, the use of `OptionT.mk`

indicates that its arguments should be considered as code that uses the interface of `m`

, which allows Lean to select the correct `Monad`

instances.

After defining the monad instance, it's a good idea to check that the monad contract is satisfied.
The first step is to show that `bind (pure v) f`

is the same as `f v`

.
Here's the steps:

`bind (pure v) f`

*Unfolding the definitions of*}=

`bind`

and `pure`

```
OptionT.mk do
match ← pure (some v) with
| none => pure none
| some x => f x
```

*Desugaring nested action syntax*}=

```
OptionT.mk do
let y ← pure (some v)
match y with
| none => pure none
| some x => f x
```

*Desugaring*}=

`do`

-notation```
OptionT.mk
(pure (some v) >>= fun y =>
match y with
| none => pure none
| some x => f x)
```

*Using the first monad rule for*}=

`m`

```
OptionT.mk
(match some v with
| none => pure none
| some x => f x)
```

*Reduce*}=

`match`

`OptionT.mk (f v)`

*Definition of*}=

`OptionT.mk`

`f v`

The second rule states that `bind w pure`

is the same as `w`

.
To demonstrate this, unfold the definitions of `bind`

and `pure`

, yielding:

```
OptionT.mk do
match ← w with
| none => pure none
| some v => pure (some v)
```

In this pattern match, the result of both cases is the same as the pattern being matched, just with `pure`

around it.
In other words, it is equivalent to `w >>= fun y => pure y`

, which is an instance of `m`

's second monad rule.

The final rule states that `bind (bind v f) g`

is the same as `bind v (fun x => bind (f x) g)`

.
It can be checked in the same way, by expanding the definitions of `bind`

and `pure`

and then delegating to the underlying monad `m`

.

### An `Alternative`

Instance

One convenient way to use `OptionT`

is through the `Alternative`

type class.
Successful return is already indicated by `pure`

, and the `failure`

and `orElse`

methods of `Alternative`

provide a way to write a program that returns the first successful result from a number of subprograms:

```
instance [Monad m] : Alternative (OptionT m) where
failure := OptionT.mk (pure none)
orElse x y := OptionT.mk do
match ← x with
| some result => pure (some result)
| none => y ()
```

### Lifting

Lifting an action from `m`

to `OptionT m`

only requires wrapping `some`

around the result of the computation:

```
instance [Monad m] : MonadLift m (OptionT m) where
monadLift action := OptionT.mk do
pure (some (← action))
```

## Exceptions

The monad transformer version of `Except`

is very similar to the monad transformer version of `Option`

.
Adding exceptions of type `ε`

to some monadic action of type `m α`

can be accomplished by adding exceptions to `α`

, yielding type `m (Except ε α)`

:

```
def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
m (Except ε α)
```

`OptionT`

provides `mk`

and `run`

functions to guide the type checker towards the correct `Monad`

instances.
This trick is also useful for `ExceptT`

:

```
def ExceptT.mk {ε α : Type u} (x : m (Except ε α)) : ExceptT ε m α := x
def ExceptT.run {ε α : Type u} (x : ExceptT ε m α) : m (Except ε α) := x
```

The `Monad`

instance for `ExceptT`

is also very similar to the instance for `OptionT`

.
The only difference is that it propagates a specific error value, rather than `none`

:

```
instance {ε : Type u} {m : Type u → Type v} [Monad m] : Monad (ExceptT ε m) where
pure x := ExceptT.mk (pure (Except.ok x))
bind result next := ExceptT.mk do
match ← result with
| .error e => pure (.error e)
| .ok x => next x
```

The type signatures of `ExceptT.mk`

and `ExceptT.run`

contain a subtle detail: they annotate the universe levels of `α`

and `ε`

explicitly.
If they are not explicitly annotated, then Lean generates a more general type signature in which they have distinct polymorphic universe variables.
However, the definition of `ExceptT`

expects them to be in the same universe, because they can both be provided as arguments to `m`

.
This can lead to a problem in the `Monad`

instance where the universe level solver fails to find a working solution:

```
def ExceptT.mk (x : m (Except ε α)) : ExceptT ε m α := x
instance {ε : Type u} {m : Type u → Type v} [Monad m] : Monad (ExceptT ε m) where
pure x := ExceptT.mk (pure (Except.ok x))
bind result next := ExceptT.mk do
match (← result) with
| .error e => pure (.error e)
| .ok x => next x
```

```
stuck at solving universe constraint
max ?u.12144 ?u.12145 =?= u
while trying to unify
ExceptT ε m α✝
with
(ExceptT ε m α✝) ε m α✝
```

This kind of error message is typically caused by underconstrained universe variables. Diagnosing it can be tricky, but a good first step is to look for reused universe variables in some definitions that are not reused in others.

Unlike `Option`

, the `Except`

datatype is typically not used as a data structure.
It is always used as a control structure with its `Monad`

instance.
This means that it is reasonable to lift `Except ε`

actions into `ExceptT ε m`

, as well as actions from the underlying monad `m`

.
Lifting `Except`

actions into `ExceptT`

actions is done by wrapping them in `m`

's `pure`

, because an action that only has exception effects cannot have any effects from the monad `m`

:

```
instance [Monad m] : MonadLift (Except ε) (ExceptT ε m) where
monadLift action := ExceptT.mk (pure action)
```

Because actions from `m`

do not have any exceptions in them, their value should be wrapped in `Except.ok`

.
This can be accomplished using the fact that `Functor`

is a superclass of `Monad`

, so applying a function to the result of any monadic computation can be accomplished using `Functor.map`

:

```
instance [Monad m] : MonadLift m (ExceptT ε m) where
monadLift action := ExceptT.mk (.ok <$> action)
```

### Type Classes for Exceptions

Exception handling fundamentally consists of two operations: the ability to throw exceptions, and the ability to recover from them.
Thus far, this has been accomplished using the constructors of `Except`

and pattern matching, respectively.
However, this ties a program that uses exceptions to one specific encoding of the exception handling effect.
Using a type class to capture these operations allows a program that uses exceptions to be used in *any* monad that supports throwing and catching.

Throwing an exception should take an exception as an argument, and it should be allowed in any context where a monadic action is requested.
The "any context" part of the specification can be written as a type by writing `m α`

—because there's no way to produce a value of any arbitrary type, the `throw`

operation must be doing something that causes control to leave that part of the program.
Catching an exception should accept any monadic action together with a handler, and the handler should explain how to get back to the action's type from an exception:

```
class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) where
throw : ε → m α
tryCatch : m α → (ε → m α) → m α
```

The universe levels on `MonadExcept`

differ from those of `ExceptT`

.
In `ExceptT`

, both `ε`

and `α`

have the same level, while `MonadExcept`

imposes no such limitation.
This is because `MonadExcept`

never places an exception value inside of `m`

.
The most general universe signature recognizes the fact that `ε`

and `α`

are completely independent in this definition.
Being more general means that the type class can be instantiated for a wider variety of types.

An example program that uses `MonadExcept`

is a simple division service.
The program is divided into two parts: a frontend that supplies a user interface based on strings that handles errors, and a backend that actually does the division.
Both the frontend and the backend can throw exceptions, the former for ill-formed input and the latter for division by zero errors.
The exceptions are an inductive type:

```
inductive Err where
| divByZero
| notANumber : String → Err
```

The backend checks for zero, and divides if it can:

```
def divBackend [Monad m] [MonadExcept Err m] (n k : Int) : m Int :=
if k == 0 then
throw .divByZero
else pure (n / k)
```

The frontend's helper `asNumber`

throws an exception if the string it is passed is not a number.
The overall frontend converts its inputs to `Int`

s and calls the backend, handling exceptions by returning a friendly string error:

```
def asNumber [Monad m] [MonadExcept Err m] (s : String) : m Int :=
match s.toInt? with
| none => throw (.notANumber s)
| some i => pure i
def divFrontend [Monad m] [MonadExcept Err m] (n k : String) : m String :=
tryCatch (do pure (toString (← divBackend (← asNumber n) (← asNumber k))))
fun
| .divByZero => pure "Division by zero!"
| .notANumber s => pure s!"Not a number: \"{s}\""
```

Throwing and catching exceptions is common enough that Lean provides a special syntax for using `MonadExcept`

.
Just as `+`

is short for `HAdd.hAdd`

, `try`

and `catch`

can be used as shorthand for the `tryCatch`

method:

```
def divFrontend [Monad m] [MonadExcept Err m] (n k : String) : m String :=
try
pure (toString (← divBackend (← asNumber n) (← asNumber k)))
catch
| .divByZero => pure "Division by zero!"
| .notANumber s => pure s!"Not a number: \"{s}\""
```

In addition to `Except`

and `ExceptT`

, there are useful `MonadExcept`

instances for other types that may not seem like exceptions at first glance.
For example, failure due to `Option`

can be seen as throwing an exception that contains no data whatsoever, so there is an instance of `MonadExcept Unit Option`

that allows `try ... catch ...`

syntax to be used with `Option`

.

## State

A simulation of mutable state is added to a monad by having monadic actions accept a starting state as an argument and return a final state together with their result. The bind operator for a state monad provides the final state of one action as an argument to the next action, threading the state through the program. This pattern can also be expressed as a monad transformer:

```
def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
σ → m (α × σ)
```

Once again, the monad instance is very similar to that for `State`

.
The only difference is that the input and output states are passed around and returned in the underlying monad, rather than with pure code:

```
instance [Monad m] : Monad (StateT σ m) where
pure x := fun s => pure (x, s)
bind result next := fun s => do
let (v, s') ← result s
next v s'
```

The corresponding type class has `get`

and `set`

methods.
One downside of `get`

and `set`

is that it becomes too easy to `set`

the wrong state when updating it.
This is because retrieving the state, updating it, and saving the updated state is a natural way to write some programs.
For example, the following program counts the number of diacritic-free English vowels and consonants in a string of letters:

```
structure LetterCounts where
vowels : Nat
consonants : Nat
deriving Repr
inductive Err where
| notALetter : Char → Err
deriving Repr
def vowels :=
let lowerVowels := "aeiuoy"
lowerVowels ++ lowerVowels.map (·.toUpper)
def consonants :=
let lowerConsonants := "bcdfghjklmnpqrstvwxz"
lowerConsonants ++ lowerConsonants.map (·.toUpper )
def countLetters (str : String) : StateT LetterCounts (Except Err) Unit :=
let rec loop (chars : List Char) := do
match chars with
| [] => pure ()
| c :: cs =>
let st ← get
let st' ←
if c.isAlpha then
if vowels.contains c then
pure {st with vowels := st.vowels + 1}
else if consonants.contains c then
pure {st with consonants := st.consonants + 1}
else -- modified or non-English letter
pure st
else throw (.notALetter c)
set st'
loop cs
loop str.toList
```

It would be very easy to write `set st`

instead of `set st'`

.
In a large program, this kind of mistake can lead to difficult-to-diagnose bugs.

While using a nested action for the call to `get`

would solve this problem, it can't solve all such problems.
For example, a function might update a field on a structure based on the values of two other fields.
This would require two separate nested-action calls to `get`

.
Because the Lean compiler contains optimizations that are only effective when there is a single reference to a value, duplicating the references to the state might lead to code that is significantly slower.
Both the potential performance problem and the potential bug can be worked around by using `modify`

, which transforms the state using a function:

```
def countLetters (str : String) : StateT LetterCounts (Except Err) Unit :=
let rec loop (chars : List Char) := do
match chars with
| [] => pure ()
| c :: cs =>
if c.isAlpha then
if vowels.contains c then
modify fun st => {st with vowels := st.vowels + 1}
else if consonants.contains c then
modify fun st => {st with consonants := st.consonants + 1}
else -- modified or non-English letter
pure ()
else throw (.notALetter c)
loop cs
loop str.toList
```

The type class contains a function akin to `modify`

called `modifyGet`

, which allows the function to both compute a return value and transform an old state in a single step.
The function returns a pair in which the first element is the return value, and the second element is the new state; `modify`

just adds the constructor of `Unit`

to the pair used in `modifyGet`

:

```
def modify [MonadState σ m] (f : σ → σ) : m Unit :=
modifyGet fun s => ((), f s)
```

The definition of `MonadState`

is as follows:

```
class MonadState (σ : outParam (Type u)) (m : Type u → Type v) : Type (max (u+1) v) where
get : m σ
set : σ → m PUnit
modifyGet : (σ → α × σ) → m α
```

`PUnit`

is a version of the `Unit`

type that is universe-polymorphic to allow it to be in `Type u`

instead of `Type`

.
While it would be possible to provide a default implementation of `modifyGet`

in terms of `get`

and `set`

, it would not admit the optimizations that make `modifyGet`

useful in the first place, rendering the method useless.

`Of`

Classes and `The`

Functions

Thus far, each monad type class that takes extra information, like the type of exceptions for `MonadExcept`

or the type of the state for `MonadState`

, has this type of extra information as an output parameter.
For simple programs, this is generally convenient, because a monad that combines one use each of `StateT`

, `ReaderT`

, and `ExceptT`

has only a single state type, environment type, and exception type.
As monads grow in complexity, however, they may involve multiple states or errors types.
In this case, the use of an output parameter makes it impossible to target both states in the same `do`

-block.

For these cases, there are additional type classes in which the extra information is not an output parameter.
These versions of the type classes use the word `Of`

in the name.
For example, `MonadStateOf`

is like `MonadState`

, but without an `outParam`

modifier.

Similarly, there are versions of the type class methods that accept the type of the extra information as an *explicit*, rather than implicit, argument.
For `MonadStateOf`

, there are `getThe`

with type

```
(σ : Type u) → {m : Type u → Type v} → [MonadStateOf σ m] → m σ
```

and `modifyThe`

with type

```
(σ : Type u) → {m : Type u → Type v} → [MonadStateOf σ m] → (σ → σ) → m PUnit
```

There is no `setThe`

because the type of the new state is enough to decide which surrounding state monad transformer to use.

In the Lean standard library, there are instances of the non-`Of`

versions of the classes defined in terms of the instances of the versions with `Of`

.
In other words, implementing the `Of`

version yields implementations of both.
It's generally a good idea to implement the `Of`

version, and then start writing programs using the non-`Of`

versions of the class, transitioning to the `Of`

version if the output parameter becomes inconvenient.

## Transformers and `Id`

The identity monad `Id`

is the monad that has no effects whatsoever, to be used in contexts that expect a monad for some reason but where none is actually necessary.
Another use of `Id`

is to serve as the bottom of a stack of monad transformers.
For instance, `StateT σ Id`

works just like `State σ`

.

## Exercises

### Monad Contract

Using pencil and paper, check that the rules of the monad transformer contract are satisfied for each monad transformer in this section.

### Logging Transformer

Define a monad transformer version of `WithLog`

.
Also define the corresponding type class `MonadWithLog`

, and write a program that combines logging and exceptions.

### Counting Files

Modify `doug`

's monad with `StateT`

such that it counts the number of directories and files seen.
At the end of execution, it should display a report like:

```
Viewed 38 files in 5 directories.
```