base-compat-batteries-0.12.3: base-compat with extra batteries

Safe Haskell | Trustworthy
Language | Haskell2010

Data.Type.Equality.Compat

Contents

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

Synopsis

- data (a :: k) :~: (b :: k) where
  - Refl :: forall {k} (a :: k). a :~: a
- class a ~# b => (a :: k0) ~~ (b :: k1)
- data (a :: k1) :~~: (b :: k2) where
  - HRefl :: forall {k1} (a :: k1). a :~~: a
- sym :: forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a
- trans :: forall {k} (a :: k) (b :: k) (c :: k). (a :~: b) -> (b :~: c) -> a :~: c
- castWith :: (a :~: b) -> a -> b
- gcastWith :: forall {k} (a :: k) (b :: k) r. (a :~: b) -> (a ~ b => r) -> r
- apply :: forall {k1} {k2} (f :: k1 -> k2) (g :: k1 -> k2) (a :: k1) (b :: k1). (f :~: g) -> (a :~: b) -> f a :~: g b
- inner :: forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (g :: k1 -> k2) (b :: k1). (f a :~: g b) -> a :~: b
- outer :: forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (g :: k1 -> k2) (b :: k1). (f a :~: g b) -> f :~: g
- class TestEquality (f :: k -> Type) where
  - testEquality :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
- type family (a :: k) == (b :: k) :: Bool where ...

# The equality types

data (a :: k) :~: (b :: k) 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 :: forall {k} (a :: k). a :~: a |

#### Instances

Instances details

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

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

class a ~# b => (a :: k0) ~~ (b :: k1) infix 4 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.

In `0.7.0`, the fixity was set to `infix 4` to match the fixity of `:~~:`.

data (a :: k1) :~~: (b :: k2) 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 :: forall {k1} (a :: k1). a :~~: a |

#### Instances

Instances details

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

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

# Working with equality

sym :: forall {k} (a :: k) (b :: k). (a :~: b) -> b :~: a Source #

Symmetry of equality

trans :: forall {k} (a :: k) (b :: k) (c :: k). (a :~: b) -> (b :~: c) -> a :~: c Source #

Transitivity of equality

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

Type-safe cast, using propositional equality

gcastWith :: forall {k} (a :: k) (b :: k) r. (a :~: b) -> (a ~ b => r) -> r Source #

Generalized form of type-safe cast using propositional equality

apply :: forall {k1} {k2} (f :: k1 -> k2) (g :: k1 -> k2) (a :: k1) (b :: k1). (f :~: g) -> (a :~: b) -> f a :~: g b Source #

Apply one equality to another, respectively

inner :: forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (g :: k1 -> k2) (b :: k1). (f a :~: g b) -> a :~: b Source #

Extract equality of the arguments from an equality of applied types

outer :: forall {k1} {k2} (f :: k1 -> k2) (a :: k1) (g :: k1 -> k2) (b :: k1). (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 :: k -> Type) where Source #

This class contains types where you can learn the equality of two types from information contained in terms.

The result should be `Just Refl` if and only if the types applied to `f` are equal:

    TestEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b

Typically, only singleton types should inhabit this class. In that case type argument equality coincides with term equality:

    TestEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b ⟺ x = y

    isJust (TestEquality x y) = x == y

Singleton types are not required, however, and so the latter two would-be laws are not in fact valid in general.

Methods

testEquality :: forall (a :: k) (b :: k). 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 :: k) == (b :: k) :: Bool where ... infix 4 Source #

A type family to compute Boolean equality.

Equations

(f a :: k2) == (g b :: k2) = (f == g) && (a == b) |
(a :: k) == (a :: k) = 'True |
(_1 :: k) == (_2 :: k) = 'False |