On Mon, Aug 13, 2012 at 6:53 PM, Alexander Solla <alex.solla@gmail.com> wrote:
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,

Ex Px <=> !Ax! Px (not all x's are not P)
and
Ax Px <=> !Ex! Px (there does not exist an x which is not P)

Negation is relatively tricky to represent in a constructive logic -- hence the use of functions/implications and bottoms/contradictions.  The type ConcreteType -> b represents the negation of ConcreteType, because it shows that ConcreteType "implies the contradiction".

Put these ideas together, and you will recover the duality as expressed earlier.

I'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!

If you do the naive encoding, you get something like

-- This is my favorite representation of "Contradiction" in Haskell, since
-- it has reductio ad absurdum encoded directly in the type
-- and only requires Rank2Types.
newtype Contradiction = Bottom { absurd :: forall a. a }
-- absurd :: forall a. Contradiction -> a

type Not a = a -> Contradiction
newtype NotC (c :: * -> Constraint) = MkNotC { unNotC :: forall a. c a => Not a }
type UselessExists (c :: * -> Constraint) = Not (NotC c)
-- here I'm using ConstraintKinds as, in a sense, the 'most generic' way of specifying a type-level predicate,
-- at least in bleeding edge Haskell.  It's trivial to make a less generic version for any particular constraint
-- you care about without going quite so overboard on type system extensions :)
-- i.e.
--     newtype NoShow = MkNoShow {  unNoShow :: forall a. Show a => Not a }
--     type UselessExistsShow = Not NoShow

-- A simple example: there is a type that is equal to Bool:
silly :: UselessExists ((~) Bool)
silly (MkNotC k) = k True

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

    This type is useless, however; NotC c isn't usefully inhabited at any reasonable c -- there's no way to actually call it!

    The magic comes when you unify the 'return type' from the two Nots instead of using bottoms as a catch-all... I guess this is the CPS translation of negation?

type NotR r a = a -> r
newtype NotRC r (c :: * -> Constraint) = MkNotRC { unNotRC :: forall a. c a => NotR r a }
-- MkNotRC :: forall r c. (forall a. c a => a -> r) -> NotRC r

type ExistsR r (c :: * -> Constraint) = NotR r (NotRC r c)
-- ~= c a => (a -> r) -> r

newtype Exists (c :: * -> Constraint) = MkExists { unExists :: forall r. ExistsR r c }
-- MkExists :: forall c. (forall r. NotR r (NotRC r c)) -> Exists c
-- ~= forall c. (forall r. c a => (a -> r) -> r) -> Exists c

-- A simple example: there is a type that is equal to Bool:
silly2 :: Exists ((~) Bool)
silly2 = MkExists (\(MkNotRC k) -> k False)

    This version allows you to specify the type of 'absurd' result you want, and use that to let the witness of existence escape out via whatever interface the provided constraint gives.

caseExists :: (forall a. c a => a -> r)  -> Exists c -> r
caseExists k (MkExists f) = f (MkNotRC k)

main = putStrLn $ caseExists show silly2
-- should print "False"