Data.Dependent.Sum

Documentation

data DSum tag f

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 Applicative f => DSum Tag f:

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

And 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

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 :=> and ==> operators have very low precedence and bind to the right, so if the Tag GADT is extended with an additional constructor Rec :: Tag (DSum Tag Identity), then Rec ==> AnInt ==> 3 + 4 is parsed as would be expected (Rec ==> (AnInt ==> (3 + 4))) and has type DSum Identity Tag. Its precedence is just above that of $, so foo bar $ AString ==> "eep" is equivalent to foo bar (AString ==> "eep").

Constructors

!(tag a) :=> (f a) infixr 1

Instances

(GEq tag, Has' Eq tag f) => Eq (DSum tag f)

Defined in Data.Dependent.Sum

Methods

(==) :: DSum tag f -> DSum tag f -> Bool

(/=) :: DSum tag f -> DSum tag f -> Bool

(GCompare tag, Has' Eq tag f, Has' Ord tag f) => Ord (DSum tag f)

Defined in Data.Dependent.Sum

Methods

compare :: DSum tag f -> DSum tag f -> Ordering

(<) :: DSum tag f -> DSum tag f -> Bool

(<=) :: DSum tag f -> DSum tag f -> Bool

(>) :: DSum tag f -> DSum tag f -> Bool

(>=) :: DSum tag f -> DSum tag f -> Bool

max :: DSum tag f -> DSum tag f -> DSum tag f

min :: DSum tag f -> DSum tag f -> DSum tag f

(GRead tag, Has' Read tag f) => Read (DSum tag f)

Defined in Data.Dependent.Sum

Methods

readsPrec :: Int -> ReadS (DSum tag f)

readList :: ReadS [DSum tag f]

readPrec :: ReadPrec (DSum tag f)

readListPrec :: ReadPrec [DSum tag f]

(GShow tag, Has' Show tag f) => Show (DSum tag f)

Defined in Data.Dependent.Sum

Methods

showsPrec :: Int -> DSum tag f -> ShowS

show :: DSum tag f -> String

showList :: [DSum tag f] -> ShowS

(==>) :: Applicative f => tag a -> a -> DSum tag f infixr 1

type ShowTag tag f = (GShow tag, Has' Show tag f)

Deprecated: Instead of 'ShowTag tag f', use '(GShow tag, Has' Show tag f)'

showTaggedPrec :: forall tag f a. (GShow tag, Has' Show tag f) => tag a -> Int -> f a -> ShowS

type ReadTag tag f = (GRead tag, Has' Read tag f)

Deprecated: Instead of 'ReadTag tag f', use '(GRead tag, Has' Read tag f)'

readTaggedPrec :: forall tag f a. (GRead tag, Has' Read tag f) => tag a -> Int -> ReadS (f a)

type EqTag tag f = (GEq tag, Has' Eq tag f)

Deprecated: Instead of 'EqTag tag f', use '(GEq tag, Has' Eq tag f)'

eqTaggedPrec :: forall tag f a. (GEq tag, Has' Eq tag f) => tag a -> tag a -> f a -> f a -> Bool

eqTagged :: forall tag f a. EqTag tag f => tag a -> tag a -> f a -> f a -> Bool

type OrdTag tag f = (GCompare tag, Has' Eq tag f, Has' Ord tag f)

Deprecated: Instead of 'OrdTag tag f', use '(GCompare tag, Has' Eq tag f, Has' Ord tag f)'

compareTaggedPrec :: forall tag f a. (GCompare tag, Has' Eq tag f, Has' Ord tag f) => tag a -> tag a -> f a -> f a -> Ordering

compareTagged :: forall tag f a. OrdTag tag f => tag a -> tag a -> f a -> f a -> Ordering