License | BSD-style (see the LICENSE file in the distribution) |
---|---|
Maintainer | [email protected] |
Stability | experimental |
Portability | not portable |
Safe Haskell | Trustworthy |
Language | Haskell2010 |
Definition of propositional equality (:~:)
. Pattern-matching on a variable of type (a :~: b)
produces a proof that a ~ b
.
Since: 4.7.0.0
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
Category k ((:~:) k) | Since: 4.7.0.0 |
TestEquality k ((:~:) k a) | Since: 4.7.0.0 |
TestCoercion k ((:~:) k a) | Since: 4.7.0.0 |
(~) k a b => Bounded ((:~:) k a b) | Since: 4.7.0.0 |
(~) k a b => Enum ((:~:) k a b) | Since: 4.7.0.0 |
Eq ((:~:) k a b) | |
((~) * a b, Data a) => Data ((:~:) * a b) | Since: 4.7.0.0 |
Ord ((:~:) k a b) | |
(~) k a b => Read ((:~:) k a b) | Since: 4.7.0.0 |
Show ((:~:) k a b) | |
class (~#) k0 k1 a b => (k0 ~~ k1) (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 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: 4.10.0.0
Category k ((:~~:) k k) | Since: 4.10.0.0 |
TestEquality k ((:~~:) k1 k a) | Since: 4.10.0.0 |
TestCoercion k ((:~~:) k1 k a) | Since: 4.10.0.0 |
(~~) k1 k2 a b => Bounded ((:~~:) k1 k2 a b) | Since: 4.10.0.0 |
(~~) k1 k2 a b => Enum ((:~~:) k1 k2 a b) | Since: 4.10.0.0 |
Eq ((:~~:) k1 k2 a b) | Since: 4.10.0.0 |
(Typeable * i2, Typeable * j2, Typeable i2 a, Typeable j2 b, (~~) i2 j2 a b) => Data ((:~~:) i2 j2 a b) | Since: 4.10.0.0 |
Ord ((:~~:) k1 k2 a b) | Since: 4.10.0.0 |
(~~) k1 k2 a b => Read ((:~~:) k1 k2 a b) | Since: 4.10.0.0 |
Show ((:~~:) k1 k2 a b) | Since: 4.10.0.0 |
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
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.
testEquality :: f a -> f b -> Maybe (a :~: b) Source
Conditionally prove the equality of a
and b
.
TestEquality k (TypeRep k) | |
TestEquality k ((:~:) k a) | Since: 4.7.0.0 |
TestEquality k ((:~~:) k1 k a) | Since: 4.10.0.0 |
type family (a :: k) == (b :: k) :: 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.
type (==) Bool a b | |
type (==) Ordering a b | |
type (==) * a b | |
type (==) Nat a b | |
type (==) Symbol a b | |
type (==) () a b | |
type (==) [k] a b | |
type (==) (Maybe k) a b | |
type (==) (k1 -> k2) a b | |
type (==) (Either k1 k2) a b | |
type (==) (k1, k2) a b | |
type (==) (k1, k2, k3) a b | |
type (==) (k1, k2, k3, k4) a b | |
type (==) (k1, k2, k3, k4, k5) a b | |
type (==) (k1, k2, k3, k4, k5, k6) a b | |
type (==) (k1, k2, k3, k4, k5, k6, k7) a b | |
type (==) (k1, k2, k3, k4, k5, k6, k7, k8) a b | |
type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9) a b | |
type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10) a b | |
type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11) a b | |
type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11, k12) a b | |
type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11, k12, k13) a b | |
type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11, k12, k13, k14) a b | |
type (==) (k1, k2, k3, k4, k5, k6, k7, k8, k9, k10, k11, k12, k13, k14, k15) a b | |
© The University of Glasgow and others
Licensed under a BSD-style license (see top of the page).
https://downloads.haskell.org/~ghc/8.2.1/docs/html/libraries/base-4.10.0.0/Data-Type-Equality.html