{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
module Newtype.Union(
  module Data.Type.Coercion.Related,
  IsUnion(..),

  withUnion,
  
  unique, greater, idemp, commutative, associative
) where

import Prelude hiding (id, (.))
import Control.Category
import Data.Type.Coercion.Sub (sub, equiv)
import Data.Type.Coercion.Sub.Internal
import Data.Type.Coercion.Related
import Data.Type.Coercion.Related.Internal
import Data.Type.Coercion ( Coercion(Coercion), TestCoercion(..))

-- | @IsUnion x y z@ witnesses the fact:
--
--   * All @x, y, z@ share the same runtime representation
--   * @z@ is a union type of @x@ and @y@. In other words, the following three holds:
--
--     * @'Sub' x z@
--     * @Sub y z@
--     * For any type @r@ satisfying both of @(Sub x r, Sub y r)@, @Sub z r@.
data IsUnion x y z = IsUnion
  {
    forall x y z. IsUnion x y z -> Sub x z
inl :: !(Sub x z), -- ^ @x@ can be safely coerced to @z@
    forall x y z. IsUnion x y z -> Sub y z
inr :: !(Sub y z), -- ^ @y@ can be safely coerced to @z@
    forall x y z.
IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
elim :: forall r. Sub x r -> Sub y r -> Sub z r
      -- ^ Given both @x@ and @y@ can be safely coerced to @r@, too @z@ can.
  }

instance Eq (IsUnion x y z) where
  IsUnion x y z
_ == :: IsUnion x y z -> IsUnion x y z -> Bool
== IsUnion x y z
_ = Bool
True
instance Ord (IsUnion x y z) where
  compare :: IsUnion x y z -> IsUnion x y z -> Ordering
compare IsUnion x y z
_ IsUnion x y z
_ = Ordering
EQ

instance TestCoercion (IsUnion x y) where
  testCoercion :: forall a b. IsUnion x y a -> IsUnion x y b -> Maybe (Coercion a b)
testCoercion IsUnion x y a
u1 IsUnion x y b
u2 = Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just (IsUnion x y a -> IsUnion x y b -> Coercion a b
forall x y z z'. IsUnion x y z -> IsUnion x y z' -> Coercion z z'
unique IsUnion x y a
u1 IsUnion x y b
u2)

-- | For a pair of 'Related' types @x@ and @y@, make some (existentially quantified)
--   type @xy@ where @xy@ is a union type of @x, y@.
withUnion :: Related x y -> (forall xy. IsUnion x y xy -> r) -> r
withUnion :: forall x y r. Related x y -> (forall xy. IsUnion x y xy -> r) -> r
withUnion (Related Coercion x y
Coercion) forall xy. IsUnion x y xy -> r
body =
    IsUnion x y y -> r
forall xy. IsUnion x y xy -> r
body IsUnion{ inl :: Sub x y
inl = Sub x y
forall {k} (a :: k) (b :: k). Coercible a b => Sub a b
sub, inr :: Sub y y
inr = Sub y y
forall a. Sub a a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id, elim :: forall r. Sub x r -> Sub y r -> Sub y r
elim = Sub x r -> Sub y r -> Sub y r
forall r. Sub x r -> Sub y r -> Sub y r
forall a b. a -> b -> b
seq }

-- | Two union types @z,z'@ of the same pair of types @x,y@ may be different,
--   but they are equivalent in terms of coercibility.
unique :: IsUnion x y z -> IsUnion x y z' -> Coercion z z'
unique :: forall x y z z'. IsUnion x y z -> IsUnion x y z' -> Coercion z z'
unique IsUnion x y z
xy IsUnion x y z'
xy' = Sub z z' -> Sub z' z -> Coercion z z'
forall {k} (a :: k) (b :: k). Sub a b -> Sub b a -> Coercion a b
equiv (IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
forall x y z.
IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
elim IsUnion x y z
xy (IsUnion x y z' -> Sub x z'
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion x y z'
xy') (IsUnion x y z' -> Sub y z'
forall x y z. IsUnion x y z -> Sub y z
inr IsUnion x y z'
xy')) (IsUnion x y z' -> forall r. Sub x r -> Sub y r -> Sub z' r
forall x y z.
IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
elim IsUnion x y z'
xy' (IsUnion x y z -> Sub x z
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion x y z
xy) (IsUnion x y z -> Sub y z
forall x y z. IsUnion x y z -> Sub y z
inr IsUnion x y z
xy))

-- | When @Sub x y@, @y@ itself is a union type of @x, y@.
greater :: Sub x y -> IsUnion x y y
greater :: forall x y. Sub x y -> IsUnion x y y
greater Sub x y
l = IsUnion{ inl :: Sub x y
inl = Sub x y
l, inr :: Sub y y
inr = Sub y y
forall a. Sub a a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id, elim :: forall r. Sub x r -> Sub y r -> Sub y r
elim=Sub x r -> Sub y r -> Sub y r
forall r. Sub x r -> Sub y r -> Sub y r
forall a b. a -> b -> b
seq }

-- | Union is idempotent.
--
--   Note: combining @idemp@ and 'unique', @IsUnion x x z -> Coercion x z@ holds.
idemp :: IsUnion x x x
idemp :: forall x. IsUnion x x x
idemp = Sub x x -> IsUnion x x x
forall x y. Sub x y -> IsUnion x y y
greater Sub x x
forall a. Sub a a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

-- | Union is commutative.
--
--   Note: combining @commutative@ and 'unique', @IsUnion x y xy -> IsUnion y x yx -> Coercion xy yx@ holds.
commutative :: IsUnion x y z -> IsUnion y x z
commutative :: forall x y z. IsUnion x y z -> IsUnion y x z
commutative IsUnion x y z
xyz = IsUnion{ inl :: Sub y z
inl = IsUnion x y z -> Sub y z
forall x y z. IsUnion x y z -> Sub y z
inr IsUnion x y z
xyz, inr :: Sub x z
inr = IsUnion x y z -> Sub x z
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion x y z
xyz, elim :: forall r. Sub y r -> Sub x r -> Sub z r
elim = (Sub x r -> Sub y r -> Sub z r) -> Sub y r -> Sub x r -> Sub z r
forall a b c. (a -> b -> c) -> b -> a -> c
flip (IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
forall x y z.
IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
elim IsUnion x y z
xyz) }

-- | Union is associative.
--
--   Note: combining @associative@ and 'unique', the following holds.
--   
--   >    IsUnion x y xy -> IsUnion xy z xy'z
--   > -> IsUnion y z yz -> IsUnion x yz x'yz
--   > -> Coercion xy'z x'yz 
associative :: IsUnion x y xy -> IsUnion xy z xyz -> IsUnion y z yz -> IsUnion x yz xyz
associative :: forall x y xy z xyz yz.
IsUnion x y xy
-> IsUnion xy z xyz -> IsUnion y z yz -> IsUnion x yz xyz
associative IsUnion x y xy
xy IsUnion xy z xyz
xy'z IsUnion y z yz
yz =
    IsUnion {
       inl :: Sub x xyz
inl = IsUnion xy z xyz -> Sub xy xyz
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion xy z xyz
xy'z Sub xy xyz -> Sub x xy -> Sub x xyz
forall b c a. Sub b c -> Sub a b -> Sub a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IsUnion x y xy -> Sub x xy
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion x y xy
xy 
     , inr :: Sub yz xyz
inr = IsUnion y z yz -> forall r. Sub y r -> Sub z r -> Sub yz r
forall x y z.
IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
elim IsUnion y z yz
yz (IsUnion xy z xyz -> Sub xy xyz
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion xy z xyz
xy'z Sub xy xyz -> Sub y xy -> Sub y xyz
forall b c a. Sub b c -> Sub a b -> Sub a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IsUnion x y xy -> Sub y xy
forall x y z. IsUnion x y z -> Sub y z
inr IsUnion x y xy
xy) (IsUnion xy z xyz -> Sub z xyz
forall x y z. IsUnion x y z -> Sub y z
inr IsUnion xy z xyz
xy'z)
     , elim :: forall r. Sub x r -> Sub yz r -> Sub xyz r
elim = \Sub x r
x_r Sub yz r
yz_r -> IsUnion xy z xyz -> forall r. Sub xy r -> Sub z r -> Sub xyz r
forall x y z.
IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
elim IsUnion xy z xyz
xy'z (IsUnion x y xy -> forall r. Sub x r -> Sub y r -> Sub xy r
forall x y z.
IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
elim IsUnion x y xy
xy Sub x r
x_r (Sub yz r
yz_r Sub yz r -> Sub y yz -> Sub y r
forall b c a. Sub b c -> Sub a b -> Sub a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IsUnion y z yz -> Sub y yz
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion y z yz
yz)) (Sub yz r
yz_r Sub yz r -> Sub z yz -> Sub z r
forall b c a. Sub b c -> Sub a b -> Sub a c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IsUnion y z yz -> Sub z yz
forall x y z. IsUnion x y z -> Sub y z
inr IsUnion y z yz
yz)
    }