|Maintainer||Erik Hesselink <firstname.lastname@example.org>|
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
Type equality. A value of
a :=: b is a proof that types
b are equal. By pattern matching on
Refl this fact is
introduced to the type checker.
|EqT k (:=: k a)|
|Category (:=: *)|
|Read (:=: k a a)|
|Show (:=: k a b)|
Any value is just shown as Refl, but this cannot be derived for a GADT, so it is defined here manually.
Equality is transitive. This is the same as (>>>) from the
instance, but also works in GHC 6.8.
Congruence for type constructors with two parameters.
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
A type class for constructing equality proofs for type constructor with two parameters. Can be useful when representing relations between types.