Re: Question aboutthe use of an inner forall

[Scott J.]

Ok, a and s are type variables. It may be common usage for computer people but for someone with a math background it is difficult to call forall a a type . In logic one expects a statement in the scope of forall a like this

 

(forall a) statement. The statement may or may not depend on a.

 

So let's come backe to runST.

 

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

 

So I insist what is the statement ST s a ?

 

Scott

 

 

----- Original Message -----

From: "Ashley Yakeley" <[EMAIL PROTECTED]>

To: "Scott J." <[EMAIL PROTECTED]>

Cc: "Haskell Cafe List" <[EMAIL PROTECTED]>

Sent: Monday, August 19, 2002 4:26 AM

Subject: Re: Question aboutthe use of an inner forall

> At 2002-08-18 18:19, Scott J. wrote:
>
> >A question: s is not a type variable as a isn't it?
>
> Both are quantified type variables. But only one of those quantifiers can
> be placed at the top level of the expression.
>
>    runST :: forall a. ((forall s. ST s a) -> a)
>
> > I mean a can be of type Integer while s cannot.
>
> Well yes, you can specialise "forall a" to Integer. So runST can be
> specialised to this type:
>
>    runST ::[special] (forall s. ST s Integer) -> Integer
>
> ...whereas you cannot specialise "s" in the same way. Think of it in
> terms of logic, if for all a: f(a), then by simple specialisation
> f(Integer).
>
> --
> Ashley Yakeley, Seattle WA
>
>