Module 5 · Lesson 3

Mutable State

Lean provides controlled mutation through StateM and local mutability with let mut—no global mutable state.

Local Mutability with let mut

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

lean

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

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

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

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

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

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

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

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

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

IO with State

Use ST for mutation within IO:

lean

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.getLine
6    let n := input.trim.toNat!
7    count := count + n
8  IO.println s!"Final count: {count}"

Deep Dive: References and ST

For heap-allocated mutable references, Lean provides ST.Ref:

lean

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

References are useful when you need to share mutable state across different parts of your code.

Purely Functional Alternatives

Often, you can avoid mutation entirely:

lean

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

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