"Scott J."
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