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 :: forall (a :: k0). a :== a

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

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

Defined in Data.Eq.Type.Hetero

Methods

inv :: forall (a :: k0) (b :: k0). (a :== b) -> b :== a

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

Defined in Data.Eq.Type.Hetero

Methods

o :: forall (j :: k0) (k1 :: k0) (i :: k0). (j :== k1) -> (i :== j) -> i :== k1

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

Defined in Data.Eq.Type.Hetero

Methods

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

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

Defined in Data.Eq.Type.Hetero

Methods

testEquality :: forall (a0 :: k0) (b :: k0). (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.

apply :: (f :== g) -> (a :== b) -> f a :== g b

Apply one equality to another, respectively

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 a b f g. (f a :== g b) -> a :== b

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

lower2 :: forall a b f g c c'. (f a c :== g b c') -> a :== b

lower3 :: forall a b f g c c' d d'. (f a c d :== g 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 (:=).

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

Convert a homogeneous Leibnizian equality (:=) 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