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

[Derek Elkins]

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.