| 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
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
| 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) -> rSource
Generalized form of type-safe cast using propositional equality
inner :: (f a :~: g b) -> a :~: bSource
Extract equality of the arguments from an equality of a applied types
outer :: (f a :~: g b) -> f :~: gSource
Extract equality of type constructors from an equality of applied types
Inferring equality from other types
class TestEquality f whereSource
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 :: BoolSource
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.