base- Basic libraries
Portabilitynot portable
Safe HaskellNone



Definition of propositional equality (:=:). Pattern-matching on a variable of type (a :=: b) produces a proof that a ~ b.



data a :=: b whereSource

Propositional equality. If a :=: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :=: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.


Refl :: a :=: a 


Category k (:=: k) 
EqualityT k (:=: k a) 
Typeable (k -> k -> *) (:=: k) 
Bounded (:=: k a a) 
Enum (:=: k a a) 
Eq (:=: k a b) 
(Typeable * a, Data a) => Data (:=: * a a) 
Ord (:=: k a b) 
Read (:=: k a a) 
Show (:=: k a b) 

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

Symmetry of equality

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

Transitivity of equality

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

Type-safe cast, using propositional equality

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

Lift equality into a unary type constructor

liftEq2 :: (a :=: a') -> (b :=: b') -> f a b :=: f a' b'Source

Lift equality into a binary type constructor

liftEq3 :: (a :=: a') -> (b :=: b') -> (c :=: c') -> f a b c :=: f a' b' c'Source

Lift equality into a ternary type constructor

liftEq4 :: (a :=: a') -> (b :=: b') -> (c :=: c') -> (d :=: d') -> f a b c d :=: f a' b' c' d'Source

Lift equality into a quaternary type constructor

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

Lower equality from a parameterized type into the parameters

class EqualityT f whereSource

This class contains types where you can learn the equality of two types from information contained in terms. Typically, only singleton types should inhabit this class.


equalsT :: f a -> f b -> Maybe (a :=: b)Source

Conditionally prove the equality of a and b.


EqualityT k (:=: k a)