Search code examples
haskellmonadshindley-milner

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?

Solution

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

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

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