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

_______________________________________________
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to