RunST阻止访问闭包中另一个有状态线程的引用

Question

我遇到过RunST的Rank 2类型的许多解释,以及它如何阻止引用逃避RunST.但我无法找出为什么这也会阻止以下代码进行类型检查(这是正确的,但我仍然想了解它是如何做到的):

test = do v ? newSTRef True
          let a = runST $ readSTRef v
          return True

相比:

test = do v ? newSTRef True
          let a = runST $ newSTRef True >>= ?v ? readSTRef v
          return True

在我看来newSTRef,两种情况的类型相同:?s. Bool ? ST s (STRef s Bool).和类型v是?s. STRef s Bool在这两种情况下,以及如果我的理解是正确的.但后来我很困惑,接下来该做什么,为什么第一个例子不进行类型检查,我没有看到两个例子之间的差异,除了在第一个例子中v被绑定runST在第二个外部和内部,我怀疑是关键在这里.如果我在推理的某个地方出错了,请帮我展示一下这个和/或纠正我.

Answer 1

该功能runST :: (forall s . ST s a) -> a是魔术发生的地方.要问的正确问题是如何生成具有类型的计算forall s . ST s a.

将其读作英语,这是一个对所有选择有效的计算s,幻象变量表示ST计算的特定"线程" .

当你使用newSTRef :: a -> ST s (STRef s a)你正在生成一个STRef与ST生成它的线程共享其线程变量.这意味着s值的类型v固定s为与较大线程的类型相同.这种固定性意味着v不再涉及的操作对于所有线程的选择都是有效的s.因此,runST将拒绝涉及的操作v.

相反,类似的计算newSTRef True >>= \v -> readSTRef v在任何ST线程中都是有意义的.整个计算有一个"适用于所有" ST线程的类型s.这意味着它可以使用runST.

一般来说,runST必须包装所有ST线程的创建.这意味着s参数内部的所有选择runST都是任意的.如果来自周围环境的某些东西runST与其runST论证相互作用,则可能会修复一些s与周围环境相匹配的选择,从而不再适用于"所有"选择s.