# Question aboutthe use of an inner forall

**Jon Cast
**
jcast@ou.edu

*Mon, 19 Aug 2002 13:22:41 -0500*

"Scott J." <jscott@planetinternet.be> wrote:
>* Ok, a and s are type variables. It may be common usage for computer
*>* people
*
Bingo. You're trying to impose a non-CS understanding on a CS
statement. If you're familiar with the analogy, it's like a French
speaker trying to insist that ``demand'' in English cannot mean an
insistence, since it doesn't mean that in English.
>* but for someone with a math background it is difficult
*
Get used to difficulty. Seriously.
>* to call forall a a type . In logic one expects a statement in the
*>* scope of forall a like this
*
forall a is not a type (nor a statement) :) It's a phrase in any
number of languages, including formal logic and type theory (and it
has different, although cognate, meanings in those languages).
>* (forall a) statement. The statement may or may not depend on a.
*
True. But if you have (forall a. type), that doesn't fit your form.
And, just like (forall a. statement) is a statement, (forall a. type)
is a type. Easy, no?
>* So let's come backe to runST.
*
>* runST ::( forall s) (ST s a )-> a
*
May I ask a favor? If you're going to discuss type theory, learn
our notation:
>* runST :: (forall s. ST s a) -> a
*
Just a minor nit.
>* So I insist what is the statement ST s a ?
*
It's not a statement, and forall s. is not a logic quantifier. ST s a
is a type, and forall s. is a type quantifier.
>* Scott
*
Jon Cast