Jay Cox
From: "Ashley Yakeley"
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