Question aboutthe use of an inner forall

Alastair Reid
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.

Alastair Reid         
Reid Consulting (UK) Limited

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.