Stability | Experimental |
---|---|

Maintainer | Erik Hesselink <hesselink@gmail.com> |

Type equality, coercion/cast and other operations.

- data a :=: b where
- sym :: (a :=: b) -> b :=: a
- trans :: (a :=: b) -> (b :=: c) -> a :=: c
- subst :: (a :=: b) -> f a -> f b
- cong :: (a :=: b) -> f a :=: f b
- cong2 :: (a :=: b) -> (c :=: d) -> f a c :=: f b d
- cong3 :: (a :=: a') -> (b :=: b') -> (c :=: c') -> f a b c :=: f a' b' c'
- coerce :: (a :=: b) -> a -> b
- class EqT f where
- class EqT2 f where
- class EqT3 f where

# Documentation

Type equality. A value of `a :=: b`

is a proof that types `a`

and
`b`

are equal. By pattern matching on `Refl`

this fact is
introduced to the type checker.

Category :=: | |

EqT (:=: a) | |

Read (:=: a a) | We can only read values if the result is |

Show (:=: a b) | Any value is just shown as Refl, but this cannot be derived for a GADT, so it is defined here manually. |

trans :: (a :=: b) -> (b :=: c) -> a :=: cSource

Equality is transitive. This is the same as (>>>) from the `Category`

instance, but also works in GHC 6.8.

cong2 :: (a :=: b) -> (c :=: d) -> f a c :=: f b dSource

Congruence for type constructors with two parameters.

cong3 :: (a :=: a') -> (b :=: b') -> (c :=: c') -> f a b c :=: f a' b' c'Source

Congruence for type constructors with three parameters.

A type class for constructing equality proofs. This is as close
as we can get to decidable equality on types. Note that `f`

must be
a GADT to be able to define `eqT`

.

A type class for constructing equality proofs for type constructor with two parameters. Can be useful when representing relations between types.