Question aboutthe use of an inner forall
Ashley Yakeley
ashley@semantic.org
Sun, 18 Aug 2002 20:30:33 -0700
At 2002-08-18 20:12, Scott J. wrote:
>So let's come backe to runST.
>
>runST ::( forall s) (ST s a )-> a
>
>So I insist what is the statement ST s a ?
Oh it's not really a statement, it just plays a similar role in types
that statements play in logic. The comparison runs something like this:
type variable variable
type statement
type constructor function
"->" implies
application derivation
"forall" universal quantification
type specialisation specialisation
For instance, in logic if you have "A" and you have "A implies B", you
can derive "B". Likewise, if you have a value of type "a", and a value of
type "a -> b", by using function application you can obtain a value of
type "b".
The type theory has the same structure as the logic, merely a different
interpretation.
--
Ashley Yakeley, Seattle WA