Monad Transformers

In the previous sections you learned about some handy monads Option, IO, Reader, State and Except, and you now know how to make your function use one of these, but what you do not yet know is how to make your function use multiple monads at once.

For example, suppose you need a function that wants to access some Reader context and optionally throw an exception? This would require composition of two monads ReaderM and Except and this is what monad transformers are for.

A monad transformer is fundamentally a wrapper type. It is generally parameterized by another monadic type. You can then run actions from the inner monad, while adding your own customized behavior for combining actions in this new monad. The common transformers add T to the end of an existing monad name. You will find OptionT, ExceptT, ReaderT, StateT but there is no transformer for IO. So generally if you need IO it becomes the innermost wrapped monad.

In the following example we use ReaderT to provide some read only context to a function and this ReaderT transformer will wrap an Except monad. If all goes well the requiredArgument returns the value of a required argument and optionalSwitch returns true if the optional argument is present.

abbrev 
Arguments: Type
Arguments := 
List: Type → Type
List 
String: Type
String

def 
indexOf?: {α : Type u_1} → [inst : BEq α] → List α → α → optParam Nat 0 → Option Nat
indexOf? [
BEq: Type u_1 → Type u_1
BEq 
α: Type u_1
α] (
xs: List α
xs : 
List: Type u_1 → Type u_1
List 
α: Type u_1
α) (
s: α
s : 
α: Type u_1
α) (
start: optParam Nat 0
start := 
0: Nat
0): 
Option: Type → Type
Option 
Nat: Type
Nat :=
  match 
xs: List α
xs with
  | [] => 
none: {α : Type} → Option α
none
  | 
a: α
a :: 
tail: List α
tail => if 
a: α
a == 
s: α
s then 
some: {α : Type} → α → Option α
some 
start: optParam Nat 0
start else 
indexOf?: {α : Type u_1} → [inst : BEq α] → List α → α → optParam Nat 0 → Option Nat
indexOf? 
tail: List α
tail 
s: α
s (
start: optParam Nat 0
start+
1: Nat
1)

def 
requiredArgument: String → ReaderT Arguments (Except String) String
requiredArgument (
name: String
name : 
String: Type
String) : 
ReaderT: Type → (Type → Type) → Type → Type
ReaderT 
Arguments: Type
Arguments (
Except: Type → Type → Type
Except 
String: Type
String) 
String: Type
String := do
  let 
args: Arguments
args ← 
read: {ρ : outParam Type} → {m : Type → Type} → [self : MonadReader ρ m] → m ρ
read
  let 
value: String
value := match 
indexOf?: {α : Type} → [inst : BEq α] → List α → α → optParam Nat 0 → Option Nat
indexOf? 
args: Arguments
args 
name: String
name with
    | 
some: {α : Type ?u.836} → α → Option α
some 
i: Nat
i => if 
i: Nat
i + 
1: Nat
1 < 
args: Arguments
args.
length: {α : Type} → List α → Nat
length then 
args: Arguments
args[
i: Nat
i+
1: Nat
1]! else 
"": String
""
    | 
none: {α : Type ?u.1107} → Option α
none => 
"": String
""
  if 
value: String
value == 
"": String
"" then 
throw: {ε : outParam Type} → {m : Type → Type} → [self : MonadExcept ε m] → {α : Type} → ε → m α
throw
throw s!"Command line argument {name} missing": ReaderT Arguments (Except String) String
 
throw s!"Command line argument {name} missing": ReaderT Arguments (Except String) String
s!
throw s!"Command line argument {name} missing": ReaderT Arguments (Except String) String
"Command line argument {
name: String
name
throw s!"Command line argument {name} missing": ReaderT Arguments (Except String) String
} missing"
  return 
value: String
value

def 
optionalSwitch: String → ReaderT Arguments (Except String) Bool
optionalSwitch (
name: String
name : 
String: Type
String) : 
ReaderT: Type → (Type → Type) → Type → Type
ReaderT 
Arguments: Type
Arguments (
Except: Type → Type → Type
Except 
String: Type
String) 
Bool: Type
Bool := do
  let 
args: Arguments
args ← 
read: {ρ : outParam Type} → {m : Type → Type} → [self : MonadReader ρ m] → m ρ
read
  return match (
indexOf?: {α : Type} → [inst : BEq α] → List α → α → optParam Nat 0 → Option Nat
indexOf? 
args: Arguments
args 
name: String
name) with
  | 
some: {α : Type ?u.1665} → α → Option α
some _ => 
true: Bool
true
  | 
none: {α : Type ?u.1681} → Option α
none => 
false: Bool
false

#eval
Except.ok "foo" 
requiredArgument: String → ReaderT Arguments (Except String) String
requiredArgument 
"--input": String
"--input" |>.
run: {ρ : Type} → {m : Type → Type} → {α : Type} → ReaderT ρ m α → ρ → m α
run [
"--input": String
"--input", 
"foo": String
"foo"]
-- Except.ok "foo"

#eval
Except.error "Command line argument --input missing" 
requiredArgument: String → ReaderT Arguments (Except String) String
requiredArgument 
"--input": String
"--input" |>.
run: {ρ : Type} → {m : Type → Type} → {α : Type} → ReaderT ρ m α → ρ → m α
run [
"foo": String
"foo", 
"bar": String
"bar"]
-- Except.error "Command line argument --input missing"

#eval
Except.ok true 
optionalSwitch: String → ReaderT Arguments (Except String) Bool
optionalSwitch 
"--help": String
"--help" |>.
run: {ρ : Type} → {m : Type → Type} → {α : Type} → ReaderT ρ m α → ρ → m α
run [
"--help": String
"--help"]
-- Except.ok true

#eval
Except.ok false 
optionalSwitch: String → ReaderT Arguments (Except String) Bool
optionalSwitch 
"--help": String
"--help" |>.
run: {ρ : Type} → {m : Type → Type} → {α : Type} → ReaderT ρ m α → ρ → m α
run 
[]: List String
[]
-- Except.ok false

Notice that throw was available from the inner Except monad. The cool thing is you can switch this around and get the exact same result using ExceptT as the outer monad transformer and ReaderM as the wrapped monad. Try changing requiredArgument to ExceptT String (ReaderM Arguments) Bool.

Note: the |>. notation is described in Readers.

Adding more layers

Here's the best part about monad transformers. Since the result of a monad transformer is itself a monad, you can wrap it inside another transformer! Suppose you need to pass in some read only context like the command line arguments, update some read-write state (like program Config) and optionally throw an exception, then you could write this:

structure 
Config: Type
Config where
  
help: Config → Bool
help : 
Bool: Type
Bool := 
false: Bool
false
  
verbose: Config → Bool
verbose : 
Bool: Type
Bool := 
false: Bool
false
  
input: Config → String
input : 
String: Type
String := 
"": String
""
  deriving 
Repr: Type u → Type u
Repr

abbrev 
CliConfigM: Type → Type
CliConfigM := 
StateT: Type → (Type → Type) → Type → Type
StateT 
Config: Type
Config (
ReaderT: Type → (Type → Type) → Type → Type
ReaderT 
Arguments: Type
Arguments (
Except: Type → Type → Type
Except 
String: Type
String))

def 
parseArguments: CliConfigM Bool
parseArguments : 
CliConfigM: Type → Type
CliConfigM 
Bool: Type
Bool := do
  let mut 
config: Config
config ← 
get: {σ : outParam Type} → {m : Type → Type} → [self : MonadState σ m] → m σ
get
  if 
(← optionalSwitch "--help"): Bool
(← 
optionalSwitch: String → ReaderT Arguments (Except String) Bool
optionalSwitch
(← optionalSwitch "--help"): Bool
 
"--help": String
"--help"
(← optionalSwitch "--help"): Bool
) then
    
throw: {ε : outParam Type} → {m : Type → Type} → [self : MonadExcept ε m] → {α : Type} → ε → m α
throw 
"Usage: example [--help] [--verbose] [--input <input file>]": String
"Usage: example [--help] [--verbose] [--input <input file>]"
  
config: Config
config := { 
config: Config
config with
    verbose := 
(← optionalSwitch "--verbose"): Bool
(← 
optionalSwitch: String → ReaderT Arguments (Except String) Bool
optionalSwitch
(← optionalSwitch "--verbose"): Bool
 
"--verbose": String
"--verbose"
(← optionalSwitch "--verbose"): Bool
),
    input := 
(← requiredArgument "--input"): String
(← 
requiredArgument: String → ReaderT Arguments (Except String) String
requiredArgument
(← requiredArgument "--input"): String
 
"--input": String
"--input"
(← requiredArgument "--input"): String
) }
  
set: {σ : semiOutParam Type} → {m : Type → Type} → [self : MonadStateOf σ m] → σ → m PUnit
set 
config: Config
config
  return 
true: Bool
true

def 
main: List String → IO Unit
main (
args: List String
args : 
List: Type → Type
List 
String: Type
String) : 
IO: Type → Type
IO 
Unit: Type
Unit := do
  let 
config: Config
config : 
Config: Type
Config := { input := 
"default": String
"default"}
  match 
parseArguments: CliConfigM Bool
parseArguments |>.
run: {σ : Type} → {m : Type → Type} → {α : Type} → StateT σ m α → σ → m (α × σ)
run 
config: Config
config |>.
run: {ρ : Type} → {m : Type → Type} → {α : Type} → ReaderT ρ m α → ρ → m α
run 
args: List String
args with
  | 
Except.ok: {ε : Type ?u.5364} → {α : Type ?u.5363} → α → Except ε α
Except.ok (_, 
c: Config
c) => do
    
IO.println: {α : Type} → [inst : ToString α] → α → IO Unit
IO.println s!"Processing input '{
c: Config
c.
input: Config → String
input}' with verbose={
c: Config
c.
verbose: Config → Bool
verbose}"
  | 
Except.error: {ε : Type ?u.5603} → {α : Type ?u.5602} → ε → Except ε α
Except.error 
s: String
s => 
IO.println: {α : Type} → [inst : ToString α] → α → IO Unit
IO.println 
s: String
s


#eval
Usage: example [--help] [--verbose] [--input <input file>]
 
main: List String → IO Unit
main [
"--help": String
"--help"]
-- Usage: example [--help] [--verbose] [--input <input file>]

#eval
Processing input 'foo' with verbose=false
 
main: List String → IO Unit
main [
"--input": String
"--input", 
"foo": String
"foo"]
-- Processing input file 'foo' with verbose=false

#eval
Processing input 'bar' with verbose=true
 
main: List String → IO Unit
main [
"--verbose": String
"--verbose", 
"--input": String
"--input", 
"bar": String
"bar"]
-- Processing input 'bar' with verbose=true

In this example parseArguments is actually three stacked monads, StateM, ReaderM, Except. Notice the convention of abbreviating long monadic types with an alias like CliConfigM.

Monad Lifting

Lean makes it easy to compose functions that use different monads using a concept of automatic monad lifting. You already used lifting in the above code, because you were able to compose optionalSwitch which has type ReaderT Arguments (Except String) Bool and call it from parseArguments which has a bigger type StateT Config (ReaderT Arguments (Except String)). This "just worked" because Lean did some magic with monad lifting.

To give you a simpler example of this, suppose you have the following function:

def 
divide: Float → Float → ExceptT String Id Float
divide (
x: Float
x : 
Float: Type
Float ) (
y: Float
y : 
Float: Type
Float): 
ExceptT: Type → (Type → Type) → Type → Type
ExceptT 
String: Type
String 
Id: Type → Type
Id 
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.000000 
divide: Float → Float → ExceptT String Id Float
divide 
6: Float
6 
3: Float
3 -- Except.ok 2.000000
#eval
Except.error "can't divide by zero" 
divide: Float → Float → ExceptT String Id Float
divide 
1: Float
1 
0: Float
0 -- Except.error "can't divide by zero"

Notice here we used the ExceptT transformer, but we composed it with the Id identity monad. This is then the same as writing Except String Float since the identity monad does nothing.

Now suppose you want to count the number of times divide is called and store the result in some global state:

def 
divideCounter: Float → Float → StateT Nat (ExceptT String Id) Float
divideCounter (
x: Float
x : 
Float: Type
Float) (
y: Float
y : 
Float: Type
Float) : 
StateT: Type → (Type → Type) → Type → Type
StateT 
Nat: Type
Nat (
ExceptT: Type → (Type → Type) → Type → Type
ExceptT 
String: Type
String 
Id: Type → Type
Id) 
Float: Type
Float := do
  
modify: {σ : Type} → {m : Type → Type} → [inst : MonadState σ m] → (σ → σ) → m PUnit
modify fun 
s: Nat
s => 
s: Nat
s + 
1: Nat
1
  
divide: Float → Float → ExceptT String Id Float
divide 
x: Float
x 
y: Float
y

#eval
Except.ok (2.000000, 1) 
divideCounter: Float → Float → StateT Nat (ExceptT String Id) Float
divideCounter 
6: Float
6 
3: Float
3 |>.
run: {σ : Type} → {m : Type → Type} → {α : Type} → StateT σ m α → σ → m (α × σ)
run 
0: Nat
0    -- Except.ok (2.000000, 1)
#eval
Except.error "can't divide by zero" 
divideCounter: Float → Float → StateT Nat (ExceptT String Id) Float
divideCounter 
1: Float
1 
0: Float
0 |>.
run: {σ : Type} → {m : Type → Type} → {α : Type} → StateT σ m α → σ → m (α × σ)
run 
0: Nat
0    -- Except.error "can't divide by zero"

The modify function is a helper which makes it easier to use modifyGet from the StateM monad. But something interesting is happening here, divideCounter is returning the value of divide, but the types don't match, yet it works? This is monad lifting in action.

You can see this more clearly with the following test:

def 
liftTest: Except String Float → StateT Nat (Except String) Float
liftTest (
x: Except String Float
x : 
Except: Type → Type → Type
Except 
String: Type
String 
Float: Type
Float) :
  
StateT: Type → (Type → Type) → Type → Type
StateT 
Nat: Type
Nat (
Except: Type → Type → Type
Except 
String: Type
String) 
Float: Type
Float := 
x: Except String Float
x

#eval
Except.ok (5.000000, 3) 
liftTest: Except String Float → StateT Nat (Except String) Float
liftTest (
divide: Float → Float → ExceptT String Id Float
divide 
5: Float
5 
1: Float
1) |>.
run: {σ : Type} → {m : Type → Type} → {α : Type} → StateT σ m α → σ → m (α × σ)
run 
3: Nat
3 -- Except.ok (5.000000, 3)

Notice that liftTest returned x without doing anything to it, yet that matched the return type StateT Nat (Except String) Float. Monad lifting is provided by monad transformers. if you #print liftTest you will see that Lean is implementing this using a call to a function named monadLift from the MonadLift type class:

class MonadLift (m : Type u → Type v) (n : Type u → Type w) where
  monadLift : {α : Type u} → m α → n α

So monadLift is a function for lifting a computation from an inner Monad m α to an outer Monad n α. You could replace x in liftTest with monadLift x if you want to be explicit about it.

The StateT monad transformer defines an instance of MonadLift like this:

@[inline] protected def lift {α : Type u} (t : m α) : StateT σ m α :=
  fun s => do let a ← t; pure (a, s)

instance : MonadLift m (StateT σ m) := ⟨StateT.lift⟩

This means that any monad m can be wrapped in a StateT monad by using the function fun s => do let a ← t; pure (a, s) that takes state s, runs the inner monad action t, and returns the result and the new state in a pair (a, s) without making any changes to s.

Because MonadLift is a type class, Lean can automatically find the required monadLift instances in order to make your code compile and in this way it was able to find the StateT.lift function and use it to wrap the result of divide so that the correct type is returned from divideCounter.

If you have an instance MonadLift m n that means there is a way to turn a computation that happens inside of m into one that happens inside of n and (this is the key part) usually without the instance itself creating any additional data that feeds into the computation. This means you can in principle declare lifting instances from any monad to any other monad, it does not, however, mean that you should do this in all cases. You can get a very nice report on how all this was done by adding the line set_option trace.Meta.synthInstance true in before divideCounter and moving you cursor to the end of the first line after do.

This was a lot of detail, but it is very important to understand how monad lifting works because it is used heavily in Lean programs.

Transitive lifting

There is also a transitive version of MonadLift called MonadLiftT which can lift multiple monad layers at once. In the following example we added another monad layer with ReaderT String ... and notice that x is also automatically lifted to match.

def 
liftTest2: Except String Float → ReaderT String (StateT Nat (Except String)) Float
liftTest2 (
x: Except String Float
x : 
Except: Type → Type → Type
Except 
String: Type
String 
Float: Type
Float) :
  
ReaderT: Type → (Type → Type) → Type → Type
ReaderT 
String: Type
String (
StateT: Type → (Type → Type) → Type → Type
StateT 
Nat: Type
Nat (
Except: Type → Type → Type
Except 
String: Type
String)) 
Float: Type
Float := 
x: Except String Float
x

#eval
Except.ok (5.000000, 3) 
liftTest2: Except String Float → ReaderT String (StateT Nat (Except String)) Float
liftTest2 (
divide: Float → Float → ExceptT String Id Float
divide 
5: Float
5 
1: Float
1) |>.
run: {ρ : Type} → {m : Type → Type} → {α : Type} → ReaderT ρ m α → ρ → m α
run 
"": String
"" |>.
run: {σ : Type} → {m : Type → Type} → {α : Type} → StateT σ m α → σ → m (α × σ)
run 
3: Nat
3
-- Except.ok (5.000000, 3)

The ReaderT monadLift is even simpler than the one for StateT:

instance  : MonadLift m (ReaderT ρ m) where
  monadLift x := fun _ => x

This lift operation creates a function that defines the required ReaderT input argument, but the inner monad doesn't know or care about ReaderT so the monadLift function throws it away with the _ then calls the inner monad action x. This is a perfectly legal implementation of the ReaderM monad.

Add your own Custom MonadLift

This does not compile:

def 
main2: IO Unit
main2 : 
IO: Type → Type
IO 
Unit: Type
Unit := do
  try
    let 
ret: ?m.8410
ret ← 
divideCounter: Float → Float → StateT Nat (ExceptT String Id) Float
divideCounter 
5: Float
5 
2: Float
2 |>.
run: {σ : Type} → {m : Type → Type} → {α : Type} → StateT σ m α → σ → m (α × σ)
run 
0: Nat
0
Error: type mismatch
  (divideCounter 5 2).run 0
has type
  ExceptT String Id (Float × Nat) : Type
but is expected to have type
  IO ?m.8441 : Type
    
IO.println: {α : Type} → [inst : ToString α] → α → IO Unit
IO.println (
toString: {α : Type} → [self : ToString α] → α → String
toString 
ret: ?m.8410
ret)
  catch 
e: IO.Error
e =>
    
IO.println: {α : Type} → [inst : ToString α] → α → IO Unit
IO.println 
e: IO.Error
e

saying:

typeclass instance problem is stuck, it is often due to metavariables
  ToString ?m.4786

The reason is divideCounter returns the big StateT Nat (ExceptT String Id) Float and that type cannot be automatically lifted into the main return type of IO Unit unless you give it some help.

The following custom MonadLift solves this problem:

def 
liftIO: {α : Type} → ExceptT String Id α → IO α
liftIO (
t: ExceptT String Id α
t : 
ExceptT: Type → (Type → Type) → Type → Type
ExceptT 
String: Type
String 
Id: Type → Type
Id 
α: Type
α) : 
IO: Type → Type
IO 
α: Type
α := do
  match 
t: ExceptT String Id α
t with
  | 
.ok: {ε α : Type} → α → Except ε α
.ok 
r: α
r => 
EStateM.Result.ok: {ε σ α : Type} → α → σ → EStateM.Result ε σ α
EStateM.Result.ok 
r: α
r
  | 
.error: {ε α : Type} → ε → Except ε α
.error 
s: String
s => 
EStateM.Result.error: {ε σ α : Type} → ε → σ → EStateM.Result ε σ α
EStateM.Result.error 
s: String
s

instance: MonadLift (ExceptT String Id) IO
instance : 
MonadLift: semiOutParam (Type → Type) → (Type → Type) → Type 1
MonadLift (
ExceptT: Type → (Type → Type) → Type → Type
ExceptT 
String: Type
String 
Id: Type → Type
Id) 
IO: Type → Type
IO where
  monadLift := 
liftIO: {α : Type} → ExceptT String Id α → IO α
liftIO

def 
main3: IO Unit
main3 : 
IO: Type → Type
IO 
Unit: Type
Unit := do
  try
    let 
ret: Float × Nat
ret ← 
divideCounter: Float → Float → StateT Nat (ExceptT String Id) Float
divideCounter 
5: Float
5 
2: Float
2 |>.
run: {σ : Type} → {m : Type → Type} → {α : Type} → StateT σ m α → σ → m (α × σ)
run 
0: Nat
0
    
IO.println: {α : Type} → [inst : ToString α] → α → IO Unit
IO.println (
toString: {α : Type} → [self : ToString α] → α → String
toString 
ret: Float × Nat
ret)
  catch 
e: IO.Error
e =>
    
IO.println: {α : Type} → [inst : ToString α] → α → IO Unit
IO.println 
e: IO.Error
e

#eval
(2.500000, 1)
 
main3: IO Unit
main3 -- (2.500000, 1)

It turns out that the IO monad you see in your main function is based on the EStateM.Result type which is similar to the Except type but it has an additional return value. The liftIO function converts any Except String α into IO α by simply mapping the ok case of the Except to the Result.ok and the error case to the Result.error.

Lifting ExceptT

In the previous Except section you saw functions that throw Except values. When you get all the way back up to your main function which has type IO Unit you have the same problem you had above, because Except String Float doesn't match even if you use a try/catch.

def 
main4: IO Unit
main4 : 
IO: Type → Type
IO 
Unit: Type
Unit := do
  try
    let 
ret: Float
ret ← 
divide: Float → Float → ExceptT String Id Float
divide 
5: Float
5 
0: Float
0
    
IO.println: {α : Type} → [inst : ToString α] → α → IO Unit
IO.println (
toString: {α : Type} → [self : ToString α] → α → String
toString 
ret: Float
ret)  -- lifting happens here.
  catch 
e: IO.Error
e =>
    
IO.println: {α : Type} → [inst : ToString α] → α → IO Unit
IO.println s!"Unhandled exception: {
e: IO.Error
e}"

#eval
Unhandled exception: can't divide by zero
 
main4: IO Unit
main4 -- Unhandled exception: can't divide by zero

Without the liftIO the (toString ret) expression would not compile with a similar error:

typeclass instance problem is stuck, it is often due to metavariables
  ToString ?m.6007

So the general lesson is that if you see an error like this when using monads, check for a missing MonadLift.

Summary

Now that you know how to combine your monads together, you're almost done with understanding the key concepts of monads! You could probably go out now and start writing some pretty nice code! But to truly master monads, you should know how to make your own, and there's one final concept that you should understand for that. This is the idea of type "laws". Each of the structures you've learned so far has a series of laws associated with it. And for your instances of these classes to make sense, they should follow the laws! Check out Monad Laws.