Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

# Equality

A class for type-contexts which contain enough information to (at least in some cases) decide the equality of types occurring within them.

geq :: f a -> f b -> Maybe (a :~: b) Source #

Produce a witness of type-equality, if one exists.

A handy idiom for using this would be to pattern-bind in the Maybe monad, eg.:

extract :: GEq tag => tag a -> DSum tag -> Maybe a extract t1 (t2 :=> x) = do Refl <- geq t1 t2 return x

Or in a list comprehension:

extractMany :: GEq tag => tag a -> [DSum tag] -> [a] extractMany t1 things = [ x | (t2 :=> x) <- things, Refl <- maybeToList (geq t1 t2)]

(Making use of the `DSum`

type from Data.Dependent.Sum in both examples)

defaultEq :: GEq f => f a -> f b -> Bool Source #

If `f`

has a `GEq`

instance, this function makes a suitable default
implementation of '(==)'.

defaultNeq :: GEq f => f a -> f b -> Bool Source #

If `f`

has a `GEq`

instance, this function makes a suitable default
implementation of '(/=)'.

# Total order comparison

class GEq f => GCompare f where Source #

Type class for comparable GADT-like structures. When 2 things are equal,
must return a witness that their parameter types are equal as well (`GEQ`

).

defaultCompare :: GCompare f => f a -> f b -> Ordering Source #

data GOrdering a b where Source #

A type for the result of comparing GADT constructors; the type parameters of the GADT values being compared are included so that in the case where they are equal their parameter types can be unified.

## Instances

GRead (GOrdering a :: k -> Type) Source # | |

Defined in Data.GADT.Internal | |

GShow (GOrdering a :: k -> Type) Source # | |

Defined in Data.GADT.Internal | |

Eq (GOrdering a b) Source # | |

Ord (GOrdering a b) Source # | |

Defined in Data.GADT.Internal compare :: GOrdering a b -> GOrdering a b -> Ordering # (<) :: GOrdering a b -> GOrdering a b -> Bool # (<=) :: GOrdering a b -> GOrdering a b -> Bool # (>) :: GOrdering a b -> GOrdering a b -> Bool # (>=) :: GOrdering a b -> GOrdering a b -> Bool # | |

Show (GOrdering a b) Source # | |