{-# OPTIONS_GHC -fglasgow-exts #-}

module Isomorphism where

{- Proof of isomorphism of \exists t . a t and \exists . b t
   by the relation f.
   A relation is an isomorphism if it is
   * a function
   * total
   * injective
   * surjective
-}

data Iso a b = forall f . Iso (Function f a b)
                              (Total f a b)
                              (Injective f a b)
                              (Surjective f a b)

-- A relation is a function if equal preimages map to equal results.
type Function f a b = 
    forall p q r . f (a p) (b q) -> f (a p) (b r) -> Equal q r

-- A function is total if there is some image for every value in the domain
type Total f a b = forall n . a n -> SomeImage f (a n) b
{- Haskell doesn't have first class existentials, so we wrap this one up
   in a data type. We could use the CPS-style equivalent to existentials:
   type SomeImage f an b = forall x . (forall m . f an (b m) -> x) -> x
   but it's a pain to work with when using type inference.
-}
data SomeImage f an b = 
    forall m . SomeImage    (f  an   (b m))

-- A total function is injective when each value in the codomain has
-- only one preimage.
type Injective f a b = 
    forall p q r . f (a p) (b q) -> f (a r) (b q) -> Equal p r

-- A total injective function is surjective when each value in the
-- codomain has a preimage.
type Surjective f a b = forall m . b m -> SomePreImage f a (b m)
data SomePreImage f a bm = 
    forall n . SomePreImage (f (a n)  bm)

data Equal a b where
    Equal :: Equal a a

-- We first show that a type is isomorphic to itself
eqIso :: Iso a a
eqIso = Iso eqRightInv (const $ SomeImage    Equal)
            eqLeftInv  (const $ SomePreImage Equal)

-- The relation /Equal/ is the isomorphism.
-- It is it's own left and its own right inverse.
eqRightInv :: Equal (a p) (b q) -> Equal (a p) (b r) -> Equal q r
eqRightInv Equal Equal = Equal
eqLeftInv :: Equal (a p) (b q) -> Equal (a r) (b q) -> Equal p r
eqLeftInv Equal Equal = Equal

-- Phantom types with only one constructor are isomorphic
phantomIso :: Iso Phantom1 Phantom2
phantomIso = Iso phantomRightInv (const $ SomeImage    PhantomEqual)
                 phantomLeftInv  (const $ SomePreImage PhantomEqual)

data Phantom1 a = Phantom1
data Phantom2 a = Phantom2

data PhantomEqual a b where
    PhantomEqual :: PhantomEqual (Phantom1 a) (Phantom2 a)

phantomLeftInv :: PhantomEqual (a p) (b q) -> PhantomEqual (a r) (b q) -> Equal p r
phantomLeftInv PhantomEqual PhantomEqual = Equal
phantomRightInv :: PhantomEqual (a p) (b q) -> PhantomEqual (a p) (b r) -> Equal q r
phantomRightInv PhantomEqual PhantomEqual = Equal

-- Finally, we show that the unary and binary representations of the 
-- natural numbers are isomorphic

data Z
data S n

data Unary n where
    Z :: Unary Z
    S :: Unary n -> Unary (S n)

data Zero
data Even n
data Odd n

data Binary n where
    Zero :: Binary Zero
    -- Left shift, then add one:
    Odd  :: Binary n -> Binary (Odd n)
    -- We can only left shift (without adding one) on non-zero
    -- natural numbers. We don't want /00/ and /0/ to both have
    -- representations.
    Quad :: Binary (Even n) -> Binary (Even (Even n))
    Even :: Binary (Odd n)  -> Binary (Even (Odd n))

-- The isomorphism:
data Ary a b where
    -- case 0:
    ZZ :: Ary (Unary Z) (Binary Zero)
    -- case 1:
    OO :: Ary (Unary (S Z)) (Binary (Odd Zero))
    -- if a number is even, adding one just increments the least-significant digit
    S0 :: Ary (Unary n) (Binary (Even m)) ->
          Ary (Unary (S n)) (Binary (Odd m))
    -- if a number is odd, we change the least-significant bit to 0, 
    -- then carry the 1. We do this by adding one to the higher-order
    -- bits of the odd number, then setting the low bit to zero. This
    -- adds two and subtracts 1.
    S1 :: Ary (Unary (S n)) (Binary (Odd m)) -> 
          Ary (Unary o)     (Binary m) ->
          Ary (Unary (S o)) (Binary p) ->
          Ary (Unary (S (S n))) (Binary (Even p))

-- Surjectivity:
surjectAry :: Binary n -> SomePreImage Ary Unary (Binary n)
surjectAry Zero = SomePreImage ZZ
surjectAry (Odd Zero) = SomePreImage OO
surjectAry (Odd (Odd n)) = 
    case surjectAry (Even (Odd n)) of
      SomePreImage a -> SomePreImage (S0 a)
surjectAry (Odd (Even n)) = 
    case surjectAry (Quad (Even n)) of
      SomePreImage a -> SomePreImage (S0 a)
surjectAry (Odd (Quad n)) = 
    case surjectAry (Quad (Quad n)) of
      SomePreImage a -> SomePreImage (S0 a)
surjectAry (Even (Odd Zero)) = 
    SomePreImage (S1 OO ZZ OO)
surjectAry (Even (Odd (Odd n))) = 
    case surjectAry (Odd (Odd n)) of
      SomePreImage a@(S0 b) -> 
          case surjectAry (Odd (Even (Odd n))) of
            SomePreImage c@(S0 d) -> SomePreImage (S1 c b a)
surjectAry (Even (Odd (Even n))) = 
    case surjectAry (Odd (Even n)) of
      SomePreImage a@(S0 b) -> 
          case surjectAry (Odd (Quad (Even n))) of
            SomePreImage c@(S0 d) -> SomePreImage (S1 c b a)
surjectAry (Even (Odd (Quad n))) = 
    case surjectAry (Odd (Quad n)) of
      SomePreImage a@(S0 b) -> 
          case surjectAry (Odd (Quad (Quad n))) of
            SomePreImage c@(S0 d) -> SomePreImage (S1 c b a)

-- Total:
totalAry :: Unary n -> SomeImage Ary (Unary n) Binary
totalAry Z = SomeImage ZZ
totalAry (S Z) = SomeImage OO
totalAry (S (S n)) = 
    case totalAry n of
      SomeImage c -> incTwice c SomeImage

-- The helper function incTwice uses the CPS-style existentials,
-- since we want more detailed types from it: adding two to an odd number
-- gives an Odd number, for instance. 
incTwice :: Ary (Unary n) (Binary m) -> (forall o . Ary (Unary (S (S n))) (Binary o) -> x) -> x
incTwice ZZ f = incTwiceZero ZZ f
incTwice OO f = incTwiceOdd OO f
incTwice a@(S0 _) f = incTwiceOdd a f
incTwice a@(S1 _ _ _) f = incTwiceEven a f

incTwiceOdd :: Ary (Unary (S n)) (Binary (Odd m)) -> (forall o . Ary (Unary (S (S (S n)))) (Binary (Odd o)) -> x) -> x
incTwiceOdd OO f = f (S0 (S1 OO ZZ OO))
incTwiceOdd (S0 b@(S1 _ _ _)) f = (incTwiceEven b (f . S0))

incTwiceEven :: Ary (Unary n) (Binary (Even m)) -> (forall o . Ary (Unary (S (S n))) (Binary (Even o)) -> x) -> x
incTwiceEven a@(S1 _ c@ZZ d) f = incTwiceZero c (\e -> f (S1 (S0 a) d e))
incTwiceEven a@(S1 _ c@OO d) f = incTwiceOdd c (\e -> f (S1 (S0 a) d e))
incTwiceEven a@(S1 _ c@(S1 _ _ _) d) f = incTwiceEven c (\e -> f (S1 (S0 a) d e))
incTwiceEven a@(S1 _ c@(S0 _) d) f = incTwiceOdd c (\e -> f (S1 (S0 a) d e))

incTwiceZero :: Ary (Unary n) (Binary Zero) -> (forall o . Ary (Unary (S (S n))) (Binary (Even o)) -> x) -> x
incTwiceZero ZZ f = f (S1 OO ZZ OO)

-- Injective:
invAry :: Ary (Unary p) (Binary q) -> Ary (Unary r) (Binary q) -> Equal p r
invAry ZZ ZZ = Equal
invAry OO OO = Equal
invAry (S0 b) (S0 d) = 
    case invAry b d of
      Equal -> Equal
invAry (S1 b c d) (S1 b' c' d') = 
    case invAry d d' of
      Equal -> case invAry' c c' of
                 Equal -> case invAry b b' of
                            Equal -> Equal

-- Function:
invAry' :: Ary (Unary p) (Binary q) -> Ary (Unary p) (Binary r) -> Equal q r
invAry' ZZ ZZ = Equal
invAry' OO OO = Equal
invAry' (S0 b) (S0 d) = 
    case invAry' b d of
      Equal -> Equal
invAry' (S1 b c d) (S1 b' c' d') = 
    case invAry' b b' of
      Equal -> case invAry c c' of
                 Equal -> case invAry' d d' of
                            Equal -> Equal

isoAry = Iso invAry' totalAry invAry surjectAry

-- A few examples of proof terms of the isomorphism

zero = ZZ
one = OO
two = S1 one zero one
three = S0 two
four = S1 three one two
five = S0 four
six = S1 five two three
seven = S0 six
eight = S1 seven three four
nine = S0 eight
ten = S1 nine four five