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