License	BSD-style (see the LICENSE file in the distribution)
Maintainer	libraries@haskell.org
Stability	experimental
Portability	not portable
Safe Haskell	Trustworthy
Language	Haskell2010

Data.Type.Equality

Contents

Description

Definition of propositional equality(:~:). Pattern-matching on a variable of type(a :~: b) produces a proof thata ~ b.

Since: 4.7.0.0

Synopsis

data a:~: bwhere
- Refl :: a:~: a
class a ~# b => (a :: k0)~~ (b :: k1)
data (a :: k1):~~: (b :: k2)where
- HRefl :: a:~~: a
sym :: (a:~: b) -> b:~: a
trans :: (a:~: b) -> (b:~: c) -> a:~: c
castWith :: (a:~: b) -> a -> b
gcastWith :: (a:~: b) -> (a ~ b => r) -> r
apply :: (f:~: g) -> (a:~: b) -> f a:~: g b
inner :: (f a:~: g b) -> a:~: b
outer :: (f a:~: g b) -> f:~: g
classTestEquality fwhere
- testEquality :: f a -> f b ->Maybe (a:~: b)
type family (a :: k)== (b :: k) ::Boolwhere ...

The equality types

data a:~: bwhereinfix 4Source #

Propositional equality. Ifa :~: b is inhabited by some terminating value, then the typea is the same as the typeb. To use this equality in practice, pattern-match on thea :~: b to get out theRefl constructor; in the body of the pattern-match, the compiler knows thata ~ b.

Since: 4.7.0.0

Constructors

Refl :: a:~: a

Instances

Category ((:~:) :: k -> k ->Type)Source #	Since: 4.7.0.0
Instance details Defined inControl.Category Methods id :: a:~: aSource # (.) :: (b:~: c) -> (a:~: b) -> a:~: cSource #
TestEquality ((:~:) a :: k ->Type)Source #	Since: 4.7.0.0
Instance details Defined inData.Type.Equality Methods testEquality :: (a:~: a0) -> (a:~: b) ->Maybe (a0:~: b)Source #
TestCoercion ((:~:) a :: k ->Type)Source #	Since: 4.7.0.0
Instance details Defined inData.Type.Coercion Methods testCoercion :: (a:~: a0) -> (a:~: b) ->Maybe (Coercion a0 b)Source #
a ~ b =>Bounded (a:~: b)Source #	Since: 4.7.0.0
Instance details Defined inData.Type.Equality Methods minBound :: a:~: bSource # maxBound :: a:~: bSource #
a ~ b =>Enum (a:~: b)Source #	Since: 4.7.0.0
Instance details Defined inData.Type.Equality Methods succ :: (a:~: b) -> a:~: bSource # pred :: (a:~: b) -> a:~: bSource # toEnum ::Int -> a:~: bSource # fromEnum :: (a:~: b) ->Int Source # enumFrom :: (a:~: b) -> [a:~: b]Source # enumFromThen :: (a:~: b) -> (a:~: b) -> [a:~: b]Source # enumFromTo :: (a:~: b) -> (a:~: b) -> [a:~: b]Source # enumFromThenTo :: (a:~: b) -> (a:~: b) -> (a:~: b) -> [a:~: b]Source #
Eq (a:~: b)Source #	Since: 4.7.0.0
Instance details Defined inData.Type.Equality Methods (==) :: (a:~: b) -> (a:~: b) ->Bool # (/=) :: (a:~: b) -> (a:~: b) ->Bool #
(a ~ b,Data a) =>Data (a:~: b)Source #	Since: 4.7.0.0
Instance details Defined inData.Data Methods gfoldl :: (forall d b0.Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a:~: b) -> c (a:~: b)Source # gunfold :: (forall b0 r.Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) ->Constr -> c (a:~: b)Source # toConstr :: (a:~: b) ->Constr Source # dataTypeOf :: (a:~: b) ->DataType Source # dataCast1 ::Typeable t => (forall d.Data d => c (t d)) ->Maybe (c (a:~: b))Source # dataCast2 ::Typeable t => (forall d e. (Data d,Data e) => c (t d e)) ->Maybe (c (a:~: b))Source # gmapT :: (forall b0.Data b0 => b0 -> b0) -> (a:~: b) -> a:~: bSource # gmapQl :: (r -> r' -> r) -> r -> (forall d.Data d => d -> r') -> (a:~: b) -> rSource # gmapQr :: (r' -> r -> r) -> r -> (forall d.Data d => d -> r') -> (a:~: b) -> rSource # gmapQ :: (forall d.Data d => d -> u) -> (a:~: b) -> [u]Source # gmapQi ::Int -> (forall d.Data d => d -> u) -> (a:~: b) -> uSource # gmapM ::Monad m => (forall d.Data d => d -> m d) -> (a:~: b) -> m (a:~: b)Source # gmapMp ::MonadPlus m => (forall d.Data d => d -> m d) -> (a:~: b) -> m (a:~: b)Source # gmapMo ::MonadPlus m => (forall d.Data d => d -> m d) -> (a:~: b) -> m (a:~: b)Source #
Ord (a:~: b)Source #	Since: 4.7.0.0
Instance details Defined inData.Type.Equality Methods compare :: (a:~: b) -> (a:~: b) ->Ordering # (<) :: (a:~: b) -> (a:~: b) ->Bool # (<=) :: (a:~: b) -> (a:~: b) ->Bool # (>) :: (a:~: b) -> (a:~: b) ->Bool # (>=) :: (a:~: b) -> (a:~: b) ->Bool # max :: (a:~: b) -> (a:~: b) -> a:~: b# min :: (a:~: b) -> (a:~: b) -> a:~: b#
a ~ b =>Read (a:~: b)Source #	Since: 4.7.0.0
Instance details Defined inData.Type.Equality Methods readsPrec ::Int ->ReadS (a:~: b)Source # readList ::ReadS [a:~: b]Source # readPrec ::ReadPrec (a:~: b)Source # readListPrec ::ReadPrec [a:~: b]Source #
Show (a:~: b)Source #	Since: 4.7.0.0
Instance details Defined inData.Type.Equality Methods showsPrec ::Int -> (a:~: b) ->ShowS Source # show :: (a:~: b) ->String Source # showList :: [a:~: b] ->ShowS Source #

class a ~# b => (a :: k0)~~ (b :: k1)#

Lifted, heterogeneous equality. By lifted, we mean that it can be bogus (deferred type error). By heterogeneous, the two typesa andb might have different kinds. Because~~ can appear unexpectedly in error messages to users who do not care about the difference between heterogeneous equality~~ and homogeneous equality~, this is printed as~ unless-fprint-equality-relations is set.

data (a :: k1):~~: (b :: k2)whereinfix 4Source #

Kind heterogeneous propositional equality. Like:~:,a :~~: b is inhabited by a terminating value if and only ifa is the same type asb.

Since: 4.10.0.0

Constructors

HRefl :: a:~~: a

Instances

Category ((:~~:) :: k -> k ->Type)Source #	Since: 4.10.0.0
Instance details Defined inControl.Category Methods id :: a:~~: aSource # (.) :: (b:~~: c) -> (a:~~: b) -> a:~~: cSource #
TestEquality ((:~~:) a :: k ->Type)Source #	Since: 4.10.0.0
Instance details Defined inData.Type.Equality Methods testEquality :: (a:~~: a0) -> (a:~~: b) ->Maybe (a0:~: b)Source #
TestCoercion ((:~~:) a :: k ->Type)Source #	Since: 4.10.0.0
Instance details Defined inData.Type.Coercion Methods testCoercion :: (a:~~: a0) -> (a:~~: b) ->Maybe (Coercion a0 b)Source #
a~~ b =>Bounded (a:~~: b)Source #	Since: 4.10.0.0
Instance details Defined inData.Type.Equality Methods minBound :: a:~~: bSource # maxBound :: a:~~: bSource #
a~~ b =>Enum (a:~~: b)Source #	Since: 4.10.0.0
Instance details Defined inData.Type.Equality Methods succ :: (a:~~: b) -> a:~~: bSource # pred :: (a:~~: b) -> a:~~: bSource # toEnum ::Int -> a:~~: bSource # fromEnum :: (a:~~: b) ->Int Source # enumFrom :: (a:~~: b) -> [a:~~: b]Source # enumFromThen :: (a:~~: b) -> (a:~~: b) -> [a:~~: b]Source # enumFromTo :: (a:~~: b) -> (a:~~: b) -> [a:~~: b]Source # enumFromThenTo :: (a:~~: b) -> (a:~~: b) -> (a:~~: b) -> [a:~~: b]Source #
Eq (a:~~: b)Source #	Since: 4.10.0.0
Instance details Defined inData.Type.Equality Methods (==) :: (a:~~: b) -> (a:~~: b) ->Bool # (/=) :: (a:~~: b) -> (a:~~: b) ->Bool #
(Typeable i,Typeable j,Typeable a,Typeable b, a~~ b) =>Data (a:~~: b)Source #	Since: 4.10.0.0
Instance details Defined inData.Data Methods gfoldl :: (forall d b0.Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a:~~: b) -> c (a:~~: b)Source # gunfold :: (forall b0 r.Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) ->Constr -> c (a:~~: b)Source # toConstr :: (a:~~: b) ->Constr Source # dataTypeOf :: (a:~~: b) ->DataType Source # dataCast1 ::Typeable t => (forall d.Data d => c (t d)) ->Maybe (c (a:~~: b))Source # dataCast2 ::Typeable t => (forall d e. (Data d,Data e) => c (t d e)) ->Maybe (c (a:~~: b))Source # gmapT :: (forall b0.Data b0 => b0 -> b0) -> (a:~~: b) -> a:~~: bSource # gmapQl :: (r -> r' -> r) -> r -> (forall d.Data d => d -> r') -> (a:~~: b) -> rSource # gmapQr :: (r' -> r -> r) -> r -> (forall d.Data d => d -> r') -> (a:~~: b) -> rSource # gmapQ :: (forall d.Data d => d -> u) -> (a:~~: b) -> [u]Source # gmapQi ::Int -> (forall d.Data d => d -> u) -> (a:~~: b) -> uSource # gmapM ::Monad m => (forall d.Data d => d -> m d) -> (a:~~: b) -> m (a:~~: b)Source # gmapMp ::MonadPlus m => (forall d.Data d => d -> m d) -> (a:~~: b) -> m (a:~~: b)Source # gmapMo ::MonadPlus m => (forall d.Data d => d -> m d) -> (a:~~: b) -> m (a:~~: b)Source #
Ord (a:~~: b)Source #	Since: 4.10.0.0
Instance details Defined inData.Type.Equality Methods compare :: (a:~~: b) -> (a:~~: b) ->Ordering # (<) :: (a:~~: b) -> (a:~~: b) ->Bool # (<=) :: (a:~~: b) -> (a:~~: b) ->Bool # (>) :: (a:~~: b) -> (a:~~: b) ->Bool # (>=) :: (a:~~: b) -> (a:~~: b) ->Bool # max :: (a:~~: b) -> (a:~~: b) -> a:~~: b# min :: (a:~~: b) -> (a:~~: b) -> a:~~: b#
a~~ b =>Read (a:~~: b)Source #	Since: 4.10.0.0
Instance details Defined inData.Type.Equality Methods readsPrec ::Int ->ReadS (a:~~: b)Source # readList ::ReadS [a:~~: b]Source # readPrec ::ReadPrec (a:~~: b)Source # readListPrec ::ReadPrec [a:~~: b]Source #
Show (a:~~: b)Source #	Since: 4.10.0.0
Instance details Defined inData.Type.Equality Methods showsPrec ::Int -> (a:~~: b) ->ShowS Source # show :: (a:~~: b) ->String Source # showList :: [a:~~: b] ->ShowS Source #

Working with equality

sym :: (a:~: b) -> b:~: aSource #

Symmetry of equality

trans :: (a:~: b) -> (b:~: c) -> a:~: cSource #

Transitivity of equality

castWith :: (a:~: b) -> a -> bSource #

Type-safe cast, using propositional equality

gcastWith :: (a:~: b) -> (a ~ b => r) -> rSource #

Generalized form of type-safe cast using propositional equality

apply :: (f:~: g) -> (a:~: b) -> f a:~: g bSource #

Apply one equality to another, respectively

inner :: (f a:~: g b) -> a:~: bSource #

Extract equality of the arguments from an equality of applied types

outer :: (f a:~: g b) -> f:~: gSource #

Extract equality of type constructors from an equality of applied types

Inferring equality from other types

classTestEquality fwhereSource #

This class contains types where you can learn the equality of two types from information contained interms. Typically, only singleton types should inhabit this class.

Methods

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

Conditionally prove the equality ofa andb.

Instances

TestEquality (TypeRep :: k ->Type)Source #
Instance details Defined inData.Typeable.Internal Methods testEquality ::TypeRep a ->TypeRep b ->Maybe (a:~: b)Source #
TestEquality ((:~:) a :: k ->Type)Source #	Since: 4.7.0.0
Instance details Defined inData.Type.Equality Methods testEquality :: (a:~: a0) -> (a:~: b) ->Maybe (a0:~: b)Source #
TestEquality ((:~~:) a :: k ->Type)Source #	Since: 4.10.0.0
Instance details Defined inData.Type.Equality Methods testEquality :: (a:~~: a0) -> (a:~~: b) ->Maybe (a0:~: b)Source #

Boolean type-level equality

type family (a :: k)== (b :: k) ::Boolwhere ...infix 4Source #

A type family to compute Boolean equality.

Equations

(f a)== (g b) = (f== g)&& (a== b)
a== a =True
_== _ =False

Movatterモバイル変換

The equality types

Working with equality

Inferring equality from other types

Boolean type-level equality