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

Stability Experimental Erik Hesselink Safe-Inferred

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`.

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