Data.Type.Equality

Type equality, coercion/cast and other operations.

Documentation

data a :=: b where

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.

Constructors

Refl :: a :=: a

Instances

EqT k (:=: k a)

Category (:=: *)

Read (:=: k a a)

We can only read values if the result is a :=: a, not a :=: b since that is not true, in general. We just parse the string Refl, optionally surrounded with parentheses, and return Refl.

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.

sym :: (a :=: b) -> b :=: a

Equality is symmetric.

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

Equality is transitive. This is the same as (>>>) from the Category instance, but also works in GHC 6.8.

subst :: (a :=: b) -> f a -> f b

Equality is substitutive. This is defined directly, but can also be defined as coerce . cong.

subst2 :: (a :=: b) -> f (g a) -> f (g b)

Substitution inside nested type constructors. This is equivalent to coerce . cong . cong.

cong :: (a :=: b) -> f a :=: f b

Equality is congruential.

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

Congruence for type constructors with two parameters.

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

Congruence for type constructors with three parameters.

coerce :: (a :=: b) -> a -> b

Coerce a type to another using an equality proof.

class EqT f where

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.

Methods

eqT :: f a -> f b -> Maybe (a :=: b)

Instances

EqT k (:=: k a)

class EqT2 f where

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

Methods

eqT2 :: f a b -> f c d -> (Maybe (a :=: c), Maybe (b :=: d))

class EqT3 f where

A type class for constructing equality proofs for type constructor with three parameters. If you find a use for this, let me know.

Methods

eqT3 :: f a b c -> f a' b' c' -> (Maybe (a :=: a'), Maybe (b :=: b'), Maybe (c :=: c'))