runST with Hindley-Milner type system

问题:

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?

回答1:

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 () 
...