Data.Type.Equality

License BSD-style (see the LICENSE file in the distribution)
Maintainer [email protected]
Stability experimental
Portability not portable
Safe Haskell Trustworthy
Language Haskell2010

Description

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

Since: base-4.7.0.0

The equality types

data a :~: b where infix 4 Source

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Since: base-4.7.0.0

Constructors

Refl :: a :~: a
Instances
Instances details
Category ((:~:) :: k -> k -> Type)

Since: base-4.7.0.0
Instance details

Defined in Control.Category

Methods

id :: forall (a :: k0). a :~: a Source

(.) :: forall (b :: k0) (c :: k0) (a :: k0). (b :~: c) -> (a :~: b) -> a :~: c Source

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

Since: base-4.7.0.0
Instance details

Defined in Data.Type.Equality

Methods

testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Source

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

Since: base-4.7.0.0
Instance details

Defined in Data.Type.Coercion

Methods

testCoercion :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) Source

a ~ b => Bounded (a :~: b)

Since: base-4.7.0.0
Instance details

Defined in Data.Type.Equality

Methods

minBound :: a :~: b Source

maxBound :: a :~: b Source

a ~ b => Enum (a :~: b)

Since: base-4.7.0.0
Instance details

Defined in Data.Type.Equality

Methods

succ :: (a :~: b) -> a :~: b Source

pred :: (a :~: b) -> a :~: b Source

toEnum :: Int -> a :~: b Source

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)

Since: base-4.7.0.0
Instance details

Defined in Data.Type.Equality

Methods

(==) :: (a :~: b) -> (a :~: b) -> Bool Source

(/=) :: (a :~: b) -> (a :~: b) -> Bool Source

(a ~ b, Data a) => Data (a :~: b)

Since: base-4.7.0.0
Instance details

Defined in Data.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 :~: b Source

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r Source

gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] Source

gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u Source

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)

Since: base-4.7.0.0
Instance details

Defined in Data.Type.Equality

Methods

compare :: (a :~: b) -> (a :~: b) -> Ordering Source

(<) :: (a :~: b) -> (a :~: b) -> Bool Source

(<=) :: (a :~: b) -> (a :~: b) -> Bool Source

(>) :: (a :~: b) -> (a :~: b) -> Bool Source

(>=) :: (a :~: b) -> (a :~: b) -> Bool Source

max :: (a :~: b) -> (a :~: b) -> a :~: b Source

min :: (a :~: b) -> (a :~: b) -> a :~: b Source

a ~ b => Read (a :~: b)

Since: base-4.7.0.0
Instance details

Defined in Data.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)

Since: base-4.7.0.0
Instance details

Defined in Data.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) Source

Lifted, heterogeneous equality. By lifted, we mean that it can be bogus (deferred type error). By heterogeneous, the two types a and b 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 :~~: b where infix 4 Source

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

Since: base-4.10.0.0

Constructors

HRefl :: a :~~: a
Instances
Instances details
Category ((:~~:) :: k -> k -> Type)

Since: base-4.10.0.0
Instance details

Defined in Control.Category

Methods

id :: forall (a :: k0). a :~~: a Source

(.) :: forall (b :: k0) (c :: k0) (a :: k0). (b :~~: c) -> (a :~~: b) -> a :~~: c Source

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

Since: base-4.10.0.0
Instance details

Defined in Data.Type.Equality

Methods

testEquality :: forall (a0 :: k0) (b :: k0). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) Source

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

Since: base-4.10.0.0
Instance details

Defined in Data.Type.Coercion

Methods

testCoercion :: forall (a0 :: k0) (b :: k0). (a :~~: a0) -> (a :~~: b) -> Maybe (Coercion a0 b) Source

a ~~ b => Bounded (a :~~: b)

Since: base-4.10.0.0
Instance details

Defined in Data.Type.Equality

Methods

minBound :: a :~~: b Source

maxBound :: a :~~: b Source

a ~~ b => Enum (a :~~: b)

Since: base-4.10.0.0
Instance details

Defined in Data.Type.Equality

Methods

succ :: (a :~~: b) -> a :~~: b Source

pred :: (a :~~: b) -> a :~~: b Source

toEnum :: Int -> a :~~: b Source

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)

Since: base-4.10.0.0
Instance details

Defined in Data.Type.Equality

Methods

(==) :: (a :~~: b) -> (a :~~: b) -> Bool Source

(/=) :: (a :~~: b) -> (a :~~: b) -> Bool Source

(Typeable i, Typeable j, Typeable a, Typeable b, a ~~ b) => Data (a :~~: b)

Since: base-4.10.0.0
Instance details

Defined in Data.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 :~~: b Source

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~~: b) -> r Source

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~~: b) -> r Source

gmapQ :: (forall d. Data d => d -> u) -> (a :~~: b) -> [u] Source

gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~~: b) -> u Source

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)

Since: base-4.10.0.0
Instance details

Defined in Data.Type.Equality

Methods

compare :: (a :~~: b) -> (a :~~: b) -> Ordering Source

(<) :: (a :~~: b) -> (a :~~: b) -> Bool Source

(<=) :: (a :~~: b) -> (a :~~: b) -> Bool Source

(>) :: (a :~~: b) -> (a :~~: b) -> Bool Source

(>=) :: (a :~~: b) -> (a :~~: b) -> Bool Source

max :: (a :~~: b) -> (a :~~: b) -> a :~~: b Source

min :: (a :~~: b) -> (a :~~: b) -> a :~~: b Source

a ~~ b => Read (a :~~: b)

Since: base-4.10.0.0
Instance details

Defined in Data.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)

Since: base-4.10.0.0
Instance details

Defined in Data.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 :~: a Source

Symmetry of equality

trans :: (a :~: b) -> (b :~: c) -> a :~: c Source

Transitivity of equality

castWith :: (a :~: b) -> a -> b Source

Type-safe cast, using propositional equality

gcastWith :: (a :~: b) -> (a ~ b => r) -> r Source

Generalized form of type-safe cast using propositional equality

apply :: (f :~: g) -> (a :~: b) -> f a :~: g b Source

Apply one equality to another, respectively

inner :: (f a :~: g b) -> a :~: b Source

Extract equality of the arguments from an equality of applied types

outer :: (f a :~: g b) -> f :~: g Source

Extract equality of type constructors from an equality of applied types

Inferring equality from other types

class TestEquality f where Source

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

Methods

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

Conditionally prove the equality of a and b.

Instances
Instances details
TestEquality (TypeRep :: k -> Type)
Instance details

Defined in Data.Typeable.Internal

Methods

testEquality :: forall (a :: k0) (b :: k0). TypeRep a -> TypeRep b -> Maybe (a :~: b) Source

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

Since: base-4.7.0.0
Instance details

Defined in Data.Type.Equality

Methods

testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Source

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

Since: base-4.10.0.0
Instance details

Defined in Data.Type.Equality

Methods

testEquality :: forall (a0 :: k0) (b :: k0). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) Source

TestEquality f => TestEquality (Compose f g :: k2 -> Type)

The deduction (via generativity) that if g x :~: g y then x :~: y.

Since: base-4.14.0.0
Instance details

Defined in Data.Functor.Compose

Methods

testEquality :: forall (a :: k) (b :: k). Compose f g a -> Compose f g b -> Maybe (a :~: b) Source

Boolean type-level equality

type family a == b where ... infix 4 Source

A type family to compute Boolean equality.

Equations

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

© The University of Glasgow and others
Licensed under a BSD-style license (see top of the page).
https://downloads.haskell.org/~ghc/8.10.2/docs/html/libraries/base-4.14.1.0/Data-Type-Equality.html