[Haskell-cafe] forall & ST monad

[Ryan Ingram]

On Sun, Feb 15, 2009 at 11:50 AM, Kim-Ee Yeoh <a.biurvOir4 at asuhan.com> wrote:
> 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