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

Now that that works, one more question. Is it possible to hide the "r" that is attached to every single type? For example to do something like this (which doesn't compile): No answer needed. Duh.. I can just pick "r" to be any type (like "()"). I've got intuitionistic logic and classic logi

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

On Sun, 2007-10-14 at 17:19 -1000, Tim Newsham wrote: > On Sun, 14 Oct 2007, Roberto Zunino wrote: > > (Warning: wild guess follows, I can not completely follow CPS ;-)) > > Adding a couple of forall's makes it compile: > > propCC :: ((forall q . p -> Prop r q) -> Prop r p) -> Prop r p > > func1 ::

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

On Sun, 14 Oct 2007, Roberto Zunino wrote: (Warning: wild guess follows, I can not completely follow CPS ;-)) Adding a couple of forall's makes it compile: propCC :: ((forall q . p -> Prop r q) -> Prop r p) -> Prop r p func1 :: (forall q . Or r p (Not r p) -> Prop r q) -> Prop r (Or r p (Not

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

You realize that Djinn can write all that code for you? :) Well, not with your encoding of Not, but with a similar one. -- Lennart 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

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 <[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.

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

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

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

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.