为什么 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
最佳答案
更多的是对问题标题的回答,而不是问题本身,但仍然:
是的,ST 是引用透明的。
很长一段时间以来,这只是猜测和相信,直到今年我们才得到了适当的证明:
状态一元封装的逻辑关系:在存在 runST 的情况下证明上下文等价
阿明·蒂马尼、莱奥·斯特凡内斯科、莫滕·克罗格-杰斯佩森、拉斯·伯克达尔
有条件接受 POPL 2018
http://iris-project.org/ Preprint PDF
关于haskell - ST 引用透明吗?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/47381464/