Data.GADT.Compare

Documentation

class GEq f => GCompare f where

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 (TypeRep :: k -> Type)

Defined in Data.GADT.Compare

Methods

gcompare :: TypeRep a -> TypeRep b -> GOrdering a b

GCompare ((:~:) a :: k -> Type)

Defined in Data.GADT.Compare

Methods

gcompare :: (a :~: a0) -> (a :~: b) -> GOrdering a0 b

(GCompare a, GCompare b) => GCompare (Product a b :: k -> Type)

Defined in Data.GADT.Compare

Methods

gcompare :: Product a b a0 -> Product a b b0 -> GOrdering a0 b0

(GCompare a, GCompare b) => GCompare (Sum a b :: k -> Type)

Defined in Data.GADT.Compare

Methods

gcompare :: Sum a b a0 -> Sum a b b0 -> GOrdering a0 b0

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

GRead (GOrdering a :: k -> Type)

Defined in Data.GADT.Compare

Methods

greadsPrec :: Int -> GReadS (GOrdering a)

GShow (GOrdering a :: k -> Type)

Defined in Data.GADT.Compare

Methods

gshowsPrec :: Int -> GOrdering a a0 -> ShowS

Eq (GOrdering a b)

Defined in Data.GADT.Compare

Methods

(==) :: GOrdering a b -> GOrdering a b -> Bool

(/=) :: GOrdering a b -> GOrdering a b -> Bool

Ord (GOrdering a b)

Defined in Data.GADT.Compare

Methods

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

max :: GOrdering a b -> GOrdering a b -> GOrdering a b

min :: GOrdering a b -> GOrdering a b -> GOrdering a b

Show (GOrdering a b)

Defined in Data.GADT.Compare

Methods

showsPrec :: Int -> GOrdering a b -> ShowS

show :: GOrdering a b -> String

showList :: [GOrdering a b] -> ShowS

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 (TypeRep :: k -> Type)

Defined in Data.GADT.Compare

Methods

geq :: TypeRep a -> TypeRep b -> Maybe (a :~: b)

GEq ((:~:) a :: k -> Type)

Defined in Data.GADT.Compare

Methods

geq :: (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b)

(GEq a, GEq b) => GEq (Product a b :: k -> Type)

Defined in Data.GADT.Compare

Methods

geq :: Product a b a0 -> Product a b b0 -> Maybe (a0 :~: b0)

(GEq a, GEq b) => GEq (Sum a b :: k -> Type)

Defined in Data.GADT.Compare

Methods

geq :: Sum a b a0 -> Sum a b b0 -> Maybe (a0 :~: b0)

type (:=) = (:~:)

Deprecated: use '(:~:)' from 'Data.Type,Equality'.

Backwards compatibility alias; as of GHC 7.8, this is the same as `(:~:)`.

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 '(/=)'.

weakenOrdering :: GOrdering a b -> Ordering

TODO: Think of a better name

This operation forgets the phantom types of a GOrdering value.

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

data (a :: k) :~: (b :: k) :: forall k. k -> k -> Type where infix 4

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.

Since: base-4.7.0.0

Constructors

Refl :: forall k (a :: k) (b :: k). a :~: a

Instances

TestEquality ((:~:) a :: k -> Type)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

testEquality :: (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b)

GRead ((:~:) a :: k -> Type)

Defined in Data.GADT.Show

Methods

greadsPrec :: Int -> GReadS ((:~:) a)

GShow ((:~:) a :: k -> Type)

Defined in Data.GADT.Show

Methods

gshowsPrec :: Int -> (a :~: a0) -> ShowS

GCompare ((:~:) a :: k -> Type)

Defined in Data.GADT.Compare

Methods

gcompare :: (a :~: a0) -> (a :~: b) -> GOrdering a0 b

GEq ((:~:) a :: k -> Type)

Defined in Data.GADT.Compare

Methods

geq :: (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b)

a ~ b => Bounded (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

minBound :: a :~: b

maxBound :: a :~: b

a ~ b => Enum (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

succ :: (a :~: b) -> a :~: b

pred :: (a :~: b) -> a :~: b

toEnum :: Int -> a :~: b

fromEnum :: (a :~: b) -> Int

enumFrom :: (a :~: b) -> [a :~: b]

enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b]

Eq (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

(==) :: (a :~: b) -> (a :~: b) -> Bool

(/=) :: (a :~: b) -> (a :~: b) -> Bool

Ord (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

compare :: (a :~: b) -> (a :~: b) -> Ordering

(<) :: (a :~: b) -> (a :~: b) -> Bool

(<=) :: (a :~: b) -> (a :~: b) -> Bool

(>) :: (a :~: b) -> (a :~: b) -> Bool

(>=) :: (a :~: b) -> (a :~: b) -> Bool

max :: (a :~: b) -> (a :~: b) -> a :~: b

min :: (a :~: b) -> (a :~: b) -> a :~: b

a ~ b => Read (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

readsPrec :: Int -> ReadS (a :~: b)

readList :: ReadS [a :~: b]

readPrec :: ReadPrec (a :~: b)

readListPrec :: ReadPrec [a :~: b]

Show (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

showsPrec :: Int -> (a :~: b) -> ShowS

show :: (a :~: b) -> String

showList :: [a :~: b] -> ShowS