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