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

[Derek Elkins]

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.