Maintainer | libraries@haskell.org |
---|---|

Stability | experimental |

Portability | not portable |

Safe Haskell | None |

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.