Safe Haskell | Safe |
---|---|
Language | Haskell98 |
Data.GADT.Compare
Contents
Synopsis
- class GEq f => GCompare f where
- data GOrdering a b where
- 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) where
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
).
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.
Instances
GRead (GOrdering a :: k -> Type) Source # | |
Defined in Data.GADT.Compare Methods greadsPrec :: Int -> GReadS (GOrdering a) Source # | |
GShow (GOrdering a :: k -> Type) Source # | |
Defined in Data.GADT.Compare Methods gshowsPrec :: forall (a0 :: k0). Int -> GOrdering a a0 -> ShowS Source # | |
Show (f a) => ShowTag (GOrdering a :: k -> Type) (f :: k -> Type) Source # | |
Defined in Data.Dependent.Sum Methods showTaggedPrec :: forall (a0 :: k0). GOrdering a a0 -> Int -> f a0 -> ShowS Source # | |
Eq (GOrdering a b) Source # | |
Ord (GOrdering a b) Source # | |
Defined in Data.GADT.Compare | |
Show (GOrdering a b) 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)
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) where #
Instances
GRead ((:=) a :: k -> Type) Source # | |
Defined in Data.GADT.Compare Methods greadsPrec :: Int -> GReadS ((:=) a) Source # | |
GShow ((:=) a :: k -> Type) Source # | |
Defined in Data.GADT.Compare Methods gshowsPrec :: forall (a0 :: k0). Int -> (a := a0) -> ShowS Source # | |
GCompare ((:=) a :: k -> Type) Source # | |
GEq ((:=) a :: k -> Type) Source # | |
TestEquality ((:~:) a :: k -> Type) | |
Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) | |
Ord (f a) => OrdTag ((:=) a :: k -> Type) (f :: k -> Type) Source # | |
Defined in Data.Dependent.Sum Methods compareTagged :: forall (a0 :: k0). (a := a0) -> (a := a0) -> f a0 -> f a0 -> Ordering Source # | |
Eq (f a) => EqTag ((:=) a :: k -> Type) (f :: k -> Type) Source # | |
Read (f a) => ReadTag ((:=) a :: k -> Type) (f :: k -> Type) Source # | In order to make a
The 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 |
Defined in Data.Dependent.Sum Methods readTaggedPrec :: forall (a0 :: k0). (a := a0) -> Int -> ReadS (f a0) Source # | |
Show (f a) => ShowTag ((:=) a :: k -> Type) (f :: k -> Type) Source # | |
Defined in Data.Dependent.Sum Methods showTaggedPrec :: forall (a0 :: k0). (a := a0) -> Int -> f a0 -> ShowS Source # | |
a ~ b => Bounded (a :~: b) | |
Defined in Data.Type.Equality | |
a ~ b => Enum (a :~: b) | |
Defined in Data.Type.Equality | |
Eq (a :~: b) | |
Ord (a :~: b) | |
Defined in Data.Type.Equality | |
a ~ b => Read (a :~: b) | |
Defined in Data.Type.Equality | |
Show (a :~: b) | |