Question aboutthe use of an inner forall

[Jon Cast]

Jay Cox <sqrtofone@yahoo.com> wrote:
> From: "Ashley Yakeley" <ashley@semantic.org>
> > 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)).

I'm not sure I understand polymorphic types, but here's my best guess:

Polymorphic types form a sub-typing system, with the basic
sub-typing judgment:

(forall a. S) < [T/a]S

where T and S are types, and a may occur free in S, and (<) is the
sub-typing relation.  From this comes the typing judgment

S < T      x :: S
-----------------
     x :: T

For the purposes of runST, we only need to worry about one other
judgment, the standard judgment for sub-typing function arguments:

       S < T
-------------------
(T -> R) < (S -> R)

Justification: basically, the sub-typing statement (S < T) says that
every element of S is an element of T.  The typing statement (f ::
S -> R) says that f can take any value of type S and deliver a value
of type R (divergence is a value in Haskell!).  Now, if every element
of S is an element of T, and f can take every element of T, it follows
that f can take every element of S.

(x :: S) -> (x :: T)          (x :: T) -> (f x :: R)
----------------------------------------------------
               (x :: S) -> (f x :: R)

is an equivalent way of stating the above judgment.

So, runST's types are the super-types of (forall a. (forall s. ST s a)
-> a), which means all functions types for which the argument is a
super-type of (forall s. ST s a).

Does that clarify things any?

<snip>

Jon Cast