Ashley's comparision of types and logic misses out one important point of comparision: types logic value/expression of type T proof of logical statement T For example, consider a statement like: A /\ B => A The corresponding type is forall a,b. (a,b) -> a or, in English, for any a and b you choose, given a pair of an a and a b, I will give you an a. Now think of a and b as being proofs of a and b: for any propositions a and b you choose, given a pair of a proof of a and a proof of b, I will give you a proof of a. In other words, a function with type 'forall a,b. (a,b) -> a' can be used to construct a proof of A given a proof of A /\ B. This correspondance is known as the Curry-Howard Isomorphism. You can read a lot more about it on Phil Wadler's web page and you can read about how it applies specifically to runST on John Launchbury and Simon Peyton Jones' web pages. http://www.research.avayalabs.com/user/wadler/ http://www.cse.ogi.edu/~jl/ http://research.microsoft.com/Users/simonpj/ -- Alastair Reid alastair@reid-consulting-uk.ltd.uk Reid Consulting (UK) Limited http://www.reid-consulting-uk.ltd.uk/alastair/ 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 ?

Ashley Yakeley writes:

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.