Universe

If f has a GEq instance, this function makes a suitable default implementation of (==).

A basic dependent sum type where the first component is a tag that specifies the type of the second. For example, think of a GADT such as:

data Tag a where
   AString :: Tag String
   AnInt   :: Tag Int
   Rec     :: Tag (DSum Tag Identity)

Then we can write expressions where the RHS of (:=>) has different types depending on the Tag constructor used. Here are some expressions of type DSum Tag Identity:

AString :=> Identity "hello!"
AnInt   :=> Identity 42

Often, the f we choose has an Applicative instance, and we can use the helper function (==>). The following expressions all have the type Applicative f => DSum Tag f:

AString ==> "hello!"
AnInt   ==> 42

We can write functions that consume DSum Tag f values by matching, such as:

toString :: DSum Tag Identity -> String
toString (AString :=> Identity str) = str
toString (AnInt   :=> Identity int) = show int
toString (Rec     :=> Identity sum) = toString sum

The (:=>) constructor and (==>) helper are chosen to resemble the (key => value) construction for dictionary entries in many dynamic languages. The :=> and ==> operators have very low precedence and bind to the right, making repeated use of these operators behave as you'd expect:

-- Parses as: Rec ==> (AnInt ==> (3 + 4))
-- Has type: Applicative f => DSum Tag f
Rec ==> AnInt ==> 3 + 4

The precedence of these operators is just above that of $, so foo bar $ AString ==> "eep" is equivalent to foo bar (AString ==> "eep").

To use the Eq, Ord, Read, and Show instances for DSum tag f, you will need an ArgDict instance for your tag type. Use deriveArgDict from the constraints-extras package to generate this instance.

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.

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)

Show-like class for 1-type-parameter GADTs. GShow t => ... is equivalent to something like (forall a. Show (t a)) => .... The easiest way to create instances would probably be to write (or derive) an instance Show (T a), and then simply say:

instance GShow t where gshowsPrec = defaultGshowsPrec

Existential. This is type is useful to hide GADTs' parameters.

>>> data Tag :: Type -> Type where TagInt :: Tag Int; TagBool :: Tag Bool>>> instance GShow Tag where gshowsPrec _ TagInt = showString "TagInt"; gshowsPrec _ TagBool = showString "TagBool">>> classify s = case s of "TagInt" -> [mkGReadResult TagInt]; "TagBool" -> [mkGReadResult TagBool]; _ -> []>>> instance GRead Tag where greadsPrec _ s = [ (r, rest) | (con, rest) <-  lex s, r <- classify con ]

You can either use PatternSynonyms (available with GHC >= 8.0)

>>> let x = Some TagInt>>> xSome TagInt

>>> case x of { Some TagInt -> "I"; Some TagBool -> "B" } :: String"I"

or you can use functions

>>> let y = mkSome TagBool>>> ySome TagBool

>>> withSome y $ \y' -> case y' of { TagInt -> "I"; TagBool -> "B" } :: String"B"

The implementation of mapSome is safe.

>>> let f :: Tag a -> Tag a; f TagInt = TagInt; f TagBool = TagBool>>> mapSome f ySome TagBool

but you can also use:

>>> withSome y (mkSome . f)Some TagBool

>>> read "Some TagBool" :: Some TagSome TagBool

>>> read "mkSome TagInt" :: Some TagSome TagInt