Safe Haskell	Safe
Language	Haskell98

Data.GADT.Compare

Contents

Orphan instances

Synopsis

class GEq f => GCompare f where
data GOrdering a b where
- GLT :: GOrdering a b
- GEQ :: GOrdering t t
- GGT :: GOrdering a b
class GEq f where
type (:=) = (:~:)
defaultEq :: GEq f => f a -> f b -> Bool
defaultNeq :: GEq f => f a -> f b -> Bool
weakenOrdering :: GOrdering a b -> Ordering
defaultCompare :: GCompare f => f a -> f b -> Ordering
data (a :: k) :~: (b :: k) :: forall k. k -> k -> * where
- Refl :: a :~: a

Documentation

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

Minimal complete definition

gcompare

Methods

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

Instances

GCompare (TypeRep :: k -> *) Source #
Instance details Defined in Data.GADT.Compare Methods gcompare :: TypeRep a -> TypeRep b -> GOrdering a b Source #
GCompare ((:=) a :: k -> *) Source #
Instance details Defined in Data.GADT.Compare Methods gcompare :: (a := a0) -> (a := b) -> GOrdering a0 b 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

GRead (GOrdering a :: k -> *) Source #
Instance details Defined in Data.GADT.Compare Methods greadsPrec :: Int -> GReadS (GOrdering a) Source #
GShow (GOrdering a :: k -> *) Source #
Instance details Defined in Data.GADT.Compare Methods gshowsPrec :: Int -> GOrdering a a0 -> ShowS Source #
Show (f a) => ShowTag (GOrdering a :: k -> ) (f :: k -> ) Source #
Instance details Defined in Data.Dependent.Sum Methods showTaggedPrec :: GOrdering a a0 -> Int -> f a0 -> ShowS Source #
Eq (GOrdering a b) Source #
Instance details Defined in Data.GADT.Compare Methods (==) :: GOrdering a b -> GOrdering a b -> Bool # (/=) :: GOrdering a b -> GOrdering a b -> Bool #
Ord (GOrdering a b) Source #
Instance details 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) Source #
Instance details 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 Source #

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

Minimal complete definition

geq

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

GEq (TypeRep :: k -> *) Source #
Instance details Defined in Data.GADT.Compare Methods geq :: TypeRep a -> TypeRep b -> Maybe (a := b) Source #
GEq ((:=) a :: k -> *) Source #
Instance details Defined in Data.GADT.Compare Methods geq :: (a := a0) -> (a := b) -> Maybe (a0 := b) Source #

type (:=) = (:~:) Source #

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

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

weakenOrdering :: GOrdering a b -> Ordering Source #

TODO: Think of a better name

This operation forgets the phantom types of a GOrdering value.

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

data (a :: k) :~: (b :: k) :: forall k. k -> k -> * 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 :: a :~: a

Instances

TestEquality ((:~:) a :: k -> *)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods testEquality :: (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #
GRead ((:=) a :: k -> *) Source #
Instance details Defined in Data.GADT.Compare Methods greadsPrec :: Int -> GReadS ((:=) a) Source #
GShow ((:=) a :: k -> *) Source #
Instance details Defined in Data.GADT.Compare Methods gshowsPrec :: Int -> (a := a0) -> ShowS Source #
GCompare ((:=) a :: k -> *) Source #
Instance details Defined in Data.GADT.Compare Methods gcompare :: (a := a0) -> (a := b) -> GOrdering a0 b Source #
GEq ((:=) a :: k -> *) Source #
Instance details Defined in Data.GADT.Compare Methods geq :: (a := a0) -> (a := b) -> Maybe (a0 := b) Source #
Ord (f a) => OrdTag ((:=) a :: k -> ) (f :: k -> ) Source #
Instance details Defined in Data.Dependent.Sum Methods compareTagged :: (a := a0) -> (a := a0) -> f a0 -> f a0 -> Ordering Source #
Eq (f a) => EqTag ((:=) a :: k -> ) (f :: k -> ) Source #
Instance details Defined in Data.Dependent.Sum Methods eqTagged :: (a := a0) -> (a := a0) -> f a0 -> f a0 -> Bool Source #
Read (f a) => ReadTag ((:=) a :: k -> ) (f :: k -> ) Source #	In order to make a `Read` instance for `DSum tag f`, `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 f => t` is conceptually equivalent to something like this imaginary syntax: `(forall a. Inhabited (tag a) => Read (f a)) => t`, where `Inhabited` is an imaginary predicate that characterizes non-empty types, and `f` and `a` do not occur free in `t`. The `Tag` example type introduced in the `DSum` section could be given the following instances, among others: 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
Instance details Defined in Data.Dependent.Sum Methods readTaggedPrec :: (a := a0) -> Int -> ReadS (f a0) Source #
Show (f a) => ShowTag ((:=) a :: k -> ) (f :: k -> ) Source #
Instance details Defined in Data.Dependent.Sum Methods showTaggedPrec :: (a := a0) -> Int -> f a0 -> ShowS Source #
a ~ b => Bounded (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods minBound :: a :~: b # maxBound :: a :~: b #
a ~ b => Enum (a :~: b)	Since: base-4.7.0.0
Instance details 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)
Instance details Defined in Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool # (/=) :: (a :~: b) -> (a :~: b) -> Bool #
Ord (a :~: b)
Instance details 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
Instance details 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)
Instance details Defined in Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS # show :: (a :~: b) -> String # showList :: [a :~: b] -> ShowS #

Orphan instances

GRead ((:=) a :: k -> *) Source #
Instance details Methods greadsPrec :: Int -> GReadS ((:=) a) Source #
GShow ((:=) a :: k -> *) Source #
Instance details Methods gshowsPrec :: Int -> (a := a0) -> ShowS Source #