# Question aboutthe use of an inner forall

**Jon Cast
**
jcast@ou.edu

*Mon, 19 Aug 2002 13:40:25 -0500*

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