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.