Question aboutthe use of an inner forall

[Alastair Reid]

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.