Module 5 · Lesson 3

Mutable State

Pure Lean code has no mutable variables. State is either threaded through functions with StateM or kept local to a do block with let mut.

Local Mutability with let mut

Inside do blocks, you can use let mutfor local mutable variables:

lean

Try it

1def sum (xs : List Nat) : Nat := Id.run do
2  let mut total := 0
3  for x in xs do
4    total := total + x
5  return total
6
7#eval sum [1, 2, 3, 4, 5]  -- 15

ℹ

Id.run runs a do block that uses mutability but has no other effects. The result is a pure value.

Common Patterns with let mut

Accumulators

A common use of mutable state is accumulating a result. Instead of threading an accumulator through recursive calls, you can update a mutable variable directly.

lean

Try it

1def factorial (n : Nat) : Nat := Id.run do
2  let mut result := 1
3  for i in [1:n+1] do
4    result := result * i
5  return result
6
7#eval factorial 5  -- 120

Building Collections

You can build up a collection by starting with an empty list and appending elements as you go. This is especially useful in for loops.

lean

Try it

1def evens (xs : List Nat) : List Nat := Id.run do
2  let mut result : List Nat := []
3  for x in xs do
4    if x % 2 == 0 then
5      result := result ++ [x]
6  return result
7
8#eval evens [1, 2, 3, 4, 5, 6]  -- [2, 4, 6]

Avoid Quadratic Appends

Repeatedly appending to the end of a list can be slow. Build with ::and reverse at the end when possible.

lean

Try it

1def evensFast (xs : List Nat) : List Nat := Id.run do
2  let mut acc : List Nat := []
3  for x in xs do
4    if x % 2 == 0 then
5      acc := x :: acc
6  return acc.reverse

Counting

Counting elements that satisfy a predicate is straightforward with a mutable counter. Increment whenever the condition holds.

lean

Try it

1def countWhere (p : α → Bool) (xs : List α) : Nat := Id.run do
2  let mut count := 0
3  for x in xs do
4    if p x then
5      count := count + 1
6  return count
7
8#eval countWhere (· > 3) [1, 5, 2, 7, 3, 8]  -- 3

The StateM Monad

For more structured state, use StateM:

lean

Try it

1-- StateM σ α: computation with state of type σ, returning α
2-- get: read the state
3-- set: write the state
4-- modify: transform the state
5
6def counter : StateM Nat Nat := do
7  let n ← get        -- Read current state
8  set (n + 1)        -- Update state
9  return n           -- Return old value
10
11-- Run with initial state
12#eval counter.run 0   -- (0, 1) -- returned 0, new state is 1
13#eval counter.run 10  -- (10, 11)

Multiple State Operations

lean

Try it

1def countUp : StateM Nat (List Nat) := do
2  let mut results := []
3  for _ in [0:5] do
4    let n ← get
5    results := results ++ [n]
6    modify (· + 1)
7  return results
8
9#eval countUp.run 0  -- ([0, 1, 2, 3, 4], 5)

Key Takeaway

StateM is explicit about state: you can see from the type that a function uses mutable state, unlike global variables in other languages.

State Operations

StateM provides a small set of core operations for reading and writing state. Combine them to build more complex stateful computations.

lean

Try it

1-- get: read state
2def readState : StateM String String := get
3
4-- set: replace state
5def writeState : StateM String Unit := set "new value"
6
7-- modify: transform state
8def appendState (s : String) : StateM String Unit :=
9  modify (· ++ s)
10
11-- modifyGet: modify and return value
12def pop : StateM (List α) (Option α) :=
13  modifyGet fun
14    | [] => (none, [])
15    | x :: xs => (some x, xs)

Complex State Types

When you need to track several related values, define a structure for your state. The with syntax makes updates ergonomic.

lean

Try it

1-- Use a structure for complex state
2structure GameState where
3  score : Nat
4  lives : Int
5  level : Nat
6  deriving Repr
7
8def addScore (points : Nat) : StateM GameState Unit :=
9  modify fun s => { s with score := s.score + points }
10
11def loseLife : StateM GameState Bool := do
12  modify fun s => { s with lives := s.lives - 1 }
13  let s ← get
14  return s.lives > 0
15
16def nextLevel : StateM GameState Unit :=
17  modify fun s => { s with level := s.level + 1 }
18
19def gameRound : StateM GameState String := do
20  addScore 100
21  let alive ← loseLife
22  if alive then
23    nextLevel
24    return "Continue"
25  else
26    return "Game Over"
27
28#eval gameRound.run ⟨0, 3, 1⟩  -- ("Continue", { score := 100, lives := 2, level := 2 })

let mut Inside IO

let mut is not tied to Id.run — it works in any do block, including IO:

lean

Try it

1def interactiveCounter : IO Unit := do
2  let mut count := 0
3  for _ in [0:3] do
4    IO.print s!"Count is {count}. Add how much? "
5    let input ← (← IO.getStdin).getLine
6    let n := input.trimAscii.toString.toNat!
7    count := count + n
8  IO.println s!"Final count: {count}"

⚠

let mut is not real mutation. The compiler rewrites the loop into a fold that threads the value through — which is why the variable cannot escape its do block, and why you cannot capture it in a closure and expect updates to be visible. When you genuinely need shared, aliasable state, you want a reference.

References: IO.Ref and ST.Ref

A reference is a real mutable cell on the heap. Unlike let mut, it can be passed to other functions, stored in a structure, and shared.

lean

Try it

1def useRef : IO Nat := do
2  let ref ← IO.mkRef 0       -- Create a reference
3  ref.modify (· + 10)        -- Modify it
4  ref.modify (· * 2)         -- Modify again
5  ref.get                    -- Read final value
6
7#eval useRef  -- 20
8
9-- The point of a Ref: another function can update YOUR cell
10def bump (r : IO.Ref Nat) : IO Unit := r.modify (· + 1)
11
12#eval show IO Nat from do
13  let r ← IO.mkRef 0
14  bump r
15  bump r
16  bump r
17  r.get                      -- 3

IO.Ref is ST.Ref specialised to IO. The ST monad is the interesting one: it gives you real mutation, and then runST hands you back a pure value, because the type system guarantees no reference escaped.

lean

Try it

1-- Genuinely mutable inside, genuinely pure outside.
2-- The σ is the "region" tag; annotating the ref's type keeps
3-- instance resolution un-stuck.
4def sumST (xs : List Nat) : Nat := runST fun σ => do
5  let acc : ST.Ref σ Nat ← ST.mkRef 0
6  for x in xs do
7    acc.modify (· + x)
8  acc.get
9
10#eval sumST [1, 2, 3, 4, 5]   -- 15
11
12-- Note the type: no IO, no monad. It is an ordinary Nat.
13#check sumST                  -- sumST (xs : List Nat) : Nat

💡

Pick in this order: foldl or recursion if it is natural; let mut + Id.run for a loop that reads imperatively; StateM when the state is threaded through many functions; ST/IO.Refonly when you need aliasing, or in-place updates for performance.

Purely Functional Alternatives

Often, you can avoid mutation entirely:

lean

Try it

1-- Mutable version
2def sumMut (xs : List Nat) : Nat := Id.run do
3  let mut total := 0
4  for x in xs do
5    total := total + x
6  return total
7
8-- Pure version with fold
9def sumPure (xs : List Nat) : Nat :=
10  xs.foldl (· + ·) 0
11
12-- Pure version with recursion
13def sumRec : List Nat → Nat
14  | [] => 0
15  | x :: xs => x + sumRec xs
16
17-- All produce the same result
18#eval sumMut [1, 2, 3, 4, 5]   -- 15
19#eval sumPure [1, 2, 3, 4, 5]  -- 15
20#eval sumRec [1, 2, 3, 4, 5]   -- 15

💡

Use mutable state when it's clearer (imperative algorithms) or more efficient. Use pure functions when they're simpler or when you need to reason about the code.

Exercise: Running Total

Build a list of running totals using let mut.

lean

Try it

1def runningTotals (xs : List Nat) : List Nat := Id.run do
2  let mut acc : List Nat := []
3  let mut total := 0
4  for x in xs do
5    total := total + x
6    acc := acc ++ [total]
7  return acc
8
9#eval runningTotals [1, 2, 3, 4]  -- [1, 3, 6, 10]

When to Use Each Approach

let mut + Id.run: Local mutation in otherwise pure code
let mut in IO: Mutation with I/O effects
StateM: When state is central to the computation
IO.mkRef: Shared mutable references
Pure recursion/fold: When mutation isn't needed

The IO Monad Next: Lake Build System