Documentation

A basic dependent sum type; 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

Then, we have the following valid expressions of type DSum Tag:

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

And we can write functions that consume DSum Tag values by matching, such as:

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

By analogy to the (key => value) construction for dictionary entries in many dynamic languages, we use (key :=> value) as the constructor for dependent sums. The :=> operator has very low precedence and binds to the right, so if the Tag GADT is extended with an additional constructor Rec :: Tag (DSum Tag), then Rec :=> AnInt :=> 3 + 4 is parsed as would be expected (Rec :=> (AnInt :=> (3 + 4))) and has type DSum Tag. Its precedence is just above that of $, so foo bar $ AString :=> eep is equivalent to foo bar (AString :=> eep).

In order to make a Show instance for DSum tag, tag must be able to show itself as well as any value of the tagged type. GShow together with this class provides the interface by which it can do so.

GShow tag => t is conceptually equivalent to something like this imaginary syntax: (forall a. Inhabited (tag a) => Show a) => t, where Inhabited is an imaginary predicate that characterizes non-empty types, and a does not occur free in t.

The Tag example type introduced in the DSum section could be given the following instances:

 instance GShow Tag where
     gshowsPrec _showsValPrec _p AString = showString "AString"
     gshowsPrec _showsValPrec _p AnInt   = showString "AnInt"
 instance ShowTag Tag where
     showTaggedPrec AString = showsPrec
     showTaggedPrec AnInt   = showsPrec

In order to test DSum tag for equality, tag must know how to test both itself and its tagged values for equality. EqTag defines the interface by which they are expected to do so.

Continuing the Tag example from the DSum section, we can define:

 instance GEq Tag where
     geq AString AString = Just Refl
     geq AString AnInt   = Nothing
     geq AnInt   AString = Nothing
     geq AnInt   AnInt   = Just Refl
 instance EqTag Tag where
     eqTagged AString AString = (==)
     eqTagged AnInt   AnInt   = (==)

Note that eqTagged is not called until after the tags have been compared, so it only needs to consider the cases where gcompare returns GEQ.

In order to compare DSum tag values, tag must know how to compare both itself and its tagged values. OrdTag defines the interface by which they are expected to do so.

Continuing the Tag example from the EqTag section, we can define:

 instance GCompare Tag where
     gcompare AString AString = GEQ
     gcompare AString AnInt   = GLT
     gcompare AnInt   AString = GGT
     gcompare AnInt   AnInt   = GEQ
 instance OrdTag Tag where
     compareTagged AString AString = compare
     compareTagged AnInt   AnInt   = compare

As with eqTagged, compareTagged only needs to consider cases where gcompare returns GEQ.