# 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
about how it applies specifically to runST on John Launchbury and
Simon Peyton Jones' web pages.

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.

```