6.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

References

def

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

6.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

def

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

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

def

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

structure

ST.Ref (σ α : Type) : Type

Constructor

ST.Ref.mk {σ α : Type}
    (ref : ST.RefPointed.type) (h : Nonempty α)
    : ST.Ref σ α

Fields

`h`	:	`Nonempty α`
`ref`	:	`ST.RefPointed.type`

def

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

6.4.1.1. Reading and Writing

def

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

def

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

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

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 β

6.4.1.2. Comparisons

def

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

6.4.1.3. 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 α

def

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

def

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

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.