eq-4.2: Leibnizian equality

Copyright(C) 2011-2014 Edward Kmett
LicenseBSD-style (see the file LICENSE)
MaintainerEdward Kmett <ekmett@gmail.com>
Stabilityprovisional
Portabilityrank2 types, type operators, (optional) type families
Safe HaskellNone
LanguageHaskell98

Data.Eq.Type

Contents

Description

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

Synopsis

Leibnizian equality

newtype a := b infixl 4 Source #

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) Source #

Equality forms a category

Methods

id :: cat a a #

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

Groupoid k ((:=) k) Source # 

Methods

inv :: k1 a b -> k1 b a #

Semigroupoid k ((:=) k) Source # 

Methods

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

TestCoercion k ((:=) k a) Source # 

Methods

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

TestEquality k ((:=) k a) Source # 

Methods

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

Equality as an equivalence relation

refl :: a := a Source #

Equality is reflexive

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

Equality is transitive

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

Equality is symmetric

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

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

Lifting equality

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

You can lift equality into any type constructor

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

... in any position

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

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

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

Lowering equality

lower :: forall a b f. (f a := f b) -> a := b Source #

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 Source #

... in any position ...

lower3 :: forall a b c d f. (f a c d := f b c d) -> a := b Source #

... 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 Source #

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

Coercion conversion

Leibnizian equality can be converted to representational equality

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