[Haskell-cafe] Data structure containing elements which are instances of the same type class

[Ryan Ingram]

On Mon, Aug 13, 2012 at 6:53 PM, Alexander Solla <alex.solla at 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"
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120814/1e16c69a/attachment.htm>