<br><br><div class="gmail_quote">On Mon, Aug 13, 2012 at 6:53 PM, Alexander Solla <span dir="ltr">&lt;<a href="mailto:alex.solla@gmail.com" target="_blank">alex.solla@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="gmail_quote"><div>In a classical logic, the duality is expressed by !E! = A, and !A! = E, where E and A are backwards/upsidedown and ! represents negation.  In particular, for a proposition P,</div>
<div><br></div><div>Ex Px &lt;=&gt; !Ax! Px (not all x&#39;s are not P)</div><div>and</div><div>Ax Px &lt;=&gt; !Ex! Px (there does not exist an x which is not P)</div><div><br></div><div>Negation is relatively tricky to represent in a constructive logic -- hence the use of functions/implications and bottoms/contradictions.  The type ConcreteType -&gt; b represents the negation of ConcreteType, because it shows that ConcreteType &quot;implies the contradiction&quot;.</div>

<div><br></div><div>Put these ideas together, and you will recover the duality as expressed earlier.</div><div><div class="h5"><div></div></div></div></div></blockquote><div><br>I&#39;d been looking for a good explanation of how to get from Ex Px to !Ax! Px in constructive logic, and this is basically it.  What is said here is actually a slightly different statement, which is what had me confused!<br>
<br>If you do the naive encoding, you get something like<br><br>-- This is my favorite representation of &quot;Contradiction&quot; in Haskell, since<br>-- it has reductio ad absurdum encoded directly in the type<br>-- and only requires Rank2Types.<br>
newtype Contradiction = Bottom { absurd :: forall a. a }<br>-- absurd :: forall a. Contradiction -&gt; a<br><br>type Not a = a -&gt; Contradiction<br>newtype NotC (c :: * -&gt; Constraint) = MkNotC { unNotC :: forall a. c a =&gt; Not a }<br>
type UselessExists (c :: * -&gt; Constraint) = Not (NotC c)<br>-- here I&#39;m using ConstraintKinds as, in a sense, the &#39;most generic&#39; way of specifying a type-level predicate,<br>-- at least in bleeding edge Haskell.  It&#39;s trivial to make a less generic version for any particular constraint<br>
-- you care about without going quite so overboard on type system extensions :)<br>-- i.e.<br>--     newtype NoShow = MkNoShow {  unNoShow :: forall a. Show a =&gt; Not a }<br>--     type UselessExistsShow = Not NoShow<br>
<br>-- A simple example: there is a type that is equal to Bool:<br>

silly :: UselessExists ((~) Bool)<br>
silly (MkNotC k) = k True<br><br>-- need silly :: NotC ((~) Bool) -&gt; Contradiction<br>-- after pattern matching on MkNotC<br>-- k :: forall a. (a ~ Bool) =&gt; a -&gt; Contradiction<br>-- i.e. k :: Bool -&gt; Contradiction<br>
-- therefore, k True :: Contradiction.<br>

<br>    This type is useless, however; NotC c isn&#39;t usefully inhabited at any reasonable c -- there&#39;s no way to actually call it!<br><br>    The magic comes when you unify the &#39;return type&#39; from the two Nots instead of using bottoms as a catch-all... I guess this is the CPS translation of negation?<br>
<br>type NotR r a = a -&gt; r<br>newtype NotRC r (c :: * -&gt; Constraint) = MkNotRC { unNotRC :: forall a. c a =&gt; NotR r a }<br>-- MkNotRC :: forall r c. (forall a. c a =&gt; a -&gt; r) -&gt; NotRC r<br><br>type ExistsR r (c :: * -&gt; Constraint) = NotR r (NotRC r c)<br>
-- ~= c a =&gt; (a -&gt; r) -&gt; r<br><br>newtype Exists (c :: * -&gt; Constraint) = MkExists { unExists :: forall r. ExistsR r c }<br>-- MkExists :: forall c. (forall r. NotR r (NotRC r c)) -&gt; Exists c<br>-- ~= forall c. (forall r. c a =&gt; (a -&gt; r) -&gt; r) -&gt; Exists c<br>
</div></div><br>-- A simple example: there is a type that is equal to Bool:<br>

silly2 :: Exists ((~) Bool)<br>
silly2 = MkExists (\(MkNotRC k) -&gt; k False)<br>
<br>    This version allows you to specify the type of &#39;absurd&#39; result you want, and use that to let the witness of existence escape out via whatever interface the provided constraint gives.<br><br>caseExists :: (forall a. c a =&gt; a -&gt; r)  -&gt; Exists c -&gt; r<br>
caseExists k (MkExists f) = f (MkNotRC k)<br><br>main = putStrLn $ caseExists show silly2<br>-- should print &quot;False&quot;<br><br><br>