Copyright	(C) 2011-2014 Edward Kmett 2018 Ryan Scott
License	BSD-style (see the file LICENSE)
Maintainer	Edward Kmett <ekmett@gmail.com>
Stability	provisional
Portability	GHC
Safe Haskell	None
Language	Haskell2010

Data.Eq.Type.Hetero

Contents

Description

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.

Synopsis

newtype (a :: j) :== (b :: k) = HRefl {
- hsubst :: forall (c :: forall i. i -> Type). 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
toHomogeneous :: (a :== b) -> a := b
fromHomogeneous :: (a := b) -> a :== b
fromLeibniz :: forall a b. (a :== b) -> a :~: b
toLeibniz :: (a :~: b) -> a :== b
heteroFromLeibniz :: (a :== b) -> a :~~: b
heteroToLeibniz :: (a :~~: b) -> a :== b
reprLeibniz :: (a :== b) -> Coercion a b

Heterogeneous Leibnizian equality

newtype (a :: j) :== (b :: k) infixl 4 Source #

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 details

Category ((:==) :: k -> k -> Type) Source #	Equality forms a category.
Instance details 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) Source #
Instance details Defined in Data.Eq.Type.Hetero Methods inv :: forall (a :: k0) (b :: k0). (a :== b) -> b :== a #
Semigroupoid ((:==) :: k -> k -> Type) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in Data.Eq.Type.Hetero Methods testEquality :: forall (a0 :: k0) (b :: k0). (a :== a0) -> (a :== b) -> Maybe (a0 :~: b) #