lean-fp-transformers

name: lean-fp-transformers description: Combining multiple effects with monad transformers including StateT, ExceptT, ReaderT, and OptionT. Use when you need error handling AND state, or multiple effects together. allowed-tools: Read, Grep, Glob

Lean 4 Monad Transformers

Combining multiple effects with monad transformers. Use when you need both error handling AND state, or multiple effects together.

Trigger terms: "monad transformer", "StateT", "ExceptT", "ReaderT", "OptionT", "lift", "stack"

The Problem

Need both state AND error handling:

-- Can't use State AND Except separately
-- Need to combine them!

OptionT

Add optionality to any monad:

def OptionT (m : Type → Type) (α : Type) := m (Option α)

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

ExceptT

Add exceptions to any monad:

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

instance [Monad m] : Monad (ExceptT ε m) where
  pure x := pure (Except.ok x)
  bind x f := do
    match ← x with
    | Except.error e => pure (Except.error e)
    | Except.ok v => f v

-- Throw and catch
def throw (e : ε) : ExceptT ε m α := pure (Except.error e)
def tryCatch (x : ExceptT ε m α) (handle : ε → ExceptT ε m α) : ExceptT ε m α

StateT

Add state to any monad:

def StateT (σ : Type) (m : Type → Type) (α : Type) := σ → m (α × σ)

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

-- State operations
def get : StateT σ m σ := fun s => pure (s, s)
def set (s : σ) : StateT σ m Unit := fun _ => pure ((), s)
def modify (f : σ → σ) : StateT σ m Unit := fun s => pure ((), f s)

MonadLift

Lift base monad operations:

class MonadLift (m n : Type → Type) where
  monadLift : m α → n α

-- Automatic lifting with liftM
def liftM [MonadLift m n] (x : m α) : n α := MonadLift.monadLift x

Stacking Order Matters!

-- ExceptT outside StateT: error discards state changes
ExceptT String (StateT Nat Id) α

-- StateT outside ExceptT: state persists across errors
StateT Nat (ExceptT String Id) α

Decision guide:

Should errors:
├─ Discard state changes? → ExceptT (StateT ...)
└─ Preserve state? → StateT (ExceptT ...)

Type Class Effects

Use type classes for effect operations:

class MonadState (σ : Type) (m : Type → Type) where
  get : m σ
  set : σ → m Unit

class MonadExcept (ε : Type) (m : Type → Type) where
  throw : ε → m α
  tryCatch : m α → (ε → m α) → m α

-- Generic code works with any stack providing these effects
def increment [Monad m] [MonadState Nat m] : m Unit := do
  let n ← MonadState.get
  MonadState.set (n + 1)

Common Stack Patterns

Need	Stack
State + Errors (errors reset state)	`ExceptT ε (StateT σ m)`
State + Errors (state persists)	`StateT σ (ExceptT ε m)`
Config + State	`ReaderT ρ (StateT σ m)`
Config + Errors	`ReaderT ρ (ExceptT ε m)`
All three	`ReaderT ρ (ExceptT ε (StateT σ m))`

Common Mistakes

Wrong stacking order:

-- ❌ Unexpected behavior
-- ExceptT (StateT ...) vs StateT (ExceptT ...)
-- These behave DIFFERENTLY on errors!

-- ✓ Think about: what happens to state when error occurs?

Forgetting to lift:

-- ❌ Type error in nested monad
def f : StateT Nat (ExceptT String Id) Unit := do
  throw "error"  -- Won't work without lift!

-- ✓ Use MonadExcept or explicit lift
def f : StateT Nat (ExceptT String Id) Unit := do
  MonadExcept.throw "error"