type-equality-0.1.2: Type equality, coercion/cast and other operations.

Data.Type.Equality

Description

Type equality, coercion/cast and other operations.

Synopsis

# Documentation

data a :=: b whereSource

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 :=: aSource

Equality is symmetric.

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.

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

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

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

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

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

Equality is congruential.

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.

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

Coerce a type to another using an equality proof.

class EqT f whereSource

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)Source

Instances

 EqT k (:=: k a)

class EqT2 f whereSource

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))Source

class EqT3 f whereSource

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'))Source