[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Lennart Augustsson]

There's nothing wrong with Haskell types.  It's the terms that make Haskell
types an inconsistent logic.
But that doesn't mean that the C-H correspondence doesn't have any insight
to offer.

  -- Lennart

On 10/21/07, Derek Elkins <derek.a.elkins at gmail.com> wrote:
>
> 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.
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20071022/8c4d9421/attachment.htm