Fw: Question aboutthe use of an inner forall

Jon Cast jcast@ou.edu
Mon, 19 Aug 2002 13:15:40 -0500


Jan Brosius <jscott@planetinternet.be> wrote:
> Still some question: Ok a is not a type but Integer is a type .
> But a can be instantiated to integer. This comes pretty close to
> call a therefore a type variable, Isn't it?

> And otherwise why writing forall a etc.

If s, t are types, the type s -> t says ``give me a value of type s,
and I'll give you a value of type t''.  If a is a type variable, and
(given a is a type) s is a type, then forall a. s says ``give me a
type t, and I'll give you a value of type s[t]''.

More specifically, if you write

> f :: a -> b

f has the form (\ x :: a -> (y :: b)), where the \ binds values.

If you write

> f :: forall a. a

f has the form (/\ a -> (x :: a)), where the /\ binds types.

Now, runST's argument has type forall s. ST s a.  In other words, it's
essentially a function over types---and it has to take /any/ type
runST wants to hand it.

> Regards

> Scott

Jon Cast