Safe Haskell	Safe
Language	Haskell2010

Data.GADT.Compare

Contents

Equality
Total order comparison

Synopsis

class GEq f where
- geq :: f a -> f b -> Maybe (a :~: b)
defaultEq :: GEq f => f a -> f b -> Bool
defaultNeq :: GEq f => f a -> f b -> Bool
class GEq f => GCompare f where
- gcompare :: f a -> f b -> GOrdering a b
defaultCompare :: GCompare f => f a -> f b -> Ordering
data GOrdering a b where
- GLT :: GOrdering a b
- GEQ :: GOrdering t t
- GGT :: GOrdering a b

Equality

class GEq f where Source #

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) 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)

Instances

Instances details

GEq ( TypeRep :: k -> Type ) Source #
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a :: k0) (b :: k0). TypeRep a -> TypeRep b -> Maybe (a :~: b) Source #
GEq ( (:~:) a :: k -> Type ) Source #
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Source #
( GEq a, GEq b) => GEq ( Product a b :: k -> Type ) Source #
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a0 :: k0) (b0 :: k0). Product a b a0 -> Product a b b0 -> Maybe (a0 :~: b0) Source #
( GEq a, GEq b) => GEq ( Sum a b :: k -> Type ) Source #
Instance details Defined in Data.GADT.Internal Methods geq :: forall (a0 :: k0) (b0 :: k0). Sum a b a0 -> Sum a b b0 -> Maybe (a0 :~: b0) Source #

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

Methods

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

Instances

Instances details

GCompare ( TypeRep :: k -> Type ) Source #
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a :: k0) (b :: k0). TypeRep a -> TypeRep b -> GOrdering a b Source #
GCompare ( (:~:) a :: k -> Type ) Source #
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> GOrdering a0 b Source #
( GCompare a, GCompare b) => GCompare ( Product a b :: k -> Type ) Source #
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a0 :: k0) (b0 :: k0). Product a b a0 -> Product a b b0 -> GOrdering a0 b0 Source #
( GCompare a, GCompare b) => GCompare ( Sum a b :: k -> Type ) Source #
Instance details Defined in Data.GADT.Internal Methods gcompare :: forall (a0 :: k0) (b0 :: k0). Sum a b a0 -> Sum a b b0 -> GOrdering a0 b0 Source #

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.

Constructors

GLT :: GOrdering a b
GEQ :: GOrdering t t
GGT :: GOrdering a b

Instances

Instances details

GRead ( GOrdering a :: k -> Type ) Source #
Instance details Defined in Data.GADT.Internal Methods greadsPrec :: Int -> GReadS ( GOrdering a) Source #
GShow ( GOrdering a :: k -> Type ) Source #
Instance details Defined in Data.GADT.Internal Methods gshowsPrec :: forall (a0 :: k0). Int -> GOrdering a a0 -> ShowS Source #
Eq ( GOrdering a b) Source #
Instance details Defined in Data.GADT.Internal Methods (==) :: GOrdering a b -> GOrdering a b -> Bool Source # (/=) :: GOrdering a b -> GOrdering a b -> Bool Source #
Ord ( GOrdering a b) Source #
Instance details Defined in Data.GADT.Internal Methods compare :: GOrdering a b -> GOrdering a b -> Ordering Source # (<) :: GOrdering a b -> GOrdering a b -> Bool Source # (<=) :: GOrdering a b -> GOrdering a b -> Bool Source # (>) :: GOrdering a b -> GOrdering a b -> Bool Source # (>=) :: GOrdering a b -> GOrdering a b -> Bool Source # max :: GOrdering a b -> GOrdering a b -> GOrdering a b Source # min :: GOrdering a b -> GOrdering a b -> GOrdering a b Source #
Show ( GOrdering a b) Source #
Instance details Defined in Data.GADT.Internal Methods showsPrec :: Int -> GOrdering a b -> ShowS Source # show :: GOrdering a b -> String Source # showList :: [ GOrdering a b] -> ShowS Source #