You realize that Djinn can write all that code for you? :)<br>Well, not with your encoding of Not, but with a similar one.<br><br>&nbsp; -- Lennart<br><br><div><span class="gmail_quote">On 10/14/07, <b class="gmail_sendername">
Tim Newsham</b> &lt;<a href="mailto:newsham@lava.net">newsham@lava.net</a>&gt; wrote:</span><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
I&#39;ve been struggling with this for the last day and a half.&nbsp;&nbsp;I&#39;m<br>trying to get some exercise with the type system and with logic by<br>playing with the curry-howard correspondence.&nbsp;&nbsp;I got stuck on<br>the excluded-middle, and I think now I got it almost all the way
<br>there, but its still not quite right.&nbsp;&nbsp;Is this error I&#39;m getting<br>(inline at the end) easily fixed, and what exactly is going on?<br><br>---- code ---<br>{-# OPTIONS_GHC -fglasgow-exts #-}<br>module Classic where
<br>{-<br>Classic logic.&nbsp;&nbsp;(See Intuit.hs first).<br>In this system propositions all take a continuation.&nbsp;&nbsp;This allows<br>us to define the law of the excluded middle.<br>-}<br>import Control.Monad<br><br><br>-- propositions are functions taking a continuation.
<br>data Prop r p = Prop ((p -&gt; r) -&gt; r)<br>run :: Prop r p -&gt; (p -&gt; r) -&gt; r<br>run (Prop f) k = f k<br>propCC :: ((p -&gt; Prop r q) -&gt; Prop r p) -&gt; Prop r p<br>propCC f = Prop (\k -&gt; run (f (\a -&gt; Prop (\k&#39; -&gt; k a))) k)
<br>instance Monad (Prop r) where<br>&nbsp;&nbsp;&nbsp;&nbsp; return p = Prop (\c -&gt; c p)<br>&nbsp;&nbsp;&nbsp;&nbsp; p &gt;&gt;= mkq = Prop (\c -&gt; run p (\r -&gt; run (mkq r) c))<br><br><br>data TRUTH = TRUTH<br>type FALSE r = Not r TRUTH<br>data And r p q = And (Prop r p) (Prop r q)
<br>data Or r p q = OrL (Prop r p) | OrR (Prop r q)<br>data Imp r p q = Imp (Prop r p -&gt; Prop r q)<br>data Equiv r p q = Equiv (Prop r p -&gt; Prop r q) (Prop r q -&gt; Prop r p)<br>data Not r p = Not (forall q. (Prop r p -&gt; Prop r q))
<br><br><br>-- Truth<br>truth :: Prop r TRUTH<br>truth = return TRUTH<br><br>-- And-Injection<br>-- P, Q |- P /\ Q<br>andInj :: Prop r p -&gt; Prop r q -&gt; Prop r (And r p q)<br>andInj p q = return (And p q)<br><br>-- And-Elimination, left and Right
<br>-- P /\ Q |- P<br>andElimL :: Prop r (And r p q) -&gt; Prop r p<br>andElimL pq = pq &gt;&gt;= \(And p q) -&gt; p<br>-- P /\ Q |- Q<br>andElimR :: Prop r (And r p q) -&gt; Prop r q<br>andElimR pq = pq &gt;&gt;= \(And p q) -&gt; q
<br><br>-- Or-Injection, left and right<br>-- P |- P \/ Q<br>orInjL :: Prop r p -&gt; Prop r (Or r p q)<br>orInjL p = return (OrL p)<br>-- Q |- P \/ Q<br>orInjR :: Prop r q -&gt; Prop r (Or r p q)<br>orInjR q = return (OrR q)
<br><br>-- Or-Elimination.<br>-- P \/ Q, P -&gt; R, Q -&gt; R |- R<br>orElim :: Prop r (Or r p q) -&gt; (Prop r p -&gt; Prop r s) -&gt; (Prop r q -&gt; Prop r s) -&gt; Prop r s<br>orElim pORq p2r q2r = pORq &gt;&gt;= byCases
<br>&nbsp;&nbsp; where byCases (OrL p) = p2r p<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; byCases (OrR q) = q2r q<br><br>-- Implication-Injection<br>-- (P |- Q) |- P -&gt; Q<br>impInj :: (Prop r p -&gt; Prop r q) -&gt; Prop r (Imp r p q)<br>impInj p2q = return (Imp p2q)
<br><br>-- Implication-elimination (modus ponen)<br>-- P, P -&gt; Q |- Q<br>impElim :: Prop r p -&gt; Prop r (Imp r p q) -&gt; Prop r q<br>impElim p pIMPq = pIMPq &gt;&gt;= \(Imp p2q) -&gt; p2q p<br><br>-- Equivalence-Injection
<br>-- P -&gt; Q, Q -&gt; P |- P = Q<br>equivInj :: Prop r (Imp r p q) -&gt; Prop r (Imp r q p) -&gt; Prop r (Equiv r p q)<br>equivInj pIMPq qIMPp = do<br>&nbsp;&nbsp;&nbsp;&nbsp; (Imp p2q) &lt;- pIMPq<br>&nbsp;&nbsp;&nbsp;&nbsp; (Imp q2p) &lt;- qIMPp<br>&nbsp;&nbsp;&nbsp;&nbsp; return (Equiv p2q q2p)
<br><br>-- Equivalence-Elimination, Left and Right<br>-- P = Q |- P -&gt; Q<br>equivElimL :: Prop r (Equiv r p q) -&gt; Prop r (Imp r p q)<br>equivElimL pEQq = pEQq &gt;&gt;= \(Equiv p2q q2p) -&gt; return (Imp p2q)<br>equivElimR :: Prop r (Equiv r p q) -&gt; Prop r (Imp r q p)
<br>equivElimR pEQq = pEQq &gt;&gt;= \(Equiv p2q q2p) -&gt; return (Imp q2p)<br><br>-- Absurdity<br>-- False |- P<br>absurd :: Prop r (FALSE r) -&gt; Prop r p<br>absurd false = false &gt;&gt;= \(Not true2p) -&gt; true2p truth
<br><br>-- Not-Inj<br>-- (P |- False) |- ~P<br>notInj :: forall r p. (Prop r p -&gt; Prop r (FALSE r)) -&gt; Prop r (Not r p)<br>notInj p2false = return (Not p2any)<br>&nbsp;&nbsp; where p2any :: forall q. Prop r p -&gt; Prop r q<br>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; p2any assumep = absurd (p2false assumep)<br><br>-- Not-Elimination<br>-- P, ~P |- Q<br>notElim :: Prop r p -&gt; Prop r (Not r p) -&gt; Prop r q<br>notElim p np = np &gt;&gt;= \(Not p2any) -&gt; p2any p<br><br><br>
-- Excluded-Middle<br>-- P \/ ~P<br>exclMiddle :: forall r p. Prop r (Or r p (Not r p))<br>exclMiddle = propCC func1<br>&nbsp;&nbsp; where func1 :: (Or r p (Not r p) -&gt; Prop r q) -&gt; Prop r (Or r p (Not r p))<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; -- k&nbsp;&nbsp;:: Or r p (Not r p) -&gt; Prop r q
<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; func1 k = return (OrR (return (Not func2)))<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; where func2 :: Prop r p -&gt; Prop r q<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; func2 k&#39; = k (OrL k&#39;)<br><br>{-<br><a href="http://www.cse.ogi.edu/~magnus/mdo-callcc-slides.pdf">
http://www.cse.ogi.edu/~magnus/mdo-callcc-slides.pdf</a><br>-- A \/ ~A<br>excmid :: Either a (a -&gt; b)<br>excmid = callcc (\k. Right (\a.k (Left a)))<br>-}<br><br>{-<br>Classic2.hs:114:27:<br>&nbsp;&nbsp;&nbsp;&nbsp; Couldn&#39;t match expected type `q&#39; (a rigid variable)
<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;against inferred type `q1&#39; (a rigid variable)<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; `q&#39; is bound by the type signature for `func2&#39;<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; at Classic2.hs:113:44<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; `q1&#39; is bound by the type signature for `func1&#39;
<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; at Classic2.hs:110:45<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Expected type: Prop r q<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Inferred type: Prop r q1<br>&nbsp;&nbsp;&nbsp;&nbsp; In the expression: k (OrL k&#39;)<br>&nbsp;&nbsp;&nbsp;&nbsp; In the definition of `func2&#39;: func2 k&#39; = k (OrL k&#39;)<br>
-}<br><br><br>-- False-Elimination<br>-- (~P |- False) |- P<br><br>Tim Newsham<br><a href="http://www.thenewsh.com/~newsham/">http://www.thenewsh.com/~newsham/</a><br>_______________________________________________<br>Haskell-Cafe mailing list
<br><a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br><a href="http://www.haskell.org/mailman/listinfo/haskell-cafe">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br></blockquote></div><br>