Re: [Haskell-cafe] haskell-curry, classical logic, excluded middle
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/
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.
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):
No answer needed. Duh.. I can just pick "r" to be any type (like "()"). I've got intuitionistic logic and classic logic in haskell types now, using an identical interface/notation (ie. they're swappable for proofs that don't need excluded-middle). The interfaces use infix type names that "read" similarly to their meanings: logic: http://www.thenewsh.com/%7Enewsham/formal/curryhoward/IntLogic.hs http://www.thenewsh.com/%7Enewsham/formal/curryhoward/ClassLogic.hs and example theorems: http://www.thenewsh.com/%7Enewsham/formal/curryhoward/IntTheorems.hs http://www.thenewsh.com/%7Enewsham/formal/curryhoward/ClassTheorems.hs Should this go up on the wiki somewhere? Tim Newsham http://www.thenewsh.com/~newsham/
participants (2)
-
Derek Elkins -
Tim Newsham