Universal quantification and unification, example

Question

Given the following signature to start the monad ST

 runST :: (forall s. ST sa) -> a 

and functions

 newVar :: a -> ST s (MutVar sa) readVar :: MutVar sa -> ST sa 

The Haskell compiler will then reject the next invalid typed expression.

 let v = runST (newVar True) in runST (readVar v) 

Since the runST evaluation requires that the type

 readVar v :: ST s Bool 

should be generalized to

 ∀s . ST s Bool 

My question is that the only job of the Universal quantifier is to ensure that a variable of type s always free in the context of evaluation, avoiding generalization, right? or is it more about universal quantifier here?

Answer 1

Let's read the runST type. I added an explicit quatifier for a .

 runST :: forall a . (forall s. ST sa) -> a 

He reads the following contract:

• the caller selects a fixed type a
• the caller provides the argument x
• argument x must be of type ST sa for any choice of s . In other words, s will be chosen by runST rather than the caller.

See a similar example:

 runFoo :: forall a . (forall s. s -> [(s,a)]) -> [a] runFoo x = let part1 = x "hello!" -- here s is String -- part1 has type [(String, a)] part2 = x 'a' -- here s is Char -- part2 has type [(Char, a)] part3 = x (map snd part2) -- here s is [a] (!!!) -- part3 has type [([a],a)] in map snd part1 ++ map snd part2 ++ map snd part3 test1 :: [Int] test1 = runFoo (\y -> [(y,2),(y,5)]) -- here a is Int test2 :: [Int] test2 = runFoo (\y -> [("abc" ++ y,2)]) -- ** error -- I can't choose y :: String, runFoo will choose that type! 

Above, note that a fixed (before Int ) and that I cannot impose any type restrictions on y . Moreover:

 test3 = runFoo (\y -> [(y,y)]) -- ** error 

Here I am not fixing a in advance, but I'm trying to choose a=s . I am not allowed to do this: runFoo allowed to choose s in terms of a (see part3 above), so a needs to be fixed in advance.

Now, for your example. The problem is

 runST (newSTRef ...) 

Here newSTRef returns ST s (STRef s Int) , so it tries to select a = STRef s Int . Since a depends on s , this choice is not valid.

This "trick" is used by the ST monad to prevent references to the "escape" from the monad. That is, it is guaranteed that after runST all links now become inaccessible (and, possibly, they can be garbage collected). Because of this, the altered state that was used to calculate ST was selected, and the result of runST indeed a pure value. This is, after all, the main purpose of the ST monad: it is intended to resolve a (temporary) mutable state that should be used in pure computation.

Answer 2

I think you are missing something. The actual GHCi message gives:

 Prelude> :m +Control.Monad.ST Prelude Control.Monad.ST> data MutVar sa = MutVar Prelude Control.Monad.ST> :set -XRankNTypes Prelude Control.Monad.ST> data MutVar sa = MutVar Prelude Control.Monad.ST> let readVar = undefined :: MutVar sa -> ST sa Prelude Control.Monad.ST> let newVar = undefined :: a -> ST s (MutVar sa) Prelude Control.Monad.ST> runST $ readVar $ runST $ newVar True <interactive>:14:27: Couldn't match type 's' with 's1' 's' is a rigid type variable bound by a type expected by the context: ST s Bool at <interactive>:14:1 's1' is a rigid type variable bound by a type expected by the context: ST s1 (MutVar s Bool) at <interactive>:14:19 Expected type: ST s1 (MutVar s Bool) Actual type: ST s1 (MutVar s1 Bool) In the second argument of '($)', namely 'newVar True' In the second argument of '($)', namely 'runST $ newVar True' 

The Haskell compiler rejects it not because of anything related to readVar , but because of a problem with newVar , which is that ST s (MutVar sa) allows s "escape" from its context by jumping into MutVar .