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

Question

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

更具体地说,入口点函数的多态类型

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

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

这是否经过严格(甚至正式)证明？

Answer 1

这是Andrea Vezzosi 的Agda形式化,证明runST对于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单子仍是安全的,根本就没有可证明的总writeSTRef和readSTRef.

如果您有兴趣，我做了 [更简单](https://gist.github.com/AndrasKovacs/07310be00e2a1bb9e94d7c8dbd1dced6) 的 Agda 形式化 ST。它还可以正确计算，没有任何不安全的恶作剧。 (3认同)

Answer 2

Amin Timany等人就是这样.最近在POPL2018上发表了一篇关于这个主题的论文.你可以在这里找到论文.完全披露:我还没有时间彻底阅读它自己:).