21.4. 可变引用🔗

虽然普通的状态单子使用跟踪状态内容以及计算值的元组对有状态计算进行编码，但 Lean 的运行时系统还提供始终由可变内存单元支持的可变引用。可变引用的类型为 IO.Ref，指示单元格是可变的，并且读取和写入必须是显式的。 IO.Ref 是使用 ST.Ref 实现的，因此整个 ST.Ref API 也可以与 IO.Ref 一起使用。

def

IO.Ref (α : Type) : Type
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 α)
IO.mkRef {α : Type} (a : α) :
  BaseIO (IO.Ref α)

Creates a new mutable reference cell that contains a.

21.4.1. 状态转换器🔗

可变引用通常在不希望出现任意副作用的情况下很有用。当 Lean 无法将纯操作优化为突变时，它们可以显着加速，并且某些算法使用可变引用比状态单子更容易表达。此外，它还有一个其他副作用所没有的属性：如果一段代码使用的所有可变引用都是在其执行期间创建的，并且该代码中没有可变引用逃逸到其他代码，则评估结果是确定性的。

ST monad 是 IO 的受限版本，其中可变状态是唯一的副作用，并且可变引用无法转义。ST 首先由 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 采用从未用于对任何术语进行分类的类型参数。 runST 函数允许从 ST 转义，要求传递给它的 ST 操作可以使用 any 类型实例化此类型参数。这种未知类型除了作为函数的参数外不存在，这意味着由它“标记”类型的值无法逃脱其作用域。

def

ST (σ α : Type) : Type
ST (σ α : 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 σ α) : α
runST {α : Type}
  (x : (σ : Type) → ST σ α) : α

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

与 IO 和 EIO 一样，ST 也有一个变体，它采用自定义错误类型作为参数。这里，ST 类似于 BaseIO 而不是 IO，因为 ST 不会导致抛出错误。

def

EST (ε σ α : Type) : Type
EST (ε σ α : 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 ε α
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
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 σ α)
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.

21.4.1.1. 阅读和写作🔗

def

ST.Ref.get {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m] {α : Type}
  (r : ST.Ref σ α) : m α
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
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
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

该程序启动 100 个线程。每个线程模拟一次购买尝试：它生成一个随机价格，如果帐户余额足够，则将其减少该价格。余额检查和新值的计算发生在对 ST.Ref.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 β
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 α
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.

21.4.1.2. 比较🔗

def

ST.Ref.ptrEq {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m]
  {α : Type} (r1 r2 : ST.Ref σ α) : m Bool
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.

21.4.1.3. `ST` 支持的状态 Monad🔗

def

ST.Ref.toMonadStateOf {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m]
  {α : Type} (r : ST.Ref σ α) : MonadStateOf α m
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.

21.4.2. 并发性🔗

可变引用可以用作锁定机制。获取引用的内容会导致获取它或从中读取内容的尝试被阻止，直到它再次成为 set。这是一个低级功能，可用于实现其他同步机制；如果可能的话，通常最好依赖更高级别的抽象。

unsafe def

ST.Ref.take {σ : Type} {m : Type → Type} [MonadLiftT (ST σ) m]
  {α : Type} (r : ST.Ref σ α) : m α
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

该程序启动 100 个线程。每个线程模拟一次购买尝试：它生成一个随机价格，如果帐户余额足够，则将其减少该价格。如果余额不足，则不会减少。因为每个线程 take 在检查平衡单元之前都会对其进行操作，并且仅在完成时才将其返回，因此单元充当锁的作用。与使用 ST.Ref.modify（使用纯函数以原子方式修改单元格的内容）不同，其他 IO 操作可能发生在临界区中该程序的main函数被标记为Lean.Parser.Command.declaration : commandunsafe，因为take本身是不安全的。

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

该程序的输出是：

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