haskell - 有没有证据证明 runST 确实是纯的？

Question

ST monad最初由Launchbury 和 Peyton Jones设计，允许 Haskell 程序员编写命令式代码（使用可变变量、数组等），同时获得该代码的纯接口。

runST :: (forall s. ST s a) -> a

确保包含计算的所有副作用ST，并且结果值是纯的。

这曾经被严格（甚至正式）证明过吗？

score 14 · Accepted Answer

这是 Andrea Vezzosi 的Agda 形式化，它证明了对于具有可读/可写 refsrunST的 monad 来说这是安全且全面的。ST它依赖于假设的参数性，即所涉及定义的自由定理的真实性，这是预期的，因为参数性正是这个forall s.技巧起作用的原因。

但是，证明假设我们不能将值放入STRef s本身依赖的类型中ST s。在 Haskell 中，我们可以使用这种依赖来获得循环而无需递归：

loop :: ()
loop = runST $ do
  x <- newSTRef (pure ())
  writeSTRef x $ do
    y <- readSTRef x
    y
  y <- readSTRef x
  y

可能这个版本的 ST monad 仍然是安全的，只是没有可证明的writeSTRef总和readSTRef。

score 8 · Accepted Answer

Amin Timany 等人恰好如此。最近在 POPL2018 上发表了一篇关于这个主题的论文。你可以在这里找到论文。完全披露：我自己还没有时间仔细阅读它:)。

2 回答 2