Data.Eq.Type.Hetero

Leibnizian equality à la Data.Eq.Type, generalized to be heterogenous using higher-rank kinds.

This module is only exposed on GHC 8.2 and later.

Heterogeneous Leibnizian equality

newtype (a :: j) :== (b :: k) infixl 4

Heterogeneous Leibnizian equality.

Leibnizian equality states that two things are equal if you can substitute one for the other in all contexts.

Constructors

HRefl

Fields

• hsubst :: forall (c :: forall (i :: Type). i -> Type). c a -> c b

Instances

Category k ((:==) k k)

Equality forms a category.

Methods

id :: cat a a

(.) :: cat b c -> cat a b -> cat a c

Groupoid k ((:==) k k)

Methods

inv :: k1 a b -> k1 b a

Semigroupoid k ((:==) k k)

Methods

o :: c j k1 -> c i j -> c i k1

TestCoercion k ((:==) j k a)

Methods

testCoercion :: f a -> f b -> Maybe (Coercion ((j :== k) a) a b)

TestEquality k ((:==) j k a)

Methods

testEquality :: f a -> f b -> Maybe (((j :== k) a :~: a) b)

Equality as an equivalence relation

refl :: a :== a

Equality is reflexive.

trans :: (a :== b) -> (b :== c) -> a :== c

Equality is transitive.

symm :: (a :== b) -> b :== a

Equality is symmetric.

coerce :: (a :== b) -> a -> b

If two things are equal, you can convert one to the other.

Lifting equality

lift :: (a :== b) -> f a :== f b

You can lift equality into any type constructor...

lift2 :: (a :== b) -> f a c :== f b c

... in any position.

lift2' :: (a :== b) -> (c :== d) -> f a c :== f b d

lift3 :: (a :== b) -> f a c d :== f b c d

lift3' :: (a :== b) -> (c :== d) -> (e :== f) -> g a c e :== g b d f

Lowering equality

lower :: forall (j :: Type) (k :: Type) (f :: j -> k) (a :: j) (b :: j). (f a :== f b) -> a :== b

Type constructors are injective, so you can lower equality through any type constructor.

lower2 :: forall (i :: Type) (j :: Type) (k :: Type) (f :: i -> j -> k) (a :: i) (b :: i) (c :: j). (f a c :== f b c) -> a :== b

lower3 :: forall (h :: Type) (i :: Type) (j :: Type) (k :: Type) (f :: h -> i -> j -> k) (a :: h) (b :: h) (c :: i) (d :: j). (f a c d :== f b c d) -> a :== b

:= equivalence

:= is equivalent in power

toHomogeneous :: (a :== b) -> a := b

Convert an appropriately kinded heterogeneous Leibnizian equality into a homogeneous Leibnizian equality '(ET.:=)'.

fromHomogeneous :: (a := b) -> a :== b

Convert a homogeneous Leibnizian equality '(ET.:=)' to an appropriately kinded heterogeneous Leibizian equality.

:~: equivalence

:~: is equivalent in power

fromLeibniz :: forall a b. (a :== b) -> a :~: b

toLeibniz :: (a :~: b) -> a :== b

:~~: equivalence

:~~: is equivalent in power

heteroFromLeibniz :: (a :== b) -> a :~~: b

heteroToLeibniz :: (a :~~: b) -> a :== b

Coercion conversion

Leibnizian equality can be converted to representational equality

reprLeibniz :: (a :== b) -> Coercion a b