On Sun, Feb 15, 2009 at 11:50 AM, Kim-Ee Yeoh
Having said that, I'm not sure about the statement on page 9 that "readVar v simply does not have type forall s. ST s Bool." The variable v could be of type "forall s. MutVar s Bool", in which case all of "runST (readVar v)" typechecks.
"readVar v" can't have the type (forall s. ST s Bool), because v must have been created by newVar. So, (newVar True >>= \v -> readVar v) has the type (forall s. ST s Bool), but the subexpression (readVar v) has the type ST hiddenState Bool, where hiddenState is constrained to match the same state as was used by newVar and bind (>>=). Decoding into System F might make this more explicit: newVar :: forall t s. t -> ST s (MutVar s t) readVar :: forall t s. MutVar s t -> ST s t bind :: forall a b s. ST s a -> (a -> ST s b) -> ST s b Then the expression is: /\s -> bind @(MutVar s Bool) @Bool @s (newVar @Bool @s True) (\(v :: MutVar s Bool) -> readVar @Bool @s v) (where /\ is a type-level lambda, and @ is used for type-level application, that is, to remove one layer of "forall" from a type.) Note that there is no way to turn the insides of that final lambda expression into something that uses any "s" without getting something of type "forall s. MutVar s Bool". But there's no way to do so because newVar only returns results of type "forall s. ST s (MutVar s Bool)"; then s is constrained to match during the binding application. Then, looking at the type of runST: forall t. (forall s. ST s t) -> t, you see that runST must be passed an argument that has a type level lambda for s, saying that runST gets to choose the type "s" used to call it. In particular, in GHC I believe that s is always instantiated with RealWorld# when runST uses its argument, but you never get to see that. runST is just unsafePerformIO made safe by making the Real World "hidden" in the forall so that it can't escape. -- ryan