21.4. 可变引用🔗

普通的状态单子使用元组编码有状态计算，元组同时跟踪状态内容与计算结果；Lean 运行时系统还提供始终由可变内存单元支撑的可变引用。可变引用的类型为 IO.Ref，它表明单元是可变的；读取和写入都必须显式进行。 IO.Ref 使用 ST.Ref 实现，因此完整的 ST.Ref API 也可用于 IO.Ref。

定义

IO.Ref (α : Type) : Type
IO.Ref (α : Type) : Type

保存 α 类型值的可变引用单元。可以在 IO 单子中读取和修改这些单元。

定义

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

创建一个包含 a 的新可变引用单元。

21.4.1. 状态变换器🔗

在不希望出现任意副作用的场合，可变引用往往很有用。当 Lean 无法把纯操作优化为原地修改时，可变引用能显著提速；有些算法用可变引用也比用状态单子更容易表达。此外，它还具有其他副作用所不具备的性质：若一段代码使用的所有可变引用都在执行期间创建，且没有可变引用从该代码逃逸到其他代码，那么求值结果就是确定的。

ST 单子是 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 动作能把该类型参数实例化为任意类型。这个未知类型只作为函数参数存在，因此类型被它“标记”的值无法逃出其作用域。

定义

ST (σ α : Type) : Type
ST (σ α : Type) : Type

IO 的受限版本，其中可变状态是唯一的副作用。

可以使用 runST 在非单子上下文中运行 ST 计算。

定义

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

运行一个 ST 计算；该计算唯一的副作用是通过 ST.Ref 操作可变状态。

与 IO 和 EIO 类似，ST 也有一个把自定义错误类型作为参数的变体。这里，ST 对应的是 BaseIO 而非 IO，因为 ST 不会导致错误被抛出。

定义

EST (ε σ α : Type) : Type
EST (ε σ α : Type) : Type

IO 的受限版本，其中可变状态和异常是仅有的副作用。

可以使用 runEST 在非单子上下文中运行 EST 计算。

定义

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

运行一个 EST 计算；该计算仅有的副作用是可变状态和异常。

结构体

ST.Ref (σ α : Type) : Type
ST.Ref (σ α : Type) : Type

保存 α 类型值的可变引用单元。可以在 ST σ 单子中读取和修改这些单元。

构造子

ST.Ref.mk

定义

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 σ α)

创建一个包含给定值 a 的新可变引用。

21.4.1.1. 读取与写入🔗

定义

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 α

读取可变引用中的值。

定义

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

替换可变引用中的值。

get 与 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

  -- 等待所有订单完成
  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!

定义

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

原子地修改可变引用单元：用一次函数调用的结果替换其中的内容。

使用 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

  -- 等待所有订单完成
  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>

定义

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 β

原子地修改可变引用单元：用一次函数调用的结果替换其中的内容，同时计算一个要返回的值。

定义

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 α

原子地将可变引用单元中的值与另一个值交换，并返回该引用单元原来的值。

21.4.1.2. 比较🔗

定义

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

检查两个引用单元实际上是否为同一单元的别名。

即使包含相同的值，由不同次执行 IO.mkRef 或 ST.mkRef 分配的两个引用也是不同的；修改其中一个不会影响另一个。反之，同一个引用单元可以有多个别名，修改任一别名也会修改其他别名所指的同一单元。

21.4.1.3. 由 `ST` 支撑的状态单子🔗

定义

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

从引用单元创建一个 MonadStateOf 实例。

这样，针对状态单子 API 编写的程序便可使用可变引用单元来跟踪状态并执行。

21.4.2. 并发🔗

可变引用可以用作锁机制。取走引用内容后，再次尝试取走或读取它的操作都会阻塞，直至通过 set 重新设置其内容。这是一项可用于实现其他同步机制的底层功能；只要可能，通常应优先采用更高层的抽象。

不安全定义

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 α

读取并取走可变引用单元中的值。

此后若尝试读取或再次取走该引用单元，将阻塞到使用 ST.Ref.set 写入新值为止。

用引用单元充当锁

该程序启动 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

  -- 等待所有订单完成
  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.