[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Derek Elkins]

On Wed, 2007-10-17 at 15:06 -0700, Dan Weston wrote:
> That is a great tutorial. Thanks! But in the last two sentences of the 
> introduction you say:
> 
>  > We just need to find any program with the given type.
>  > The existence of a program for the type will be a proof
>  > of the corresponding proposition!
> 
> Maybe you should make explicit that
> 
> 1) the type is inhabited
> 
> undefined :: forall p . p
> 
> does not prove that all propositions are true

Yes it does.

> 
> 2) the function must halt for all defined arguments
> 
> fix :: forall p . (p -> p) -> p
> fix f = let x = f x in x
> 
> does not prove the (false) theorem
> 
> (p => p) => p

Yes it does.

Terms in Haskell prove the propositions that the types of Haskell
correspond to.  *The logic that Haskell's type systems corresponds to is
inconsistent.*  This is what you are missing.  Haskell's type systems
does not correspond to intuitionistic propositional logic.  Indeed, in
the actual statement of the Curry-Howard correspondence, it's a
correspondence between intuitionistic propositional logic and the simply
typed lambda calculus which Haskell quite certainly is not.  As is well
known, it (CH) can be generalized beyond that, but generally you need a
strongly normalizing language (or at least prove strong normalization
for your particular term and note normalization means -normal form- not
weak head normal form) to actually use the "programs" as proofs.