Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Equality
A class for type-contexts which contain enough information to (at least in some cases) decide the equality of types occurring within them.
This class is sometimes confused with TestEquality
from base.
TestEquality
only checks type equality.
Consider
>>>
data Tag a where TagInt1 :: Tag Int; TagInt2 :: Tag Int
The correct
instance isTestEquality
Tag
>>>
:{
instance TestEquality Tag where testEquality TagInt1 TagInt1 = Just Refl testEquality TagInt1 TagInt2 = Just Refl testEquality TagInt2 TagInt1 = Just Refl testEquality TagInt2 TagInt2 = Just Refl :}
While we can define
instanceGEq
Tag wheregeq
=testEquality
this will mean we probably want to have
instanceEq
Tag where _==
_ = True
Note: In the future version of some
package (to be released around GHC-9.6 / 9.8) the
forall a. Eq (f a)
constraint will be added as a constraint to GEq
,
with a law relating GEq
and Eq
:
geq
x y = Just Refl ⇒ x == y = True ∀ (x :: f a) (y :: f b) x == y ≡ isJust (geq
x y) ∀ (x, y :: f a)
So, the more useful
instance would differentiate between
different constructors:GEq
Tag
>>>
:{
instance GEq Tag where geq TagInt1 TagInt1 = Just Refl geq TagInt1 TagInt2 = Nothing geq TagInt2 TagInt1 = Nothing geq TagInt2 TagInt2 = Just Refl :}
which is consistent with a derived Eq
instance for Tag
>>>
deriving instance Eq (Tag a)
Note that even if a ~ b
, the
may
be geq
(x :: f a) (y :: f b)Nothing
(when value terms are inequal).
The consistency of GEq
and Eq
is easy to check by exhaustion:
>>>
let checkFwdGEq :: (forall a. Eq (f a), GEq f) => f a -> f b -> Bool; checkFwdGEq x y = case geq x y of Just Refl -> x == y; Nothing -> True
>>>
(checkFwdGEq TagInt1 TagInt1, checkFwdGEq TagInt1 TagInt2, checkFwdGEq TagInt2 TagInt1, checkFwdGEq TagInt2 TagInt2)
(True,True,True,True)
>>>
let checkBwdGEq :: (Eq (f a), GEq f) => f a -> f a -> Bool; checkBwdGEq x y = if x == y then isJust (geq x y) else isNothing (geq x y)
>>>
(checkBwdGEq TagInt1 TagInt1, checkBwdGEq TagInt1 TagInt2, checkBwdGEq TagInt2 TagInt1, checkBwdGEq TagInt2 TagInt2)
(True,True,True,True)
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 SNat Source # | |
GEq SChar Source # | |
GEq SSymbol Source # | |
GEq (TypeRep :: k -> Type) Source # | |
GEq ((:~:) a :: k -> Type) Source # | |
(GEq a, GEq b) => GEq (Product a b :: k -> Type) Source # | |
(GEq a, GEq b) => GEq (Sum a b :: k -> Type) Source # | |
GEq ((:~~:) a :: k -> Type) Source # | Since: 1.0.4 |
(GEq a, GEq b) => GEq (a :*: b :: k -> Type) Source # | Since: 1.0.4 |
(GEq f, GEq g) => GEq (f :+: g :: k -> Type) Source # | Since: 1.0.4 |
defaultNeq :: GEq f => f a -> f b -> Bool Source #
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
).
Instances
GCompare SNat Source # | |
GCompare SChar Source # | |
GCompare SSymbol Source # | |
GCompare (TypeRep :: k -> Type) Source # | |
GCompare ((:~:) a :: k -> Type) Source # | |
(GCompare a, GCompare b) => GCompare (Product a b :: k -> Type) Source # | |
(GCompare a, GCompare b) => GCompare (Sum a b :: k -> Type) Source # | |
GCompare ((:~~:) a :: k -> Type) Source # | Since: 1.0.4 |
(GCompare a, GCompare b) => GCompare (a :*: b :: k -> Type) Source # | Since: 1.0.4 |
(GCompare f, GCompare g) => GCompare (f :+: g :: k -> Type) Source # | Since: 1.0.4 |
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.
Instances
GRead (GOrdering a :: k -> Type) Source # | |
Defined in Data.GADT.Internal | |
GShow (GOrdering a :: k -> Type) Source # | |
Defined in Data.GADT.Internal | |
Show (GOrdering a b) Source # | |
Eq (GOrdering a b) Source # | |
Ord (GOrdering a b) Source # | |
Defined in Data.GADT.Internal 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 # |