Question aboutthe use of an inner forall

[Jay Cox]

----- Original Message -----
From: "Ashley Yakeley" <ashley@semantic.org>
To: "Scott J." <jscott@planetinternet.be>; "Haskell Cafe List"
<haskell-cafe@haskell.org>
Sent: Friday, August 16, 2002 11:15 PM
Subject: Re: Question aboutthe use of an inner forall


> At 2002-08-16 20:57, Scott J. wrote:
>
> >However what for heaven's sake should I think of
> >
> >runST :: forall a ( forall s ST s a) -> a ?
>
>   runST :: forall a. ((forall s. ST s a) -> a)
>
> "For all a, if (for all s, (ST s a)) then a."
>
> You may apply runST to anything with a type of the form (forall s. ST s
> a), for any 'a'.

I'm very fuzzy to the details of type theory in general so please forgive
any errors.

I noted the same question as Scott's when I first learned about ST threads.

When you have a rank-2 polymorphic function, like

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

the type means the function takes an argument ***at least as polymorphic***
as
(forall s . ST s (some type a independent of s)).  If (runST stthread ) has
type String, then stthread must at least have type ST s String.

Why do you need this apparent mumbo jumbo about Rank-2 polymorphism?  It
insures your ST threads are threadsafe (or so I have been led to believe).
You will not be able to throw a mutable reference outside of the thread.

take this long interaction from  ghci (the ST> is the prompt, and what
follows
on the same line is the code entered.  For instance :type gives the type of
the following code.  I have separated ghci input/ouput from comments by
placing # in front of the IO).

#ST> :type newSTRef (3::Prelude.Int)
#forall s. ST s (STRef s PrelBase.Int)

The type variable a is replaced by, or a has the value of, (STRef s
PrelBase.Int). but this depends on s.

#ST> :type readSTRef
#forall s a. STRef s a -> ST s a
#ST> :type (do x<-newSTRef (3::Prelude.Int);readSTRef x)
#forall s. ST s PrelBase.Int

a here is replaced by PrelBase.Int. the code in the do statement is runnable
with runST

#ST> runST (newSTRef (3::Prelude.Int))
#
#Ambiguous type variable(s) `a' in the constraint `PrelShow.Show a'
#arising from use of `PrelIO.print' at <No locn>
#In a 'do' expression pattern binding: PrelIO.print it
#
#<interactive>:1:
#    Inferred type is less polymorphic than expected
#        Quantified type variable `s' escapes
#        It is reachable from the type variable(s) `a'
#          which is free in the signature
#    Signature type:     forall s. ST s a
#    Type to generalise: ST s1 (STRef s1 PrelBase.Int)
#    When checking an expression type signature
#    In the first argument of `runST', namely
#        `(newSTRef (3 :: PrelBase.Int))'
#    In the definition of `it': runST (newSTRef (3 :: PrelBase.Int))

above is a demonstration of how the type checking prevents
using/reading/modifying references outside of the ST world.

I realize this is a bit of an incomplete explanation:  Some questions I
would like to answer to help your comprehension but cannot due to my
ignorance are:

1. how do you measure the polymorphic nature of a type  so that you can say
it is "at least as polymorphic"? I have a fuzzy idea and some examples (Num
a => a vs. forall a . a vs.  forall a . [a], etc.)  but I haven't yet found
out for myself a precise definition.
2. what does it mean that type variable "escapes", and why is it bad?  A
reasonable answer isn't popping into my head right now.  Something about how
the type of a program should be fully resolved pops into my head but nothing
cohesive.

Maybe that helps.

Jay Cox