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 :: a := a

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

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

Defined in Data.Eq.Type

Methods

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

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

Defined in Data.Eq.Type

Methods

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

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

Defined in Data.Eq.Type

Methods

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

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

Defined in Data.Eq.Type

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

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

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

... in any position ...

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