# Question aboutthe use of an inner forall

**Alastair Reid
**
alastair@reid-consulting-uk.ltd.uk

*19 Aug 2002 12:55:27 +0100*

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 <ashley@semantic.org> 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.
*