License | BSD-style (see the LICENSE file in the distribution) |
---|---|
Maintainer | libraries@haskell.org |
Stability | experimental |
Portability | not portable |
Safe Haskell | None |
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
- 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 == b :: Bool
The equality type
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) | |
TestEquality k ((:~:) k a) | |
TestCoercion k ((:~:) k a) | |
Typeable (k -> k -> *) ((:~:) k) | |
(~) k a b => Bounded ((:~:) k a b) | |
(~) k a b => Enum ((:~:) k a b) | |
Eq ((:~:) k a b) | |
((~) * a b, Data a) => Data ((:~:) * a b) | |
Ord ((:~:) k a b) | |
(~) k a b => Read ((:~:) k a b) | |
Show ((:~:) k a b) |
Working with equality
gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r Source
Generalized form of type-safe cast using propositional equality
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.
testEquality :: f a -> f b -> Maybe (a :~: b) Source
Conditionally prove the equality of a
and b
.
TestEquality k ((:~:) k a) |
Boolean type-level equality
type family a == b :: Bool 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 = EqBool a b | |
type (==) Ordering a b = EqOrdering a b | |
type (==) * a b = EqStar a b | |
type (==) Nat a b = EqNat a b | |
type (==) Symbol a b = EqSymbol a b | |
type (==) () a b = EqUnit a b | |
type (==) [k] a b = EqList k a b | |
type (==) (Maybe k) a b = EqMaybe k a b | |
type (==) (k -> k1) a b = EqArrow k k1 a b | |
type (==) (Either k k1) a b = EqEither k k1 a b | |
type (==) ((,) k k1) a b = Eq2 k k1 a b | |
type (==) ((,,) k k1 k2) a b = Eq3 k k1 k2 a b | |
type (==) ((,,,) k k1 k2 k3) a b = Eq4 k k1 k2 k3 a b | |
type (==) ((,,,,) k k1 k2 k3 k4) a b = Eq5 k k1 k2 k3 k4 a b | |
type (==) ((,,,,,) k k1 k2 k3 k4 k5) a b = Eq6 k k1 k2 k3 k4 k5 a b | |
type (==) ((,,,,,,) k k1 k2 k3 k4 k5 k6) a b = Eq7 k k1 k2 k3 k4 k5 k6 a b | |
type (==) ((,,,,,,,) k k1 k2 k3 k4 k5 k6 k7) a b = Eq8 k k1 k2 k3 k4 k5 k6 k7 a b | |
type (==) ((,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8) a b = Eq9 k k1 k2 k3 k4 k5 k6 k7 k8 a b | |
type (==) ((,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9) a b = Eq10 k k1 k2 k3 k4 k5 k6 k7 k8 k9 a b | |
type (==) ((,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10) a b = Eq11 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 a b | |
type (==) ((,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11) a b = Eq12 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 a b | |
type (==) ((,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12) a b = Eq13 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 a b | |
type (==) ((,,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13) a b = Eq14 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 a b | |
type (==) ((,,,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 k14) a b = Eq15 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 k14 a b |