| Maintainer | libraries@haskell.org |
|---|---|
| Stability | experimental |
| Portability | not portable |
| Safe Haskell | None |
Data.Type.Equality
Description
Definition of propositional equality (:=:). Pattern-matching on a variable
of type (a :=: b) produces a proof that a ~ b.
- data a :=: b where
- sym :: (a :=: b) -> b :=: a
- trans :: (a :=: b) -> (b :=: c) -> a :=: c
- coerce :: (a :=: b) -> a -> b
- liftEq :: (a :=: b) -> f a :=: f b
- liftEq2 :: (a :=: a') -> (b :=: b') -> f a b :=: f a' b'
- liftEq3 :: (a :=: a') -> (b :=: b') -> (c :=: c') -> f a b c :=: f a' b' c'
- liftEq4 :: (a :=: a') -> (b :=: b') -> (c :=: c') -> (d :=: d') -> f a b c d :=: f a' b' c' d'
- lower :: (f a :=: f b) -> a :=: b
- class EqualityT f where
Documentation
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.
liftEq2 :: (a :=: a') -> (b :=: b') -> f a b :=: f a' b'Source
Lift equality into a binary type constructor
liftEq3 :: (a :=: a') -> (b :=: b') -> (c :=: c') -> f a b c :=: f a' b' c'Source
Lift equality into a ternary type constructor
liftEq4 :: (a :=: a') -> (b :=: b') -> (c :=: c') -> (d :=: d') -> f a b c d :=: f a' b' c' d'Source
Lift equality into a quaternary type constructor
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.