[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
http://www.thenewsh.com/~newsham/
More information about the Haskell-Cafe
mailing list