9

如果我正确理解 Haskell 中的 ST monad,runST请以巧妙的方式使用 rank-2 类型,以确保在转义 monad 时计算不会引用任何其他线程。

我有一个带有 Hindley-Milner 类型系统的玩具语言,我的问题如下:是否可以使用用于键入应用程序的临时规则扩展 HM 类型系统,runST以便 ST monad 可以安全地逃避,而无需引入等级-2 种?

更准确地说,runST将具有类型forall s a. ST s a -> a(即 rank-1)并且类型化规则将首先尝试以与 HM 在 let 表达式中泛化类型相同的方式泛化计算类型,但如果s发现类型变量被绑定,则会引发类型错误.

与香草 HM 相比,上述内容仅限制了可接受的程序,所以看起来不错,但我不确定。这行得通吗?

4

1 回答 1

2

万一对问题的评论不完全清楚,您需要的判断是

{\Gamma \vdash e \colon \forall s.\, {\tt ST}\, s\, a ~~~~ s \not\in \text{free}(a)\over \Gamma \vdash {\ tt runST}\, e \冒号 a} ~~\text{[runST]}

这当然与Hindley-Milner附带的其他常见的打字判断相结合。有趣的是,我们最终不需要为任何引入类型的东西制定特殊规则ST,因为这些都不需要等级 2 的类型签名:

newSTRef :: a -> ST s (STRef s a)
readSTRef :: STRef s a -> ST s a
writeSTRef :: STRef s a -> a -> ST s () 
...
于 2016-11-13T07:22:15.560 回答