{-# 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(..))
data IsUnion x y z = IsUnion
{
forall x y z. IsUnion x y z -> Sub x z
inl :: !(Sub x z),
forall x y z. IsUnion x y z -> Sub y z
inr :: !(Sub y 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
}
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 = forall a. a -> Maybe a
Just (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)
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 =
forall xy. IsUnion x y xy -> r
body IsUnion{ inl :: Sub x y
inl = forall {k} (a :: k) (b :: k). Coercible a b => Sub a b
sub, inr :: Sub y y
inr = 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 = seq :: forall a b. a -> b -> b
seq }
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' = forall {k} (a :: k) (b :: k). Sub a b -> Sub b a -> Coercion a b
equiv (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 (forall x y z. IsUnion x y z -> Sub x z
inl IsUnion x y z'
xy') (forall x y z. IsUnion x y z -> Sub y z
inr IsUnion x y z'
xy')) (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' (forall x y z. IsUnion x y z -> Sub x z
inl IsUnion x y z
xy) (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 :: 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 = 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=seq :: forall a b. a -> b -> b
seq }
idemp :: IsUnion x x x
idemp :: forall x. IsUnion x x x
idemp = forall x y. Sub x y -> IsUnion x y y
greater forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
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 = forall x y z. IsUnion x y z -> Sub y z
inr IsUnion x y z
xyz, inr :: Sub x z
inr = 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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip (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 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 = forall x y z. IsUnion x y z -> Sub x z
inl IsUnion xy z xyz
xy'z forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall x y z. IsUnion x y z -> Sub x z
inl IsUnion x y xy
xy
, inr :: Sub yz xyz
inr = 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 (forall x y z. IsUnion x y z -> Sub x z
inl IsUnion xy z xyz
xy'z forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall x y z. IsUnion x y z -> Sub y z
inr IsUnion x y xy
xy) (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 -> 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 (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 forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall x y z. IsUnion x y z -> Sub x z
inl IsUnion y z yz
yz)) (Sub yz r
yz_r forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall x y z. IsUnion x y z -> Sub y z
inr IsUnion y z yz
yz)
}