[Haskell-cafe] haskell-curry, classical logic, excluded middle

Derek Elkins derek.a.elkins at gmail.com
Sun Oct 14 17:48:55 EDT 2007

On Sun, 2007-10-14 at 15:20 -0600, Luke Palmer wrote:
> On 10/14/07, Tim Newsham <newsham at lava.net> wrote:
> > I've been struggling with this for the last day and a half.  I'm
> > trying to get some exercise with the type system and with logic by
> > playing with the curry-howard correspondence.  I got stuck on
> > the excluded-middle, and I think now I got it almost all the way
> > there, but its still not quite right.  Is this error I'm getting
> > (inline at the end) easily fixed, and what exactly is going on?
> I'll admit this is a cursory response, but (to my understanding)
> excluded middle doesn't hold in the Curry-Howard correspondence.  It
> is an isomorphism between *constructive* logic and types; excluded
> middle is a nonconstructive axiom.

It's possible to embed the classical propositional logic into the
intuitionistic propositional logic.  Kolmogorov invented the typed CPS
transform long before we even had programming languages.

More information about the Haskell-Cafe mailing list