{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeOperators #-}
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))
data IsUnion x y z = IsUnion
{
IsUnion x y z -> Sub x z
inl :: !(Sub x z),
IsUnion x y z -> Sub y z
inr :: !(Sub 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
}
withUnion :: Related x y -> (forall xy. IsUnion x y xy -> r) -> r
withUnion :: 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 :: forall x y z.
Sub x z
-> Sub y z
-> (forall r. Sub x r -> Sub y r -> Sub z r)
-> IsUnion x y z
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 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 = forall r. Sub x r -> Sub y r -> Sub y r
seq }
unique :: IsUnion x y z -> IsUnion x y z' -> Coercion z z'
unique :: 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 -> Sub x z' -> Sub y z' -> Sub z z'
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' -> Sub x z -> Sub y z -> Sub z' z
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))
greater :: Sub x y -> IsUnion x y y
greater :: Sub x y -> IsUnion x y y
greater Sub x y
l = IsUnion :: forall x y z.
Sub x z
-> Sub y z
-> (forall r. Sub x r -> Sub y r -> Sub z r)
-> IsUnion x y z
IsUnion{ inl :: Sub x y
inl = Sub x y
l, inr :: Sub y y
inr = Sub y y
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=forall r. Sub x r -> Sub y r -> Sub y r
seq }
idemp :: IsUnion x x x
idemp :: 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 k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
commutative :: IsUnion x y z -> IsUnion y x z
commutative :: IsUnion x y z -> IsUnion y x z
commutative IsUnion x y z
xyz = IsUnion :: forall x y z.
Sub x z
-> Sub y z
-> (forall r. Sub x r -> Sub y r -> Sub z r)
-> IsUnion x y z
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) }
associative :: 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 xy'z
-> IsUnion y z yz
-> IsUnion x yz x'yz
-> Coercion xy'z x'yz
associative IsUnion x y xy
xy IsUnion xy z xy'z
xy'z IsUnion y z yz
yz IsUnion x yz x'yz
x'yz =
Sub xy'z x'yz -> Sub x'yz xy'z -> Coercion xy'z x'yz
forall k (a :: k) (b :: k). Sub a b -> Sub b a -> Coercion a b
equiv (IsUnion xy z xy'z -> Sub xy x'yz -> Sub z x'yz -> Sub xy'z x'yz
forall x y z.
IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
elim IsUnion xy z xy'z
xy'z (IsUnion x y xy -> Sub x x'yz -> Sub y x'yz -> Sub xy x'yz
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 (IsUnion x yz x'yz -> Sub x x'yz
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion x yz x'yz
x'yz) (IsUnion x yz x'yz -> Sub yz x'yz
forall x y z. IsUnion x y z -> Sub y z
inr IsUnion x yz x'yz
x'yz Sub yz x'yz -> Sub y yz -> Sub y x'yz
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)) (IsUnion x yz x'yz -> Sub yz x'yz
forall x y z. IsUnion x y z -> Sub y z
inr IsUnion x yz x'yz
x'yz Sub yz x'yz -> Sub z yz -> Sub z x'yz
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))
(IsUnion x yz x'yz -> Sub x xy'z -> Sub yz xy'z -> Sub x'yz xy'z
forall x y z.
IsUnion x y z -> forall r. Sub x r -> Sub y r -> Sub z r
elim IsUnion x yz x'yz
x'yz (IsUnion xy z xy'z -> Sub xy xy'z
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion xy z xy'z
xy'z Sub xy xy'z -> Sub x xy -> Sub x xy'z
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) (IsUnion y z yz -> Sub y xy'z -> Sub z xy'z -> Sub yz xy'z
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 xy'z -> Sub xy xy'z
forall x y z. IsUnion x y z -> Sub x z
inl IsUnion xy z xy'z
xy'z Sub xy xy'z -> Sub y xy -> Sub y xy'z
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 xy'z -> Sub z xy'z
forall x y z. IsUnion x y z -> Sub y z
inr IsUnion xy z xy'z
xy'z)))