Copyright | (C) 2011-2014 Edward Kmett |
---|---|
License | BSD-style (see the file LICENSE) |
Maintainer | Edward Kmett <ekmett@gmail.com> |
Stability | provisional |
Portability | rank2 types, type operators, (optional) type families |
Safe Haskell | None |
Language | Haskell2010 |
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
- newtype a := b = Refl {
- subst :: forall c. c a -> c b
- refl :: a := a
- trans :: (a := b) -> (b := c) -> a := c
- symm :: (a := b) -> b := a
- coerce :: (a := b) -> a -> b
- apply :: (f := g) -> (a := b) -> f a := g b
- lift :: (a := b) -> f a := f b
- lift2 :: (a := b) -> f a c := f b c
- 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
- lower :: forall a b f g. (f a := g b) -> a := b
- 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
- fromLeibniz :: (a := b) -> a :~: b
- toLeibniz :: (a :~: b) -> a := b
- reprLeibniz :: (a := b) -> Coercion a b
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
Instances
Category ((:=) :: k -> k -> Type) Source # | Equality forms a category |
Groupoid ((:=) :: k -> k -> Type) Source # | |
Defined in Data.Eq.Type | |
Semigroupoid ((:=) :: k -> k -> Type) Source # | |
TestCoercion ((:=) a :: k -> Type) Source # | |
Defined in Data.Eq.Type | |
TestEquality ((:=) a :: k -> Type) Source # | |
Defined in Data.Eq.Type |
Equality as an equivalence relation
Lifting equality
Lowering equality
lower :: forall a b f g. (f a := g b) -> a := b Source #
Type constructors are generative and injective, so you can lower equality through any type constructors ...
lower3 :: forall a b f g c c' d d'. (f a c d := g 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 #
Coercion
conversion
Leibnizian equality can be converted to representational equality
reprLeibniz :: (a := b) -> Coercion a b Source #