[Haskell-cafe] haskell-curry, classical logic, excluded middle
Derek Elkins
derek.a.elkins at gmail.com
Sun Oct 14 23:37:03 EDT 2007
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 :: (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)
This interesting paper,
http://pllab.is.ocha.ac.jp/~asai/papers/tr07-1abs.html
suggests that that might actually not be ideal.
More information about the Haskell-Cafe
mailing list