haskell - ST 引用透明吗？

Question

为什么 ST 被设计为禁止使用以下代码 as shown in the wikibook ？这篇文章似乎表明，如果允许的话，ST 效果会泄漏到另一个 ST 中，但我不太明白为什么。

我似乎无法运行特定的ST (STRef s a)。 ST 效果是否包含且引用透明，但此类使用仍被视为无效？

直觉告诉我，IO 和 ST 之间的语义差异与存在一个 IO 和许多独立的 相关。 ST，但我不确定。

> runST (newSTRef True)

<interactive>:5:8: error:
    • Couldn't match type ‘a’ with ‘STRef s Bool’
        because type variable ‘s’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a type expected by the context:
          forall s. ST s a
        at <interactive>:5:1-21
      Expected type: ST s a
        Actual type: ST s (STRef s Bool)
    • In the first argument of ‘runST’, namely ‘(newSTRef True)’
      In the expression: runST (newSTRef True)
      In an equation for ‘it’: it = runST (newSTRef True)
    • Relevant bindings include it :: a (bound at <interactive>:5:1)

> :t newSTRef
newSTRef :: a -> ST s (STRef s a)

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

Answer 1

更多的是对问题标题的回答，而不是问题本身，但仍然:

是的，ST 是引用透明的。

很长一段时间以来，这只是猜测和相信，直到今年我们才得到了适当的证明:

状态一元封装的逻辑关系:在存在 runST 的情况下证明上下文等价
阿明·蒂马尼、莱奥·斯特凡内斯科、莫滕·克罗格-杰斯佩森、拉斯·伯克达尔
有条件接受 POPL 2018
http://iris-project.org/ Preprint PDF