These are notes for Chapter 4.2: The Monad Type Class from Functional Programming in Lean.

All code for this post can be found at monad-typeclass.lean.

It builds on the first post (where we defined bind and unit from scratch) and the second post (where we wrote them four times for Option, Error, WithLog, and State). Each type had a fair amount of overlap in logic — which indicates that they can be grouped to be instances of the Monad type class. This is akin to traits in Rust — each type must implement the trait's functions. See the type class notes for more on how type classes work in Lean.

The Type Class

Rather than having to import ok or andThen for each type that is a monad, Lean has a type class that overloads them — so the same operators work for any monad. The simplified definition:

class Monad (m : Type → Type) where
  pure : α → m α
  bind : m α → (α → m β) → m β
  • pure — our unit/ok (the lifter)
  • bind — our andThen (the composer)

The actual definition in Lean is more involved (it inherits from Functor and Applicative, which add map and other operations). We'll get to that later.

Any type m : Type → Type1 that provides pure and bind can be registered as a Monad. From our previous posts, m was Option, Except ε, WithLog logged, State σ, etc.

1

Monad requires m : Type → Type. Except has two type parameters (Except ε α), so Except alone is Type → Type → Type — wrong kind. You fix ε to get Except ε : Type → Type. For example, Monad (Except String) works but Monad Except doesn't.

Instances

The Monad instances for Option and Except ε are just our andThen/unit definitions from the previous post, registered as a type class:

Option — pure is some (our unit), bind is andThen:

instance : Monad Option where
  pure x := some x              -- pure : α → Option α
  bind opt next :=               -- bind : Option α → (α → Option β) → Option β
    match opt with
    | none => none
    | some x => next x

Except — pure is Except.ok (our unit), bind is andThenError:

instance : Monad (Except ε) where
  pure x := Except.ok x         -- pure : α → Except ε α
  bind attempt next :=           -- bind : Except ε α → (α → Except ε β) → Except ε β
    match attempt with
    | Except.error e => Except.error e
    | Except.ok x => next x

Exactly the same code as before — just wrapped in instance : Monad ....

The Payoff: Polymorphic Code

In the previous post we wrote firstThird separately for Option and Error. Now we can write it once for any monad. The infix >>= is bind (same role as our ~~>):

def firstThirdFifthSeventh [Monad m]
    (lookup : List α → Nat → m α)
    (xs : List α) : m (α × α × α × α) :=
  lookup xs 0 >>= fun first =>
  lookup xs 2 >>= fun third =>
  lookup xs 4 >>= fun fifth =>
  lookup xs 6 >>= fun seventh =>
  pure (first, third, fifth, seventh)

>>= is just syntactic sugar for Bind.bind, and pure for Pure.pure. Without the sugar, the same function looks like:

def firstThirdFifthSeventh' [Monad m]
    (lookup : List α → Nat → m α)
    (xs : List α) : m (α × α × α × α) :=
  Bind.bind (lookup xs 0) (fun first =>
  Bind.bind (lookup xs 2) (fun third =>
  Bind.bind (lookup xs 4) (fun fifth =>
  Bind.bind (lookup xs 6) (fun seventh =>
  Pure.pure (first, third, fifth, seventh)))))

Bind.bind and Pure.pure are the functions we registered in the instance2. When m = Option, Lean looks up the Monad Option instance and calls the bind and pure we defined there. When m = Except String, it finds the Monad (Except ε) instance instead.

2

It might seem confusing that we write Pure.pure and Bind.bind when these are methods of Monad. Here's roughly what's going on: Lean's Monad doesn't directly own pure and bind — it inherits them from separate type classes (Pure owns pure, Bind owns bind). The hierarchy is Pure → Applicative → Monad ← Bind. When you write instance : Monad Option, Lean registers both Pure.pure and Bind.bind for Option. This is an internal detail we'll discuss later — the simplified definition with pure and bind directly in Monad is the right mental model for now.

[Monad m] says "this works for any m that is a monad" — both Option and Except qualify. Which one do we use? Lean infers m from the lookup function you pass in. If lookup returns Option α, then m = Option. If it returns Except String α, then m = Except String.

Given some example data:

def slowMammals : List String :=
  ["Three-toed sloth", "Slow loris"]

def fastBirds : List String := [
  "Peregrine falcon",
  "Saker falcon",
  "Golden eagle",
  "Gray-headed albatross",
  "Spur-winged goose",
  "Swift",
  "Anna's hummingbird"
]

We define two lookup functions — they do the same thing (get element at index) but return different monads:

-- Returns Option α — silent failure
def lookupSilent (xs : List α) (i : Nat) : Option α :=
  xs[i]?

-- Returns Except String α — failure with error message
def lookupVerbose (xs : List α) (i : Nat) : Except String α :=
  match xs[i]? with
  | none => Except.error s!"Index {i} not found (maximum is {xs.length - 1})"
  | some x => Except.ok x

Now pass each one into the same firstThirdFifthSeventh. The lookup's return type determines which monad m becomes:

-- lookupSilent returns Option α, so m = Option
#eval firstThirdFifthSeventh lookupSilent slowMammals
-- none

#eval firstThirdFifthSeventh lookupSilent fastBirds
-- some ("Peregrine falcon", "Golden eagle", "Spur-winged goose", "Anna's hummingbird")

-- lookupVerbose returns Except String α, so m = Except String
#eval firstThirdFifthSeventh lookupVerbose slowMammals
-- Except.error "Index 2 not found (maximum is 1)"

#eval firstThirdFifthSeventh lookupVerbose fastBirds
-- Except.ok ("Peregrine falcon", "Golden eagle", "Spur-winged goose", "Anna's hummingbird")

One function, two behaviours. Swap the lookup, swap the monad.

mapM: How Powerful This Gets

Because many types are monads, functions polymorphic over any monad are very general. mapM is a version of List.map where the function applied to each element returns a monadic type (e.g. Option β or Except String β instead of plain β), and mapM uses bind to sequence the results and handle the side effects:

def mapM' [Monad m] (f : α → m β) : List α → m (List β)
  | [] => pure []
  | x :: xs =>
    f x >>= fun hd =>
    mapM' f xs >>= fun tl =>
    pure (hd :: tl)
Aside: List.map without sugar

:: is sugar for List.cons and [] is sugar for List.nil. The same symbol does double duty: on the left of => it destructures (splits head from tail), on the right it constructs (puts an element at the front).

Here's map without any sugar:

def map (f : α → β) : List α → List β
  | List.nil => List.nil
  | List.cons x xs => List.cons (f x) (map f xs)

With sugar it's the same thing:

def map (f : α → β) : List α → List β
  | [] => []
  | x :: xs => f x :: map f xs

In map, f returns a plain β. In mapM', f returns m β — a β wrapped in a monad. So f x doesn't give us β directly; we need bind to extract it.

Line by line:

  • | [] => pure [] — empty list: return an empty list, lifted into the monad with pure
  • f x — apply f to the head. This gives us m β, not β
  • >>= fun hd => — bind: extract the β from m β, call it hd
  • mapM' f xs — recurse on the tail. This gives us m (List β)
  • >>= fun tl => — bind: extract the List β, call it tl
  • pure (hd :: tl) — cons hd onto tl, wrap the result in the monad with pure

Every step that could have a side effect (calling f, recursing) goes through bind. bind handles the side effect — if f x returns none, bind short-circuits and the whole thing is none. If f x returns Except.error, same thing.

The return type of f determines which Monad instance gets used. Same mapM', completely different behaviour depending on what f returns:

With Option — if any element fails, the whole thing fails:

#eval mapM' (fun x => if x > 0 then some x else none) [1, 2, 3]
-- some [1, 2, 3]

#eval mapM' (fun x => if x > 0 then some x else none) [1, 0, 3]
-- none

With Except — if any element fails, you get an error message saying which one:

#eval mapM' (fun x => if x > 0 then Except.ok x
             else Except.error s!"{x} is not positive") [1, 2, 3]
-- Except.ok [1, 2, 3]

#eval mapM' (fun x => if x > 0 then Except.ok x
             else Except.error s!"{x} is not positive") [1, 0, 3]
-- Except.error "0 is not positive"

We wrote mapM' once. It works with Option, Except, State, WithLog — any monad. The function f controls which effects are available, and the type system enforces it.

The Monad Contract

Every Monad instance should obey three laws:

1. Left identity: bind (pure v) f should be the same as f v

pure then bind is the same as just calling f:

Option:  bind (some 5) (fun x => some (x + 1))  =  some 6  =  (fun x => some (x + 1)) 5    -- ok
Except:  bind (Except.ok 5) (fun x => Except.ok (x + 1))  =  Except.ok 6                    -- ok

This makes sense because the problem all along in our original post was that f takes type α not m α. What bind does is act as a router — stripping away the monadic wrapper and feeding f the correct input.

2. Right identity: bind v pure should be the same as v (where v : m α, not plain α — bind always takes a monadic value as its first argument)

bind unwraps v, passes the inner value to pure, which wraps it again. Net result: same as v:

Option:  bind (some 5) some      =  some 5     -- ok
Option:  bind none some          =  none        -- ok
Except:  bind (Except.ok 5) Except.ok    =  Except.ok 5              -- ok
Except:  bind (Except.error "bad") Except.ok  =  Except.error "bad"  -- ok

3. Associativity: bind (bind v f) g should be the same as bind v (fun x => bind (f x) g)

Chaining order doesn't matter — so long as the sequence is preserved:

let f := fun x => some (x + 1)
let g := fun x => some (x * 2)

Option:  bind (bind (some 3) f) g  =  bind (some 4) g  =  some 8
         bind (some 3) (fun x => bind (f x) g)  =  bind (some 3) (fun x => bind (some (x+1)) g)
                                                  =  bind (some 3) (fun x => some ((x+1)*2))
                                                  =  some 8                                       -- ok

Since pure has no effects, sequencing it with bind shouldn't change the result — that's what the first two laws say. The third says that the sequencing bookkeeping itself doesn't matter, so long as the order in which things happen is preserved.

These laws are not enforced by the compiler. A broken example: instance : Monad Option where pure x := some x; bind _ _ := none. This satisfies the types but violates left identity — bind (pure v) f gives none instead of f v. The monad laws are a contract you must uphold.

References