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

[Luke Palmer]

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.

Luke