用Hindley-Milner型系统运行 [英] runST with Hindley-Milner type system

问题描述

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

我有一个带有Hindley-Milner类型系统的玩具语言，我的问题如下：是否可以通过ad-特殊规则，用于键入 runST 应用程序，以便ST monad可以安全地转移，不引入rank-2类型

更准确地说， runST 应该有类型 forall s a。 ST s a - >一个（即rank-1），并且打字规则首先尝试用类似于let-expressions中的类型概括计算类型，但是如果 s 类型变量被绑定。

以上只限制接受的程序与香草HM相比，所以看起来很合理，但我我不确定。这会起作用吗？

解决方案

为了防止对问题的评论不完全清楚，您需要的判断是

这当然与 Hindley-Milner 。有趣的是，我们并不需要为引入 ST 类型的任何东西制定特殊规则，因为这些都不需要rank级别签名2：

  newSTRef :: a  - > ST s（STRef s a）
 readSTRef :: STRef s a  - > ST s a 
 writeSTRef :: STRef s a  - > a  - > ST s（）
 ... 
  

If I understand the ST monad in Haskell correctly, runST uses rank-2 types in a clever way to ensure that a computation does not reference any other thread when escaping the monad.

I have a toy language with a Hindley-Milner type system, and my question is the following: is it possible to extend the HM type system with an ad-hoc rule for typing runST applications so that the ST monad is safely escapable, without introducing rank-2 types?

More precisely, runST would have type forall s a. ST s a -> a (i.e. rank-1) and the typing rule would first try to generalize the computation type in the same way HM generalizes types in let-expressions, but raise a type error if the s type variable is found to be bound.

The above only restricts accepted programs compared to vanilla HM, so it seems sound, but I am unsure. Would this work?

解决方案

Just in case the comments to the question are not entirely clear, the judgement you would need is

This is of course in conjunction with the other usual typing judgments that come with Hindley-Milner. Interestingly enough, we don't end up needing to make special rules for anything introducing an ST type, since none of these require type signatures of rank 2:

newSTRef :: a -> ST s (STRef s a)
readSTRef :: STRef s a -> ST s a
writeSTRef :: STRef s a -> a -> ST s () 
...

这篇关于用Hindley-Milner型系统运行的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！