Data.Eq.Type.Hetero

Leibnizian equality à la Data.Eq.Type, generalized to be heterogeneous 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. i -> Type). c a -> c b

Instances

Category ((:==) :: k -> k -> Type)

Equality forms a category.

Defined in Data.Eq.Type.Hetero

Methods

id :: a :== a

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

Groupoid ((:==) :: k -> k -> Type)

Defined in Data.Eq.Type.Hetero

Methods

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

Semigroupoid ((:==) :: k -> k -> Type)

Defined in Data.Eq.Type.Hetero

Methods

o :: (j :== k1) -> (i :== j) -> i :== k1

TestCoercion ((:==) a :: k -> Type)

Defined in Data.Eq.Type.Hetero

Methods

testCoercion :: (a :== a0) -> (a :== b) -> Maybe (Coercion a0 b)

TestEquality ((:==) a :: k -> Type)

Defined in Data.Eq.Type.Hetero

Methods

testEquality :: (a :== a0) -> (a :== b) -> Maybe (a0 :~: 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 k (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 j k (f :: i -> j -> k) (a :: i) (b :: i) (c :: j). (f a c :== f b c) -> a :== b

lower3 :: forall h i j k (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