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

Tim Newsham newsham at lava.net
Sun Oct 14 23:19:59 EDT 2007

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

More information about the Haskell-Cafe mailing list