| Safe Haskell | Safe |
|---|---|
| Language | Haskell98 |
Data.GADT.Compare
Contents
- type (:=) = (:~:)
- class GEq f where
- defaultEq :: GEq f => f a -> f b -> Bool
- defaultNeq :: GEq f => f a -> f b -> Bool
- data GOrdering a b where
- weakenOrdering :: GOrdering a b -> Ordering
- class GEq f => GCompare f where
- defaultCompare :: GCompare f => f a -> f b -> Ordering
- data (k :~: a) b :: forall k. k -> k -> * where
Documentation
Backwards compatibility alias; as of GHC 7.8, this is the same as `(:~:)`.
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
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 xOr 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 '(/=)'.
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.
weakenOrdering :: GOrdering a b -> Ordering Source #
TODO: Think of a better name
This operation forgets the phantom types of a GOrdering value.
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
defaultCompare :: GCompare f => f a -> f b -> Ordering Source #
data (k :~: a) b :: 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: 4.7.0.0
Instances
| TestEquality k ((:~:) k a) | |
| GCompare k ((:=) k a) Source # | |
| GEq k ((:=) k a) Source # | |
| Ord (f a) => OrdTag k ((:=) k a) f Source # | |
| Eq (f a) => EqTag k ((:=) k a) f Source # | |
| Read (f a) => ReadTag k ((:=) k a) f 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 |
| Show (f a) => ShowTag k ((:=) k a) f Source # | |
| (~) k a b => Bounded ((:~:) k a b) | |
| (~) k a b => Enum ((:~:) k a b) | |
| Eq ((:~:) k a b) | |
| Ord ((:~:) k a b) | |
| (~) k a b => Read ((:~:) k a b) | |
| Show ((:~:) k a b) | |