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 <[EMAIL PROTECTED]> 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@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
