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.