[Haskell-cafe] Tutorial: Curry-Howard Correspondence
lennart at augustsson.net
Sun Oct 21 20:12:52 EDT 2007
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
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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe