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

Data.Type.Equality

Contents

The equality type
Working with equality
Inferring equality from other types
Boolean type-level equality

Description

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

Since: 4.7.0.0

Synopsis

The equality type

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: 4.7.0.0

Constructors

Refl :: a :~: a

Instances

Category k ((:~:) k) Source
Methods id :: (k :~: a) a Source (.) :: (k :~: b) c -> (k :~: a) b -> (k :~: a) c Source
TestEquality k ((:~:) k a) Source
Methods testEquality :: (k :~: a) b -> (k :~: a) c -> Maybe ((k :~: b) c) Source
TestCoercion k ((:~:) k a) Source
Methods testCoercion :: (k :~: a) b -> (k :~: a) c -> Maybe (Coercion k b c) Source
(~) k a b => Bounded ((:~:) k a b) Source
Methods minBound :: (k :~: a) b Source maxBound :: (k :~: a) b Source
(~) k a b => Enum ((:~:) k a b) Source
Methods succ :: (k :~: a) b -> (k :~: a) b Source pred :: (k :~: a) b -> (k :~: a) b Source toEnum :: Int -> (k :~: a) b Source fromEnum :: (k :~: a) b -> Int Source enumFrom :: (k :~: a) b -> [(k :~: a) b] Source enumFromThen :: (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] Source enumFromTo :: (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] Source enumFromThenTo :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] Source
Eq ((:~:) k a b) Source
Methods (==) :: (k :~: a) b -> (k :~: a) b -> Bool (/=) :: (k :~: a) b -> (k :~: a) b -> Bool
((~) * a b, Data a) => Data ((:~:) * a b) Source
Methods gfoldl :: (forall d e. Data d => c (d -> e) -> d -> c e) -> (forall g. g -> c g) -> (* :~: a) b -> c ((* :~: a) b) Source gunfold :: (forall d r. Data d => c (d -> 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 c. Data c => c -> c) -> (* :~: a) b -> (* :~: a) b Source gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (* :~: a) b -> r Source gmapQr :: (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 ((:~:) k a b) Source
Methods compare :: (k :~: a) b -> (k :~: a) b -> Ordering (<) :: (k :~: a) b -> (k :~: a) b -> Bool (<=) :: (k :~: a) b -> (k :~: a) b -> Bool (>) :: (k :~: a) b -> (k :~: a) b -> Bool (>=) :: (k :~: a) b -> (k :~: a) b -> Bool max :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b min :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b
(~) k a b => Read ((:~:) k a b) Source
Methods readsPrec :: Int -> ReadS ((k :~: a) b) Source readList :: ReadS [(k :~: a) b] Source readPrec :: ReadPrec ((k :~: a) b) Source readListPrec :: ReadPrec [(k :~: a) b] Source
Show ((:~:) k a b) Source
Methods showsPrec :: Int -> (k :~: a) b -> ShowS Source show :: (k :~: a) b -> String Source showList :: [(k :~: 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 a 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

TestEquality k ((:~:) k a) Source
Methods testEquality :: (k :~: a) b -> (k :~: a) c -> Maybe ((k :~: b) c) Source

Boolean type-level equality

type family a == b :: Bool infix 4 Source

A type family to compute Boolean equality. Instances are provided only for open kinds, such as * and function kinds. Instances are also provided for datatypes exported from base. A poly-kinded instance is not provided, as a recursive definition for algebraic kinds is generally more useful.

Instances

type (==) Bool a b Source
type (==) Ordering a b Source
type (==) * a b Source
type (==) Nat a b Source
type (==) Symbol a b Source
type (==) () a b Source
type (==) [k] a b Source
type (==) (Maybe k) a b Source
type (==) (k -> k1) a b Source
type (==) (Either k k1) a b Source
type (==) ((,) k k1) a b Source
type (==) ((,,) k k1 k2) a b Source
type (==) ((,,,) k k1 k2 k3) a b Source
type (==) ((,,,,) k k1 k2 k3 k4) a b Source
type (==) ((,,,,,) k k1 k2 k3 k4 k5) a b Source
type (==) ((,,,,,,) k k1 k2 k3 k4 k5 k6) a b Source
type (==) ((,,,,,,,) k k1 k2 k3 k4 k5 k6 k7) a b Source
type (==) ((,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8) a b Source
type (==) ((,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9) a b Source
type (==) ((,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10) a b Source
type (==) ((,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11) a b Source
type (==) ((,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12) a b Source
type (==) ((,,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13) a b Source
type (==) ((,,,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 k14) a b Source