15.4. Mutable References

While ordinary state monads encode stateful computations with tuples that track the contents of the state along with the computation's value, Lean's runtime system also provides mutable references that are always backed by mutable memory cells. Mutable references have a type IO.Ref that indicates that a cell is mutable, and reads and writes must be explicit. IO.Ref is implemented using ST.Ref, so the entire ST.Ref API may also be used with IO.Ref.

def

IO.Ref (α : Type) : Type

Mutable reference cells that contain values of type α. These cells can read from and mutated in the IO monad.

def

IO.mkRef {α : Type} (a : α) : BaseIO (IO.Ref α)

Creates a new mutable reference cell that contains a.

15.4.1. State Transformers🔗

Mutable references are often useful in contexts where arbitrary side effects are undesired. They can give a significant speedup when Lean is unable to optimize pure operations into mutation, and some algorithms are more easily expressed using mutable references than with state monads. Additionally, it has a property that other side effects do not have: if all of the mutable references used by a piece of code are created during its execution, and no mutable references from the code escape to other code, then the result of evaluation is deterministic.

The ST monad is a restricted version of IO in which mutable state is the only side effect, and mutable references cannot escape.ST was first described by John Launchbury and Simon L Peyton Jones, 1994. “Lazy functional state threads”. In Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation.. ST takes a type parameter that is never used to classify any terms. The runST function, which allow escape from ST, requires that the ST action that is passed to it can instantiate this type parameter with any type. This unknown type does not exist except as a parameter to a function, which means that values whose types are “marked” by it cannot escape its scope.

def

ST (σ : Type) : Type → Type

A restricted version of IO in which mutable state is the only side effect.

It is possible to run ST computations in a non-monadic context using runST.

def

runST {α : Type} (x : (σ : Type) → ST σ α) : α

Runs an ST computation, in which mutable state via ST.Ref is the only side effect.

As with IO and EIO, there is also a variation of ST that takes a custom error type as a parameter. Here, ST is analogous to BaseIO rather than IO, because ST cannot result in errors being thrown.

def

EST (ε σ : Type) : Type → Type

A restricted version of IO in which mutable state and exceptions are the only side effects.

It is possible to run EST computations in a non-monadic context using runEST.

def

runEST {ε α : Type}
  (x : (σ : Type) → EST ε σ α) : Except ε α

Runs an EST computation, in which mutable state and exceptions are the only side effects.

structure

ST.Ref (σ α : Type) : Type

Mutable reference cells that contain values of type α. These cells can read from and mutated in the ST σ monad.

Constructor

ST.Ref.mk

def

ST.mkRef {σ : Type} {m : Type → Type}
  [MonadLiftT (ST σ) m] {α : Type} (a : α) :
  m (ST.Ref σ α)

Creates a new mutable reference that contains the provided value a.

15.4.1.1. Reading and Writing

def

ST.Ref.get {σ : Type} {m : Type → Type}
  [MonadLiftT (ST σ) m] {α : Type}
  (r : ST.Ref σ α) : m α

Reads the value of a mutable reference.

def

ST.Ref.set {σ : Type} {m : Type → Type}
  [MonadLiftT (ST σ) m] {α : Type}
  (r : ST.Ref σ α) (a : α) : m Unit

Replaces the value of a mutable reference.

Data races with get and set

def main : IO Unit := do
  let balance ← IO.mkRef (100 : Int)

  let mut orders := #[]
  IO.println "Sending out orders..."
  for _ in [0:100] do
    let o ← IO.asTask (prio := .dedicated) do
      let cost ← IO.rand 1 100
      IO.sleep (← IO.rand 10 100).toUInt32
      if cost < (← balance.get) then
        IO.sleep (← IO.rand 10 100).toUInt32
        balance.set ((← balance.get) - cost)
    orders := orders.push o

  -- Wait until all orders are completed
  for o in orders do
    match o.get with
    | .ok () => pure ()
    | .error e => throw e

  if (← balance.get) < 0 then
    IO.eprintln "Final balance is negative!"
  else
    IO.println "Final balance is zero or positive."

stdoutSending out orders...

stderrFinal balance is negative!

def

ST.Ref.modify {σ : Type} {m : Type → Type}
  [MonadLiftT (ST σ) m] {α : Type}
  (r : ST.Ref σ α) (f : α → α) : m Unit

Atomically modifies a mutable reference cell by replacing its contents with the result of a function call.

Avoiding data races with modify

def main : IO Unit := do
  let balance ← IO.mkRef (100 : Int)

  let mut orders := #[]
  IO.println "Sending out orders..."
  for _ in [0:100] do
    let o ← IO.asTask (prio := .dedicated) do
      let cost ← IO.rand 1 100
      IO.sleep (← IO.rand 10 100).toUInt32
      balance.modify fun b =>
        if cost < b then
          b - cost
        else b
    orders := orders.push o

  -- Wait until all orders are completed
  for o in orders do
    match o.get with
    | .ok () => pure ()
    | .error e => throw e

  if (← balance.get) < 0 then
    IO.eprintln "Final balance negative!"
  else
    IO.println "Final balance is zero or positive."

stdoutSending out orders...Final balance is zero or positive.

stderr<empty>

def

ST.Ref.modifyGet {σ : Type} {m : Type → Type}
  [MonadLiftT (ST σ) m] {α β : Type}
  (r : ST.Ref σ α) (f : α → β × α) : m β

Atomically modifies a mutable reference cell by replacing its contents with the result of a function call that simultaneously computes a value to return.

def

ST.Ref.swap {σ : Type} {m : Type → Type}
  [MonadLiftT (ST σ) m] {α : Type}
  (r : ST.Ref σ α) (a : α) : m α

Atomically swaps the value of a mutable reference cell with another value. The reference cell's original value is returned.

15.4.1.2. Comparisons

def

ST.Ref.ptrEq {σ : Type} {m : Type → Type}
  [MonadLiftT (ST σ) m] {α : Type}
  (r1 r2 : ST.Ref σ α) : m Bool

Checks whether two reference cells are in fact aliases for the same cell.

Even if they contain the same value, two references allocated by different executions of IO.mkRef or ST.mkRef are distinct. Modifying one has no effect on the other. Likewise, a single reference cell may be aliased, and modifications to one alias also modify the other.

15.4.1.3. `ST`-Backed State Monads

def

ST.Ref.toMonadStateOf {σ : Type}
  {m : Type → Type} [MonadLiftT (ST σ) m]
  {α : Type} (r : ST.Ref σ α) : MonadStateOf α m

Creates a MonadStateOf instance from a reference cell.

This allows programs written against the state monad API to be executed using a mutable reference cell to track the state.

15.4.2. Concurrency🔗

Mutable references can be used as a locking mechanism. Taking the contents of the reference causes attempts to take it or to read from it to block until it is set again. This is a low-level feature that can be used to implement other synchronization mechanisms; it's usually better to rely on higher-level abstractions when possible.

unsafe def

ST.Ref.take {σ : Type} {m : Type → Type}
  [MonadLiftT (ST σ) m] {α : Type}
  (r : ST.Ref σ α) : m α

Reads the value of a mutable reference cell, removing it.

This causes subsequent attempts to read from or take the reference cell to block until a new value is written using ST.Ref.set.

Reference Cells as Locks

This program launches 100 threads. Each thread simulates a purchase attempt: it generates a random price, and if the account balance is sufficient, it decrements it by the price. If the balance is not sufficient, then it is not decremented. Because each thread takes the balance cell prior to checking it and only returns it when it is finished, the cell acts as a lock. Unlike using ST.Ref.modify, which atomically modifies the contents of the cell using a pure function, other IO actions may occur in the critical section This program's main function is marked Lean.Parser.Command.declaration : commandunsafe because take itself is unsafe.

unsafe def main : IO Unit := do
  let balance ← IO.mkRef (100 : Int)
  let validationUsed ← IO.mkRef false

  let mut orders := #[]

  IO.println "Sending out orders..."
  for _ in [0:100] do
    let o ← IO.asTask (prio := .dedicated) do
      let cost ← IO.rand 1 100
      IO.sleep (← IO.rand 10 100).toUInt32
      let b ← balance.take
      if cost ≤ b then
        balance.set (b - cost)
      else
        balance.set b
        validationUsed.set true
    orders := orders.push o

  -- Wait until all orders are completed
  for o in orders do
    match o.get with
    | .ok () => pure ()
    | .error e => throw e

  if (← validationUsed.get) then
    IO.println "Validation prevented a negative balance."

  if (← balance.get) < 0 then
    IO.eprintln "Final balance negative!"
  else
    IO.println "Final balance is zero or positive."

The program's output is:

stdoutSending out orders...Validation prevented a negative balance.Final balance is zero or positive.