Data.Type.Equality

base-4.12.0.0: Basic libraries

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

- The equality types
- 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: base-4.7.0.0

Synopsis

- data a :~: b where
  - 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
- class TestEquality f where
  - testEquality :: f a -> f b -> Maybe (a :~: b)
- type family (a :: k) == (b :: k) :: Bool where ...

# The equality types

data a :~: b where infix 4 #

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

Category ((:~:) :: k -> k -> Type) # | Since: base-4.7.0.0
Instance details Defined in Control.Category Methods id :: a :~: a # (.) :: (b :~: c) -> (a :~: b) -> a :~: c #
TestEquality ((:~:) a :: k -> Type) # | Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods testEquality :: (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #
TestCoercion ((:~:) a :: k -> Type) # | Since: base-4.7.0.0
Instance details Defined in Data.Type.Coercion Methods testCoercion :: (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) #
a ~ b => Bounded (a :~: b) # | Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods minBound :: a :~: b # maxBound :: a :~: b #
a ~ b => Enum (a :~: b) # | Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods succ :: (a :~: b) -> a :~: b # pred :: (a :~: b) -> a :~: b # toEnum :: Int -> a :~: b # fromEnum :: (a :~: b) -> Int # enumFrom :: (a :~: b) -> [a :~: b] # enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] # enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] # enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] #
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) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) # toConstr :: (a :~: b) -> Constr # dataTypeOf :: (a :~: b) -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r # gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) #
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) # readList :: ReadS [a :~: b] # readPrec :: ReadPrec (a :~: b) # readListPrec :: ReadPrec [a :~: b] #
Show (a :~: b) # | Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS # show :: (a :~: b) -> String # showList :: [a :~: b] -> ShowS #

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 :: k1) :~~: (b :: k2) where infix 4 #

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

Category ((:~~:) :: k -> k -> Type) # | Since: base-4.10.0.0
Instance details Defined in Control.Category Methods id :: a :~~: a # (.) :: (b :~~: c) -> (a :~~: b) -> a :~~: c #
TestEquality ((:~~:) a :: k -> Type) # | Since: base-4.10.0.0
Instance details Defined in Data.Type.Equality Methods testEquality :: (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) #
TestCoercion ((:~~:) a :: k -> Type) # | Since: base-4.10.0.0
Instance details Defined in Data.Type.Coercion Methods testCoercion :: (a :~~: a0) -> (a :~~: b) -> Maybe (Coercion a0 b) #
a ~~ b => Bounded (a :~~: b) # | Since: base-4.10.0.0
Instance details Defined in Data.Type.Equality Methods minBound :: a :~~: b # maxBound :: a :~~: b #
a ~~ b => Enum (a :~~: b) # | Since: base-4.10.0.0
Instance details Defined in Data.Type.Equality Methods succ :: (a :~~: b) -> a :~~: b # pred :: (a :~~: b) -> a :~~: b # toEnum :: Int -> a :~~: b # fromEnum :: (a :~~: b) -> Int # enumFrom :: (a :~~: b) -> [a :~~: b] # enumFromThen :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] # enumFromTo :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] # enumFromThenTo :: (a :~~: b) -> (a :~~: b) -> (a :~~: b) -> [a :~~: b] #
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) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~~: b) # toConstr :: (a :~~: b) -> Constr # dataTypeOf :: (a :~~: b) -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~~: b)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~~: b)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~~: b) -> a :~~: b # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~~: b) -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~~: b) -> r # gmapQ :: (forall d. Data d => d -> u) -> (a :~~: b) -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~~: b) -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~~: b) -> m (a :~~: b) #
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) # readList :: ReadS [a :~~: b] # readPrec :: ReadPrec (a :~~: b) # readListPrec :: ReadPrec [a :~~: b] #
Show (a :~~: b) # | Since: base-4.10.0.0
Instance details Defined in Data.Type.Equality Methods showsPrec :: Int -> (a :~~: b) -> ShowS # show :: (a :~~: b) -> String # showList :: [a :~~: b] -> ShowS #

# Working with equality

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

Symmetry of equality

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

Transitivity of equality

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

Type-safe cast, using propositional equality

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

Generalized form of type-safe cast using propositional equality

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

Apply one equality to another, respectively

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

Extract equality of the arguments from an equality of applied types

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

Extract equality of type constructors from an equality of applied types

# Inferring equality from other types

class TestEquality f where #

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) #

Conditionally prove the equality of `a` and `b`.

Instances

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

# Boolean type-level equality

type family (a :: k) == (b :: k) :: Bool where ... infix 4 #

A type family to compute Boolean equality.

Equations

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