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

[Tim Newsham]

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 r p))

Yup!  That did it, thanks!

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):

   data Prop p = Prop (forall r. (p -> r) -> r)
   run :: Prop p -> (p -> r) -> r
   run (Prop f) k = f k
   propCC :: ((forall q. p -> Prop q) -> Prop p) -> Prop p
   propCC f = Prop (\k -> run (f (\a -> Prop (\k' -> k a))) k)

> Zun.

Tim Newsham
http://www.thenewsh.com/~newsham/