Data.GADT.Compare

Documentation

data a := b where

A GADT witnessing equality of two types. Its only inhabitant is Refl.

Constructors

Refl :: a := a

Instances

Typeable2 :=

GRead (:= a)

GShow (:= a)

GCompare (:= a)

GEq (:= a)

Ord a => OrdTag (:= a)

Eq a => EqTag (:= a)

Read a => ReadTag (:= a)

Show a => ShowTag (:= a)

Eq (:= a b)

Ord (:= a b)

Read (:= a a)

Show (:= a b)

class GEq f where

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

Methods

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

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)

Instances

GEq (:= a)

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

If f has a GEq instance, this function makes a suitable default implementation of '(==)'.

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

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

data GOrdering a b where

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.

Constructors

GLT :: GOrdering a b

GEQ :: GOrdering t t

GGT :: GOrdering a b

Instances

Typeable2 GOrdering

GRead (GOrdering a)

GShow (GOrdering a)

Show a => ShowTag (GOrdering a)

Eq (GOrdering a b)

Ord (GOrdering a b)

Show (GOrdering a b)

weakenOrdering :: GOrdering a b -> Ordering

TODO: Think of a better name

This operation forgets the phantom types of a GOrdering value.

class GEq f => GCompare f where

Type class for orderable GADT-like structures. When 2 things are equal, must return a witness that their parameter types are equal as well (GEQ). |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).

Methods

gcompare :: f a -> f b -> GOrdering a b

Instances

GCompare (:= a)