The Curry-Howard Isomorphism
Leon Smith
lps@po.cwru.edu
Mon, 19 Aug 2002 13:06:59 -0400
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