Data.Eq.Type

Leibnizian equality. Injectivity in the presence of type families is provided by a generalization of a trick by Oleg Kiselyov posted here:

http://www.haskell.org/pipermail/haskell-cafe/2010-May/077177.html

Leibnizian equality

newtype a := b infixl 4

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

Constructors

Refl

Fields

• subst :: forall c. c a -> c b

Instances

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

Equality forms a category

Defined in Data.Eq.Type

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

Methods

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

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

Defined in Data.Eq.Type

Methods

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

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

Defined in Data.Eq.Type

Methods

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

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

Defined in Data.Eq.Type

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

... in any position ...

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

... these definitions are poly-kinded on GHC 7.6 and up.

:~: equivalence

Data.Type.Equality GADT definition is equivalent in power

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

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

Coercion conversion

Leibnizian equality can be converted to representational equality

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