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)

In order to make a Read instance for DSum tag, tag must be able to parse itself as well as any value of the tagged type. GRead together with this class provides the interface by which it can do so.

ReadTag tag => t is conceptually equivalent to something like this imaginary syntax: (forall a. Inhabited (tag a) => Read a) => t, where Inhabited is an imaginary predicate that characterizes non-empty types, and a does not occur free in t.

The Tag example type introduced in the DSum section could be given the following instances:

 instance GRead Tag where
     greadsPrec _p str = case tag of
        "AString"   -> [(\k -> k AString, rest)]
        "AnInt"     -> [(\k -> k AnInt,   rest)]
        _           -> []
        where (tag, rest) = break isSpace str
 instance ReadTag Tag where
     readTaggedPrec AString = readsPrec
     readTaggedPrec AnInt   = readsPrec

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)