Question aboutthe use of an inner forall
Mon, 19 Aug 2002 13:22:41 -0500
"Scott J." <firstname.lastname@example.org> wrote:
> Ok, a and s are type variables. It may be common usage for computer
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
> 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.