9.4. 可変参照（Mutable References）

通常の状態モナドは計算の値とともに状態の内容を追跡するタプルを使用して状態のある計算をエンコードしますが、Lean のランタイムシステムは、常に可変なメモリセルにバックアップされた可変参照も提供しています。可変参照は IO.Ref 型を持ちます。これによってセルが可変であることが示され、読み取りと書き込みは明示的に行う必要があります。 IO.Ref は ST.Ref を使って実装されているため、 ST.Ref API をすべて IO.Ref と一緒に使うことができます。

def

IO.Ref (α : Type) : Type

References

def

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

9.4.1. 状態変換（State Transformers）🔗

可変参照は恣意的な副作用が望ましくないコンテキストでしばしば有用です。こうした参照は 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 は型パラメータを取りますが、その型パラメータはどの項の分類にも使用されません。 ST からのエスケープを可能にする runST 関数は、渡される ST アクションがこの型パラメータを 任意の 型でインスタンス化できることを要求します。この未知の型は関数のパラメータとして以外は存在しないため、この型によって「マーク」された値はそのスコープから逃れることができません。

def

ST (σ : Type) : Type → Type

def

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

IO や EIO と同様に、カスタムエラー型をパラメータとして受け取る ST のバリエーションも存在します。ここでは、 ST はエラーを投げることができないため、 IO より BaseIO に類似しています。

def

EST (ε σ : Type) : Type → Type

def

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

structure

ST.Ref (σ α : Type) : Type

Constructor

ST.Ref.mk

Fields

ref : ST.RefPointed.type

h : Nonempty α

def

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

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

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

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

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 β

9.4.1.2. 比較（Comparisons）

def

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

9.4.1.3. 並行性（Concurrency）

可変参照はロックメカニズムとして使用することができます。参照の内容を取得すると、その参照を取得しようとしたり、そのリファレンスから読み込もうとしたりすると set されるまでブロックされます。これは低レベルの機能であり、他の同期メカニズムを実装するために使用することができます；ただし可能であればより高度な抽象化に頼ったほうが良いです。

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

ロックとしての参照セル

このプログラムは100個のスレッドを起動します。各スレッドは購入をシミュレートします：ランダムな価格を生成し、口座の残高が十分であれば、その価格分だけ残高を減少させます。もし残高が十分でなければ、残高を減らしません。各スレッドは残高を確認する前に残高セルを take し、確認が終わるとそれを返すだけであるため、セルはロックとして機能します。 ST.Ref.modify を使用して純粋関数を使用してアトミックにセルの内容を変更するのとは異なり、クリティカルなセクションで他の IO アクションが発生する可能性があります。このプログラムの main 関数は take 自体が安全ではないため、 Lean.Parser.Command.declaration : commandunsafe とマークされています。

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.