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

On Sun, 2007-10-14 at 15:20 -0600, Luke Palmer wrote:

On 10/14/07, Tim Newsham 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.