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