{-# LANGUAGE CPP, Rank2Types, ScopedTypeVariables, TypeOperators #-}
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 706
#define LANGUAGE_PolyKinds
{-# LANGUAGE PolyKinds #-}
#endif
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
{-# LANGUAGE RoleAnnotations #-}
#endif
#if defined(__GLASGOW_HASKELL__) && MIN_VERSION_base(4,7,0)
#define HAS_DATA_TYPE_COERCION 1
#endif
{-# LANGUAGE GADTs #-}
module Data.Eq.Type
(
(:=)(..)
, refl
, trans
, symm
, coerce
#ifdef LANGUAGE_PolyKinds
, apply
#endif
, lift
, lift2, lift2'
, lift3, lift3'
, lower
, lower2
, lower3
, fromLeibniz
, toLeibniz
#ifdef HAS_DATA_TYPE_COERCION
, reprLeibniz
#endif
) where
import Prelude (Maybe(..))
import Control.Category
import Data.Semigroupoid
import Data.Groupoid
#ifdef HAS_DATA_TYPE_COERCION
import qualified Data.Type.Coercion as Co
#endif
import qualified Data.Type.Equality as Eq
infixl 4 :=
newtype a := b = Refl { (a := b) -> forall (c :: k -> *). c a -> c b
subst :: forall c. c a -> c b }
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
type role (:=) nominal nominal
#endif
refl :: a := a
refl :: a := a
refl = (forall (c :: k -> *). c a -> c a) -> a := a
forall k (a :: k) (b :: k).
(forall (c :: k -> *). c a -> c b) -> a := b
Refl forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
forall (c :: k -> *). c a -> c a
id
newtype Coerce a = Coerce { Coerce a -> a
uncoerce :: a }
coerce :: a := b -> a -> b
coerce :: (a := b) -> a -> b
coerce a := b
f = Coerce b -> b
forall a. Coerce a -> a
uncoerce (Coerce b -> b) -> (a -> Coerce b) -> a -> b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a := b) -> forall (c :: * -> *). c a -> c b
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
subst a := b
f (Coerce a -> Coerce b) -> (a -> Coerce a) -> a -> Coerce b
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> Coerce a
forall a. a -> Coerce a
Coerce
#ifdef LANGUAGE_PolyKinds
newtype Apply a b f g = Apply { Apply a b f g -> f a := g b
unapply :: f a := g b }
apply :: f := g -> a := b -> f a := g b
apply :: (f := g) -> (a := b) -> f a := g b
apply f := g
fg a := b
ab = Apply a b f g -> f a := g b
forall k (a :: k) k (b :: k) k (f :: k -> k) (g :: k -> k).
Apply a b f g -> f a := g b
unapply ((f := g) -> Apply a b f f -> Apply a b f g
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
subst f := g
fg ((f a := f b) -> Apply a b f f
forall k k k (a :: k) (b :: k) (f :: k -> k) (g :: k -> k).
(f a := g b) -> Apply a b f g
Apply ((a := b) -> f a := f b
forall k k (a :: k) (b :: k) (f :: k -> k). (a := b) -> f a := f b
lift a := b
ab)))
#endif
instance Category (:=) where
id :: a := a
id = (forall (c :: k -> *). c a -> c a) -> a := a
forall k (a :: k) (b :: k).
(forall (c :: k -> *). c a -> c b) -> a := b
Refl forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
forall (c :: k -> *). c a -> c a
id
b := c
bc . :: (b := c) -> (a := b) -> a := c
. a := b
ab = (b := c) -> (a := b) -> a := c
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
subst b := c
bc a := b
ab
instance Semigroupoid (:=) where
j := k1
bc o :: (j := k1) -> (i := j) -> i := k1
`o` i := j
ab = (j := k1) -> (i := j) -> i := k1
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
subst j := k1
bc i := j
ab
instance Groupoid (:=) where
inv :: (a := b) -> b := a
inv = (a := b) -> b := a
forall k (a :: k) (b :: k). (a := b) -> b := a
symm
trans :: a := b -> b := c -> a := c
trans :: (a := b) -> (b := c) -> a := c
trans a := b
ab b := c
bc = (b := c) -> (a := b) -> a := c
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
subst b := c
bc a := b
ab
newtype Symm p a b = Symm { Symm p a b -> p b a
unsymm :: p b a }
symm :: (a := b) -> (b := a)
symm :: (a := b) -> b := a
symm a := b
a = Symm (:=) a b -> b := a
forall k k (p :: k -> k -> *) (a :: k) (b :: k).
Symm p a b -> p b a
unsymm ((a := b) -> Symm (:=) a a -> Symm (:=) a b
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
subst a := b
a ((a := a) -> Symm (:=) a a
forall k k (p :: k -> k -> *) (a :: k) (b :: k).
p b a -> Symm p a b
Symm a := a
forall k (a :: k). a := a
refl))
newtype Lift f a b = Lift { Lift f a b -> f a := f b
unlift :: f a := f b }
lift :: a := b -> f a := f b
lift :: (a := b) -> f a := f b
lift a := b
a = Lift f a b -> f a := f b
forall k k (f :: k -> k) (a :: k) (b :: k).
Lift f a b -> f a := f b
unlift ((a := b) -> Lift f a a -> Lift f a b
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
subst a := b
a ((f a := f a) -> Lift f a a
forall k k (f :: k -> k) (a :: k) (b :: k).
(f a := f b) -> Lift f a b
Lift f a := f a
forall k (a :: k). a := a
refl))
newtype Lift2 f c a b = Lift2 { Lift2 f c a b -> f a c := f b c
unlift2 :: f a c := f b c }
lift2 :: a := b -> f a c := f b c
lift2 :: (a := b) -> f a c := f b c
lift2 a := b
a = Lift2 f c a b -> f a c := f b c
forall k k k (f :: k -> k -> k) (c :: k) (a :: k) (b :: k).
Lift2 f c a b -> f a c := f b c
unlift2 ((a := b) -> Lift2 f c a a -> Lift2 f c a b
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
subst a := b
a ((f a c := f a c) -> Lift2 f c a a
forall k k k (f :: k -> k -> k) (c :: k) (a :: k) (b :: k).
(f a c := f b c) -> Lift2 f c a b
Lift2 f a c := f a c
forall k (a :: k). a := a
refl))
lift2' :: a := b -> c := d -> f a c := f b d
lift2' :: (a := b) -> (c := d) -> f a c := f b d
lift2' a := b
ab c := d
cd = (f a d := f b d) -> (f a c := f a d) -> f a c := f b d
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
subst ((a := b) -> f a d := f b d
forall k k k (a :: k) (b :: k) (f :: k -> k -> k) (c :: k).
(a := b) -> f a c := f b c
lift2 a := b
ab) ((c := d) -> f a c := f a d
forall k k (a :: k) (b :: k) (f :: k -> k). (a := b) -> f a := f b
lift c := d
cd)
newtype Lift3 f c d a b = Lift3 { Lift3 f c d a b -> f a c d := f b c d
unlift3 :: f a c d := f b c d }
lift3 :: a := b -> f a c d := f b c d
lift3 :: (a := b) -> f a c d := f b c d
lift3 a := b
a = Lift3 f c d a b -> f a c d := f b c d
forall k k k k (f :: k -> k -> k -> k) (c :: k) (d :: k) (a :: k)
(b :: k).
Lift3 f c d a b -> f a c d := f b c d
unlift3 ((a := b) -> Lift3 f c d a a -> Lift3 f c d a b
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
subst a := b
a ((f a c d := f a c d) -> Lift3 f c d a a
forall k k k k (f :: k -> k -> k -> k) (c :: k) (d :: k) (a :: k)
(b :: k).
(f a c d := f b c d) -> Lift3 f c d a b
Lift3 f a c d := f a c d
forall k (a :: k). a := a
refl))
lift3' :: a := b -> c := d -> e := f -> g a c e := g b d f
lift3' :: (a := b) -> (c := d) -> (e := f) -> g a c e := g b d f
lift3' a := b
ab c := d
cd e := f
ef = (a := b) -> g a d f := g b d f
forall k k k k (a :: k) (b :: k) (f :: k -> k -> k -> k) (c :: k)
(d :: k).
(a := b) -> f a c d := f b c d
lift3 a := b
ab (g a d f := g b d f) -> (g a c f := g a d f) -> g a c f := g b d f
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
`subst` (c := d) -> g a c f := g a d f
forall k k k (a :: k) (b :: k) (f :: k -> k -> k) (c :: k).
(a := b) -> f a c := f b c
lift2 c := d
cd (g a c f := g b d f) -> (g a c e := g a c f) -> g a c e := g b d f
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
`subst` (e := f) -> g a c e := g a c f
forall k k (a :: k) (b :: k) (f :: k -> k). (a := b) -> f a := f b
lift e := f
ef
#ifdef LANGUAGE_PolyKinds
type family GenInj (f :: j -> k) (g :: j -> k) (x :: k) :: j
type family GenInj2 (f :: i -> j -> k) (g :: i -> j' -> k) (x :: k) :: i
type family GenInj3 (f :: h -> i -> j -> k) (g :: h -> i' -> j' -> k) (x :: k) :: h
#else
type family GenInj (f :: * -> *) (g :: * -> *) (x :: *) :: *
type family GenInj2 (f :: * -> * -> *) (g :: * -> * -> *) (x :: *) :: *
type family GenInj3 (f :: * -> * -> * -> *) (g :: * -> * -> * -> *) (x :: *) :: *
#endif
type instance GenInj f g (f a) = a
type instance GenInj f g (g b) = b
type instance GenInj2 f g (f a c) = a
type instance GenInj2 f g (g b c') = b
type instance GenInj3 f g (f a c d) = a
type instance GenInj3 f g (g b c' d') = b
newtype Lower f g a x = Lower { Lower f g a x -> a := GenInj f g x
unlower :: a := GenInj f g x }
newtype Lower2 f g a x = Lower2 { Lower2 f g a x -> a := GenInj2 f g x
unlower2 :: a := GenInj2 f g x }
newtype Lower3 f g a x = Lower3 { Lower3 f g a x -> a := GenInj3 f g x
unlower3 :: a := GenInj3 f g x }
lower :: forall a b f g. f a := g b -> a := b
lower :: (f a := g b) -> a := b
lower f a := g b
eq = Lower f g a (g b) -> a := GenInj f g (g b)
forall k k (f :: k -> k) (g :: k -> k) (a :: k) (x :: k).
Lower f g a x -> a := GenInj f g x
unlower ((f a := g b) -> Lower f g a (f a) -> Lower f g a (g b)
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
subst f a := g b
eq ((a := GenInj f g (f a)) -> Lower f g a (f a)
forall k k (f :: k -> k) (g :: k -> k) (a :: k) (x :: k).
(a := GenInj f g x) -> Lower f g a x
Lower a := GenInj f g (f a)
forall k (a :: k). a := a
refl :: Lower f g a (f a)))
lower2 :: forall a b f g c c'. f a c := g b c' -> a := b
lower2 :: (f a c := g b c') -> a := b
lower2 f a c := g b c'
eq = Lower2 f g a (g b c') -> a := GenInj2 f g (g b c')
forall j k k (f :: k -> j -> k) j' (g :: k -> j' -> k) (a :: k)
(x :: k).
Lower2 f g a x -> a := GenInj2 f g x
unlower2 ((f a c := g b c') -> Lower2 f g a (f a c) -> Lower2 f g a (g b c')
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
subst f a c := g b c'
eq ((a := GenInj2 f g (f a c)) -> Lower2 f g a (f a c)
forall k j k j' (f :: k -> j -> k) (g :: k -> j' -> k) (a :: k)
(x :: k).
(a := GenInj2 f g x) -> Lower2 f g a x
Lower2 a := GenInj2 f g (f a c)
forall k (a :: k). a := a
refl :: Lower2 f g a (f a c)))
lower3 :: forall a b f g c c' d d'. f a c d := g b c' d' -> a := b
lower3 :: (f a c d := g b c' d') -> a := b
lower3 f a c d := g b c' d'
eq = Lower3 f g a (g b c' d') -> a := GenInj3 f g (g b c' d')
forall i j k k (f :: k -> i -> j -> k) i' j'
(g :: k -> i' -> j' -> k) (a :: k) (x :: k).
Lower3 f g a x -> a := GenInj3 f g x
unlower3 ((f a c d := g b c' d')
-> Lower3 f g a (f a c d) -> Lower3 f g a (g b c' d')
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
subst f a c d := g b c' d'
eq ((a := GenInj3 f g (f a c d)) -> Lower3 f g a (f a c d)
forall k i j k i' j' (f :: k -> i -> j -> k)
(g :: k -> i' -> j' -> k) (a :: k) (x :: k).
(a := GenInj3 f g x) -> Lower3 f g a x
Lower3 a := GenInj3 f g (f a c d)
forall k (a :: k). a := a
refl :: Lower3 f g a (f a c d)))
fromLeibniz :: a := b -> a Eq.:~: b
fromLeibniz :: (a := b) -> a :~: b
fromLeibniz a := b
a = (a := b) -> (a :~: a) -> a :~: b
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
subst a := b
a a :~: a
forall k (a :: k). a :~: a
Eq.Refl
toLeibniz :: a Eq.:~: b -> a := b
toLeibniz :: (a :~: b) -> a := b
toLeibniz a :~: b
Eq.Refl = a := b
forall k (a :: k). a := a
refl
instance Eq.TestEquality ((:=) a) where
testEquality :: (a := a) -> (a := b) -> Maybe (a :~: b)
testEquality a := a
fa a := b
fb = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just ((a := b) -> a :~: b
forall k (a :: k) (b :: k). (a := b) -> a :~: b
fromLeibniz ((a := a) -> (a := b) -> a := b
forall k (a :: k) (b :: k) (c :: k). (a := b) -> (b := c) -> a := c
trans ((a := a) -> a := a
forall k (a :: k) (b :: k). (a := b) -> b := a
symm a := a
fa) a := b
fb))
#ifdef HAS_DATA_TYPE_COERCION
reprLeibniz :: a := b -> Co.Coercion a b
reprLeibniz :: (a := b) -> Coercion a b
reprLeibniz a := b
a = (a := b) -> Coercion a a -> Coercion a b
forall k (a :: k) (b :: k).
(a := b) -> forall (c :: k -> *). c a -> c b
subst a := b
a Coercion a a
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Co.Coercion
instance Co.TestCoercion ((:=) a) where
testCoercion :: (a := a) -> (a := b) -> Maybe (Coercion a b)
testCoercion a := a
fa a := b
fb = Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just ((a := b) -> Coercion a b
forall k (a :: k) (b :: k). (a := b) -> Coercion a b
reprLeibniz ((a := a) -> (a := b) -> a := b
forall k (a :: k) (b :: k) (c :: k). (a := b) -> (b := c) -> a := c
trans ((a := a) -> a := a
forall k (a :: k) (b :: k). (a := b) -> b := a
symm a := a
fa) a := b
fb))
#endif