haskell - 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 (STRef s Bool)。而v的类型是∃s。 STRef s Bool 在这两种情况下也是如此，如果我理解正确的话。但是接下来我很困惑接下来要做什么来说明为什么第一个示例没有类型检查，我没有看到两个示例之间的差异，除了在第一个示例中 v 绑定(bind)在 runST 并在第二个里面，我怀疑这是这里的关键。如果我的推理中有错误，请帮助我展示这一点和/或纠正我。

Answer 1

函数runST::(forall s . ST s a) -> a 是神奇发生的地方。正确的问题是如何生成 forall s 类型的计算。 ST 是一个。

用英语理解，这是一个对 s 的所有选择都有效的计算，这个虚拟变量表示 ST 计算的特定“线程”。

当您使用 newSTRef::a -> ST s (STRef s a) 时，您将生成一个 STRef ，它与 ST 生成它的线程。这意味着值 v 的 s 类型固定为与较大线程的 s 类型相同。这种固定性意味着涉及 v 的操作不再对线程 s 的“所有”选择有效。因此，runST 将拒绝涉及 v 的操作。

相反，像 newSTRef True >>=\v -> readSTRef v 这样的计算在任何 ST 线程中都有意义。整个计算有一个“对所有”ST 线程 s 有效的类型。这意味着它可以使用 runST 运行。

一般来说，runST 必须环绕所有 ST 线程的创建。这意味着 runST 参数内的所有 s 选择都是任意的。如果 runST 周围上下文中的某些内容与 runST 的参数交互，那么可能会修复 s 的某些选择以匹配周围的上下文因此不再可以自由地适用于s的“所有”选择。