You realize that Djinn can write all that code for you? :) Well, not with your encoding of Not, but with a similar one.
-- Lennart On 10/14/07, Tim Newsham <[EMAIL PROTECTED]> wrote: > > 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/ > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe