Question aboutthe use of an inner forall

[Jon Cast]

"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