Safe Haskell	Safe
Language	Haskell98

Data.Dependent.Sum

Synopsis

data DSum tag f = !(tag a) :=> (f a)
(==>) :: Applicative f => tag a -> a -> DSum tag f
class GShow tag => ShowTag tag f where
- showTaggedPrec :: tag a -> Int -> f a -> ShowS
class GRead tag => ReadTag tag f where
- readTaggedPrec :: tag a -> Int -> ReadS (f a)
class GEq tag => EqTag tag f where
- eqTagged :: tag a -> tag a -> f a -> f a -> Bool
class (EqTag tag f, GCompare tag) => OrdTag tag f where
- compareTagged :: tag a -> tag a -> f a -> f a -> Ordering

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

EqTag tag f => Eq (DSum tag f) #
Instance details Defined in Data.Dependent.Sum Methods (==) :: DSum tag f -> DSum tag f -> Bool # (/=) :: DSum tag f -> DSum tag f -> Bool #
OrdTag tag f => Ord (DSum tag f) #
Instance details 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 #
ReadTag tag f => Read (DSum tag f) #
Instance details 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] #
ShowTag tag f => Show (DSum tag f) #
Instance details 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 #

class GShow tag => ShowTag tag f where #

In order to make a Show instance for DSum tag f, 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.

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

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

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

Methods

showTaggedPrec :: tag a -> Int -> f a -> ShowS #

Given a value of type tag a, return the showsPrec function for the type f a.

Instances

Show (f a) => ShowTag (GOrdering a :: k -> Type) (f :: k -> Type) #
Instance details Defined in Data.Dependent.Sum Methods showTaggedPrec :: GOrdering a a0 -> Int -> f a0 -> ShowS #
Show (f a) => ShowTag ((:=) a :: k -> Type) (f :: k -> Type) #
Instance details Defined in Data.Dependent.Sum Methods showTaggedPrec :: (a := a0) -> Int -> f a0 -> ShowS #

class GRead tag => ReadTag tag f where #

Methods

readTaggedPrec :: tag a -> Int -> ReadS (f a) #

Instances

Read (f a) => ReadTag ((:=) a :: k -> Type) (f :: k -> Type) #

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

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

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

instance GRead Tag where
    greadsPrec _p str = case tag of
       "AString"   -> [(\k -> k AString, rest)]
       "AnInt"     -> [(\k -> k AnInt,   rest)]
       _           -> []
       where (tag, rest) = break isSpace str
instance ReadTag Tag [] where
    readTaggedPrec AString = readsPrec
    readTaggedPrec AnInt   = readsPrec

Instance details

Defined in Data.Dependent.Sum

Methods

readTaggedPrec :: (a := a0) -> Int -> ReadS (f a0) #

class GEq tag => EqTag tag f where #

In order to test DSum tag f 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 AnInt   AnInt   = Just Refl
    geq _       _       = Nothing
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.

Methods

eqTagged :: tag a -> tag a -> f a -> f a -> Bool #

Given two values of type tag a (for which gcompare returns GEQ), return the == function for the type f a.

Instances

Eq (f a) => EqTag ((:=) a :: k -> Type) (f :: k -> Type) #
Instance details Defined in Data.Dependent.Sum Methods eqTagged :: (a := a0) -> (a := a0) -> f a0 -> f a0 -> Bool #

class (EqTag tag f, GCompare tag) => OrdTag tag f where #

In order to compare DSum tag f 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.

Methods

compareTagged :: tag a -> tag a -> f a -> f a -> Ordering #

Given two values of type tag a (for which gcompare returns GEQ), return the compare function for the type f a.

Instances

Ord (f a) => OrdTag ((:=) a :: k -> Type) (f :: k -> Type) #
Instance details Defined in Data.Dependent.Sum Methods compareTagged :: (a := a0) -> (a := a0) -> f a0 -> f a0 -> Ordering #