The Curry-Howard Isomorphism

[Leon Smith]

For an explanation why runST has the type it does, see page 4 of Simon 
Peyton-Jones and John Launchbury's paper "Lazy functional state threads"

http://research.microsoft.com/Users/simonpj/Papers/lazy-functional-state-threads.ps.Z

On Friday 16 August 2002 23:57, Scott J. wrote:
>runST :: forall a ( forall s ST s a) -> a ? 
>
>In logic forall x forall y statement(x.y) is equivalent to: 
>  forall y forall x statement(x,y).

True, but that isn't runST's type.   "forall a" quantifies over the entire 
type, whereas "forall s" quantifies over the left hand side of the 
implication.  In other words, you have "forall a. statement(a)", where 
statement includes a substatement "forall s. substatement(s,a)"

Now, using a different argument, since "s" does not appear free on the R.H.S 
of the implication,  "forall s" can be moved outside the implication to 
quantify over the entire type.

However, this brings up an important point about the Curry-Howard 
Isomorphism, which basically says that types are statements in first-order 
logic, and the corresponding values are proofs of those statements.   

When we work in logic, we care mainly about the *statements*.  Proofs are 
ways of justifying new statements.   Equivalent statements are in a sense 
"equal", and can usually be freely substituted for each other.	When we have 
a statement such as P /\ Q, where P and Q are statements such as "John is 
wearing a kilt" and "John is Scottish", it doesn't really matter which order 
they come in.  Mathematicians generally understand that /\ is commutative, 
and thus we can use P /\ Q and Q /\ P interchangeably throughout our 
discussion.  (Unless you are writing proofs in certain highly formal proof 
systems, such as Coq, Isabelle, or Haskell's type system)

When we work in type theory, we care mainly about the *proofs*.  Statements 
are ways of constraining our proofs to ensure they are at least somewhat 
sensible.  When we have a type (Int, Char), where Int is the statement "my 
value is a 32-bit integer", and Char says "my value is a character", order 
does matter.  Here, (4,'H') is a "proof" of the proposition (Int,Char), and 
('H', 4) is a proof of the proposition (Char, Int).   Although (Int, Char) 
<=> (Char, Int)  are logically equivalent, (4,'H') is a different value than 
('H', 4).    This equivalence  can be "proven" using the function:  

swap :: (a,b) -> (b,a)
swap (x,y) = (y, x)

Which, using the Curry-Howard isomorphism, is also a proof that /\ is 
commutative.

In short, just because a type "a" implies type "b", and type "b" implies type 
"a", doesn't mean they are interchangeable as statements are in logic.

Hope this helps,
leon