Lean4
LanguageTacticsCourse
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

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

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]

Counting

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

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

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.

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 MonadNext: Lake Build System