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

[Tim Newsham]

I've been struggling with this for the last day and a half.  I'm
trying to get some exercise with the type system and with logic by
playing with the curry-howard correspondence.  I got stuck on
the excluded-middle, and I think now I got it almost all the way
there, but its still not quite right.  Is this error I'm getting
(inline at the end) easily fixed, and what exactly is going on?

---- code ---
{-# OPTIONS_GHC -fglasgow-exts #-}
module Classic where
{-
Classic logic.  (See Intuit.hs first).
In this system propositions all take a continuation.  This allows
us to define the law of the excluded middle.
-}
import Control.Monad


-- propositions are functions taking a continuation.
data Prop r p = Prop ((p -> r) -> r)
run :: Prop r p -> (p -> r) -> r
run (Prop f) k = f k
propCC :: ((p -> Prop r q) -> Prop r p) -> Prop r p
propCC f = Prop (\k -> run (f (\a -> Prop (\k' -> k a))) k)
instance Monad (Prop r) where
     return p = Prop (\c -> c p)
     p >>= mkq = Prop (\c -> run p (\r -> run (mkq r) c))


data TRUTH = TRUTH
type FALSE r = Not r TRUTH
data And r p q = And (Prop r p) (Prop r q)
data Or r p q = OrL (Prop r p) | OrR (Prop r q)
data Imp r p q = Imp (Prop r p -> Prop r q)
data Equiv r p q = Equiv (Prop r p -> Prop r q) (Prop r q -> Prop r p)
data Not r p = Not (forall q. (Prop r p -> Prop r q))


-- Truth
truth :: Prop r TRUTH
truth = return TRUTH

-- And-Injection
-- P, Q |- P /\ Q
andInj :: Prop r p -> Prop r q -> Prop r (And r p q)
andInj p q = return (And p q)

-- And-Elimination, left and Right
-- P /\ Q |- P
andElimL :: Prop r (And r p q) -> Prop r p
andElimL pq = pq >>= \(And p q) -> p
-- P /\ Q |- Q
andElimR :: Prop r (And r p q) -> Prop r q
andElimR pq = pq >>= \(And p q) -> q

-- Or-Injection, left and right
-- P |- P \/ Q
orInjL :: Prop r p -> Prop r (Or r p q)
orInjL p = return (OrL p)
-- Q |- P \/ Q
orInjR :: Prop r q -> Prop r (Or r p q)
orInjR q = return (OrR q)

-- Or-Elimination.
-- P \/ Q, P -> R, Q -> R |- R
orElim :: Prop r (Or r p q) -> (Prop r p -> Prop r s) -> (Prop r q -> Prop r s) -> Prop r s
orElim pORq p2r q2r = pORq >>= byCases
   where byCases (OrL p) = p2r p
         byCases (OrR q) = q2r q

-- Implication-Injection
-- (P |- Q) |- P -> Q
impInj :: (Prop r p -> Prop r q) -> Prop r (Imp r p q)
impInj p2q = return (Imp p2q)

-- Implication-elimination (modus ponen)
-- P, P -> Q |- Q
impElim :: Prop r p -> Prop r (Imp r p q) -> Prop r q
impElim p pIMPq = pIMPq >>= \(Imp p2q) -> p2q p

-- Equivalence-Injection
-- P -> Q, Q -> P |- P = Q
equivInj :: Prop r (Imp r p q) -> Prop r (Imp r q p) -> Prop r (Equiv r p q)
equivInj pIMPq qIMPp = do
     (Imp p2q) <- pIMPq
     (Imp q2p) <- qIMPp
     return (Equiv p2q q2p)

-- Equivalence-Elimination, Left and Right
-- P = Q |- P -> Q
equivElimL :: Prop r (Equiv r p q) -> Prop r (Imp r p q)
equivElimL pEQq = pEQq >>= \(Equiv p2q q2p) -> return (Imp p2q)
equivElimR :: Prop r (Equiv r p q) -> Prop r (Imp r q p)
equivElimR pEQq = pEQq >>= \(Equiv p2q q2p) -> return (Imp q2p)

-- Absurdity
-- False |- P
absurd :: Prop r (FALSE r) -> Prop r p
absurd false = false >>= \(Not true2p) -> true2p truth

-- Not-Inj
-- (P |- False) |- ~P
notInj :: forall r p. (Prop r p -> Prop r (FALSE r)) -> Prop r (Not r p)
notInj p2false = return (Not p2any)
   where p2any :: forall q. Prop r p -> Prop r q
         p2any assumep = absurd (p2false assumep)

-- Not-Elimination
-- P, ~P |- Q
notElim :: Prop r p -> Prop r (Not r p) -> Prop r q
notElim p np = np >>= \(Not p2any) -> p2any p


-- Excluded-Middle
-- P \/ ~P
exclMiddle :: forall r p. Prop r (Or r p (Not r p))
exclMiddle = propCC func1
   where func1 :: (Or r p (Not r p) -> Prop r q) -> Prop r (Or r p (Not r p))
         -- k  :: Or r p (Not r p) -> Prop r q
         func1 k = return (OrR (return (Not func2)))
           where func2 :: Prop r p -> Prop r q
                 func2 k' = k (OrL k')

{-
http://www.cse.ogi.edu/~magnus/mdo-callcc-slides.pdf
-- A \/ ~A
excmid :: Either a (a -> b)
excmid = callcc (\k. Right (\a.k (Left a)))
-}

{-
Classic2.hs:114:27:
     Couldn't match expected type `q' (a rigid variable)
            against inferred type `q1' (a rigid variable)
       `q' is bound by the type signature for `func2'
         at Classic2.hs:113:44
       `q1' is bound by the type signature for `func1'
         at Classic2.hs:110:45
       Expected type: Prop r q
       Inferred type: Prop r q1
     In the expression: k (OrL k')
     In the definition of `func2': func2 k' = k (OrL k')
-}


-- False-Elimination
-- (~P |- False) |- P

Tim Newsham
http://www.thenewsh.com/~newsham/