| 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
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
- 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
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
Instances
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.
Methods
testEquality ∷ f a → f b → Maybe (a :~: b) Source
Conditionally prove the equality of a and b.
Instances
| TestEquality k ((:~:) k a) |
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 | |
| 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 (==) (k → k1) a b | |
| type (==) (Either k k1) a b | |
| type (==) ((,) k k1) a b | |
| type (==) ((,,) k k1 k2) a b | |
| type (==) ((,,,) k k1 k2 k3) a b | |
| type (==) ((,,,,) k k1 k2 k3 k4) a b | |
| type (==) ((,,,,,) k k1 k2 k3 k4 k5) a b | |
| type (==) ((,,,,,,) k k1 k2 k3 k4 k5 k6) a b | |
| type (==) ((,,,,,,,) k k1 k2 k3 k4 k5 k6 k7) a b | |
| type (==) ((,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8) a b | |
| type (==) ((,,,,,,,,,) 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 | |
| type (==) ((,,,,,,,,,,,) 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 | |
| type (==) ((,,,,,,,,,,,,,) 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 |