some-1.0.5: Existential type: Some
Safe HaskellSafe
LanguageHaskell2010

Data.GADT.Compare

Synopsis

Equality

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.

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 TestEquality Tag instance is

>>> :{
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

instance GEq Tag where
   geq = testEquality

this will mean we probably want to have

instance Eq 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 GEq Tag instance would differentiate between different constructors:

>>> :{
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 geq (x :: f a) (y :: f b) may be 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)

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

Instances details
GEq (TypeRep :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Internal

Methods

geq :: forall (a :: k0) (b :: k0). TypeRep a -> TypeRep b -> Maybe (a :~: b) Source #

GEq ((:~:) a :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Internal

Methods

geq :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Source #

(GEq a, GEq b) => GEq (Product a b :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Internal

Methods

geq :: forall (a0 :: k0) (b0 :: k0). Product a b a0 -> Product a b b0 -> Maybe (a0 :~: b0) Source #

(GEq a, GEq b) => GEq (Sum a b :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Internal

Methods

geq :: forall (a0 :: k0) (b0 :: k0). Sum a b a0 -> Sum a b b0 -> Maybe (a0 :~: b0) Source #

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

Since: 1.0.4

Instance details

Defined in Data.GADT.Internal

Methods

geq :: forall (a0 :: k0) (b :: k0). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) Source #

(GEq a, GEq b) => GEq (a :*: b :: k -> Type) Source #

Since: 1.0.4

Instance details

Defined in Data.GADT.Internal

Methods

geq :: forall (a0 :: k0) (b0 :: k0). (a :*: b) a0 -> (a :*: b) b0 -> Maybe (a0 :~: b0) Source #

(GEq f, GEq g) => GEq (f :+: g :: k -> Type) Source #

Since: 1.0.4

Instance details

Defined in Data.GADT.Internal

Methods

geq :: forall (a :: k0) (b :: k0). (f :+: g) a -> (f :+: g) b -> Maybe (a :~: b) Source #

defaultGeq :: GCompare f => f a -> f b -> Maybe (a :~: b) Source #

If f has a GCompare instance, this function makes a suitable default implementation of geq.

Since: 1.0.4

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

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

Methods

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

Instances

Instances details
GCompare (TypeRep :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Internal

Methods

gcompare :: forall (a :: k0) (b :: k0). TypeRep a -> TypeRep b -> GOrdering a b Source #

GCompare ((:~:) a :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Internal

Methods

gcompare :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> GOrdering a0 b Source #

(GCompare a, GCompare b) => GCompare (Product a b :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Internal

Methods

gcompare :: forall (a0 :: k0) (b0 :: k0). Product a b a0 -> Product a b b0 -> GOrdering a0 b0 Source #

(GCompare a, GCompare b) => GCompare (Sum a b :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Internal

Methods

gcompare :: forall (a0 :: k0) (b0 :: k0). Sum a b a0 -> Sum a b b0 -> GOrdering a0 b0 Source #

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

Since: 1.0.4

Instance details

Defined in Data.GADT.Internal

Methods

gcompare :: forall (a0 :: k0) (b :: k0). (a :~~: a0) -> (a :~~: b) -> GOrdering a0 b Source #

(GCompare a, GCompare b) => GCompare (a :*: b :: k -> Type) Source #

Since: 1.0.4

Instance details

Defined in Data.GADT.Internal

Methods

gcompare :: forall (a0 :: k0) (b0 :: k0). (a :*: b) a0 -> (a :*: b) b0 -> GOrdering a0 b0 Source #

(GCompare f, GCompare g) => GCompare (f :+: g :: k -> Type) Source #

Since: 1.0.4

Instance details

Defined in Data.GADT.Internal

Methods

gcompare :: forall (a :: k0) (b :: k0). (f :+: g) a -> (f :+: g) b -> GOrdering a b Source #

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.

Constructors

GLT :: GOrdering a b 
GEQ :: GOrdering t t 
GGT :: GOrdering a b 

Instances

Instances details
GRead (GOrdering a :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Internal

GShow (GOrdering a :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Internal

Methods

gshowsPrec :: forall (a0 :: k0). Int -> GOrdering a a0 -> ShowS Source #

Show (GOrdering a b) Source # 
Instance details

Defined in Data.GADT.Internal

Methods

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

show :: GOrdering a b -> String #

showList :: [GOrdering a b] -> ShowS #

Eq (GOrdering a b) Source # 
Instance details

Defined in Data.GADT.Internal

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

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 #