Lean 4 Monads, Applicatives, and Effect Type Classes

Lean 4 structures effectful computation through a hierarchy of type classes: Functor, Applicative, and Monad. These classes abstract over computational contexts — sequencing, failure, state, environment, and IO — so that the same code pattern works across many different effect types. Understanding this hierarchy lets you write generic effectful code and layer multiple effects cleanly.

The Type Class Hierarchy

Functor
  └── Applicative
        └── Monad

All three classes live in Init.Prelude and apply to a type constructor f : Type u → Type v.

`Functor`

Functor provides map (the <$> operator), which applies a pure function inside a computational context without affecting the context itself.

-- class Functor (f : Type u → Type v) where
--   map : (α → β) → f α → f β

#eval (· + 1) <$> [1, 2, 3]        -- [2, 3, 4]
#eval (· * 2) <$> (some 5)         -- some 10
#eval (· * 2) <$> (none : Option Nat) -- none

`Applicative`

Applicative adds pure (inject a value) and <*> (apply a wrapped function to a wrapped argument). Effects from both sides are sequenced.

-- class Applicative (f : ...) extends Functor f where
--   pure  : α → f α
--   seq   : f (α → β) → (Unit → f α) → f β   -- i.e., <*>

#eval pure 42 : Option Nat      -- some 42
#eval pure 42 : List Nat        -- [42]

-- <*> applies a function in a context to a value in a context
#eval (some (· + 10)) <*> (some 5)   -- some 15
#eval (none : Option (Nat → Nat)) <*> some 5  -- none

The <* and *> operators sequence effects while discarding one side’s value:

-- x <* y  runs x then y, returns x's value
-- x *> y  runs x then y, returns y's value
#eval (some 1) *> (some 2)    -- some 2
#eval (none : Option Nat) *> (some 2)  -- none

`Monad`

Monad adds bind (the >>= operator), which allows the result of one computation to determine the next computation. This is the key power of monads.

-- class Monad (m : ...) extends Applicative m where
--   bind : m α → (α → m β) → m β   -- i.e., >>=

-- Chaining Options
def safeSqrt (n : Float) : Option Float :=
  if n < 0 then none else some (Float.sqrt n)

#eval (some 16.0) >>= safeSqrt    -- some 4.0
#eval (some (-1.0)) >>= safeSqrt  -- none

-- >> sequences and discards left value
#eval (some 1) >> (some 2)   -- some 2

-- do notation is sugar for >>= chains
def chainExample : Option Nat := do
  let x ← some 3
  let y ← some 4
  return x * y    -- some 12

Common Monads

`Option` Monad

Option α represents a computation that may fail without a reason. A none at any point short-circuits the rest of the chain.

def safeDiv (n d : Nat) : Option Nat :=
  if d == 0 then none else some (n / d)

def compute (a b c : Nat) : Option Nat := do
  let x ← safeDiv a b
  let y ← safeDiv x c
  return y + 1

#eval compute 100 5 2    -- some 11
#eval compute 100 0 2    -- none  (b = 0)

`Except` Monad

Except ε α is like Option but carries an error value of type ε on failure.

inductive ParseError where
  | empty : ParseError
  | invalidChar : Char → ParseError
  deriving Repr

def parseDigit (c : Char) : Except ParseError Nat :=
  if c.isDigit then
    Except.ok (c.toNat - '0'.toNat)
  else
    Except.error (ParseError.invalidChar c)

def parseTwoDigits (s : String) : Except ParseError Nat := do
  let chars := s.toList
  match chars with
  | [a, b] =>
    let d1 ← parseDigit a
    let d2 ← parseDigit b
    return d1 * 10 + d2
  | _ => Except.error ParseError.empty

#eval parseTwoDigits "42"   -- Except.ok 42
#eval parseTwoDigits "4x"   -- Except.error (ParseError.invalidChar 'x')

`StateM` Monad

StateM σ α (a synonym for StateT σ Id α) is a computation that threads state of type σ, returning α.

-- Key operations:
-- get    : StateM σ σ         -- read the state
-- set    : σ → StateM σ Unit  -- replace the state
-- modify : (σ → σ) → StateM σ Unit

def counter : StateM Nat Nat := do
  let n ← get
  set (n + 1)
  return n

def runCounter : Nat × Nat :=
  counter.run 0    -- initial state = 0
  -- returns (value, finalState) = (0, 1)

#eval runCounter   -- (0, 1)

-- Multiple state accesses
def addAndDouble : StateM Nat Nat := do
  modify (· + 3)
  modify (· * 2)
  get

#eval addAndDouble.run 5   -- (16, 16)  (5+3=8, 8*2=16)

The IO Monad

IO α is the monad for programs with real-world side effects. It is defined as:

-- From Init/System/IO.lean:
-- abbrev IO : Type → Type := EIO IO.Error
-- def EIO (ε : Type) (α : Type) : Type := EST ε IO.RealWorld α
-- def BaseIO (α : Type) := ST IO.RealWorld α

The IO.RealWorld token is a compile-time fiction that threads through every IO action, enforcing sequential evaluation. In practice, you write do blocks and never see IO.RealWorld directly.

def main : IO Unit := do
  IO.println "Hello from IO!"
  let line ← IO.getLine
  IO.println s!"You said: {line.trim}"

`BaseIO` and `EIO`

Type	Errors	Use
`BaseIO α`	None	Always succeeds (e.g., `IO.getStdout`)
`EIO ε α`	Type `ε`	IO with typed errors
`IO α`	`IO.Error`	Standard IO

-- BaseIO cannot throw; IO can
def safeGetStdout : BaseIO IO.FS.Stream := IO.getStdout

-- EIO with a custom error type
def readConfig : EIO String String := do
  let contents ← (IO.FS.readFile "config.txt").toEIO
    (fun _ => "File not found")
  return contents

Monad Transformers

Monad transformers stack effects on top of an existing monad m.

`ReaderT`

ReaderT ρ m α is a computation in m α that has read-only access to an environment of type ρ.

structure Config where
  debug : Bool
  maxRetries : Nat

abbrev AppM := ReaderT Config IO

def logIfDebug (msg : String) : AppM Unit := do
  let cfg ← read
  if cfg.debug then
    IO.println s!"[DEBUG] {msg}"

def runApp : IO Unit :=
  logIfDebug "starting" |>.run { debug := true, maxRetries := 3 }

`StateT`

StateT σ m α adds mutable state of type σ on top of monad m.

abbrev Counter := StateT Nat IO

def increment : Counter Unit := modify (· + 1)

def getCount : Counter Nat := get

def runCounter : IO Unit := do
  let (_, finalCount) ← (do
    increment
    increment
    increment
    getCount).run 0
  IO.println s!"Final count: {finalCount}"

-- StateT.run returns m (α × σ); StateT.run' returns m α

`ExceptT`

ExceptT ε m α adds typed exceptions of type ε on top of monad m.

abbrev AppE α := ExceptT String IO α

def mustBePositive (n : Int) : AppE Nat := do
  if n ≤ 0 then
    throw s!"Expected positive, got {n}"
  return n.toNat

def runAppE : IO Unit := do
  let result ← (mustBePositive 5).run
  match result with
  | Except.ok n    => IO.println s!"Got: {n}"
  | Except.error e => IO.println s!"Error: {e}"

`pure`, `bind`, and Operators

Operator	Type	Meaning
`pure x`	`m α`	Inject `x` with no effect
`x >>= f`	`m β`	Bind: run `x`, pass result to `f`
`x >> y`	`m β`	Sequence: run `x`, discard, run `y`
`f <$> x`	`m β`	Map: apply pure `f` inside context
`mf <*> mx`	`m β`	Apply wrapped function to wrapped value

-- All equivalent ways to sequence Option computations:
example : Option Nat :=
  some 3 >>= fun x => some (x * 2)

example : Option Nat := do
  let x ← some 3
  return x * 2

example : Option Nat :=
  (· * 2) <$> some 3

Monad Lifting with `MonadLift`

MonadLift m n provides a way to run computations from monad m inside monad n. Lean inserts lifts automatically in do blocks.

-- class MonadLift (m : ...) (n : ...) where
--   monadLift : m α → n α

-- liftM is the explicit form
-- liftM : [MonadLiftT m n] → m α → n α

-- Automatic: IO actions are lifted into ReaderT Config IO
def example : ReaderT String IO Unit := do
  IO.println "This IO action is lifted automatically"
  let env ← read
  IO.println s!"Environment: {env}"

The transitive closure MonadLiftT means lifts compose: if m lifts to n and n lifts to k, then m lifts to k automatically.

Running Monadic Computations

-- StateT: run with initial state, returns (value, finalState)
#eval (do modify (· + 1); get : StateM Nat Nat).run 0
-- (1, 1)

-- StateT.run': run with initial state, discard final state
#eval (do modify (· + 10); get : StateM Nat Nat).run' 5
-- 15

-- ExceptT: run, unwrap to Except
#eval (do throw "oops"; return 42 : ExceptT String Id Nat).run
-- Except.error "oops"

-- ReaderT: run with an environment
#eval (do let r ← read; return r + 1 : ReaderT Nat Id Nat).run 10
-- 11

Lawful Monads

The LawfulMonad type class requires instances to satisfy the three monad laws:

Left identity: pure a >>= f = f a
Right identity: m >>= pure = m
Associativity: (m >>= f) >>= g = m >>= fun x => f x >>= g

Lean provides LawfulMonad instances for Option, Except, StateT, ReaderT, ExceptT, and IO. You can use these laws in proofs with simp [bind_pure_comp, pure_bind, bind_assoc].

Introduction

Language Basics

Theorem Proving

Functional Programming

Lean 4 Monads, Applicatives, and Effect Type Classes

The Type Class Hierarchy

`Functor`

`Applicative`

`Monad`

Common Monads

`Option` Monad

`Except` Monad

`StateM` Monad

The IO Monad

`BaseIO` and `EIO`

Monad Transformers

`ReaderT`

`StateT`

`ExceptT`

`pure`, `bind`, and Operators

Monad Lifting with `MonadLift`

Running Monadic Computations

Build docs developers (and LLMs) love

Introduction

Language Basics

Theorem Proving

Functional Programming

Documentation Index

​The Type Class Hierarchy

​Functor

​Applicative

​Monad

​Common Monads

​Option Monad

​Except Monad

​StateM Monad

​The IO Monad

​BaseIO and EIO

​Monad Transformers

​ReaderT

​StateT

​ExceptT

​pure, bind, and Operators

​Monad Lifting with MonadLift

​Running Monadic Computations

Build docs developers (and LLMs) love

The Type Class Hierarchy

`Functor`

`Applicative`

`Monad`

Common Monads

`Option` Monad

`Except` Monad

`StateM` Monad

The IO Monad

`BaseIO` and `EIO`

Monad Transformers

`ReaderT`

`StateT`

`ExceptT`

`pure`, `bind`, and Operators

Monad Lifting with `MonadLift`

Running Monadic Computations