dependent-sum-0.7.2.0: Dependent sum type

Safe Haskell | Safe
Language | Haskell2010

Data.Dependent.Sum

Synopsis

- data DSum (tag :: k -> Type) (f :: k -> Type) = !(tag a) :=> (f a)
- (==>) :: forall (f :: Type -> Type) tag a. Applicative f => tag a -> a -> DSum tag f
- type ShowTag (tag :: k' -> Type) (f :: k' -> Type) = (GShow tag, Has' Show tag f)
- showTaggedPrec :: forall {k'} tag f (a :: k'). (GShow tag, Has' Show tag f) => tag a -> Int -> f a -> ShowS
- type ReadTag (tag :: k' -> Type) (f :: k' -> Type) = (GRead tag, Has' Read tag f)
- readTaggedPrec :: forall {k'} tag f (a :: k'). (GRead tag, Has' Read tag f) => tag a -> Int -> ReadS (f a)
- type EqTag (tag :: k' -> Type) (f :: k' -> Type) = (GEq tag, Has' Eq tag f)
- eqTaggedPrec :: forall {k'} tag f (a :: k'). (GEq tag, Has' Eq tag f) => tag a -> tag a -> f a -> f a -> Bool
- eqTagged :: forall {k'} tag f (a :: k'). EqTag tag f => tag a -> tag a -> f a -> f a -> Bool
- type OrdTag (tag :: k' -> Type) (f :: k' -> Type) = (GCompare tag, Has' Eq tag f, Has' Ord tag f)
- compareTaggedPrec :: forall {k'} tag f (a :: k'). (GCompare tag, Has' Eq tag f, Has' Ord tag f) => tag a -> tag a -> f a -> f a -> Ordering
- compareTagged :: forall {k'} tag f (a :: k'). OrdTag tag f => tag a -> tag a -> f a -> f a -> Ordering

# Documentation

data DSum (tag :: k -> Type) (f :: k -> Type) Source #

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.

Constructors

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

#### Instances

Instances details

(GRead tag, Has' Read tag f) => Read (DSum tag f) Source # |
Instance details Defined in Data.Dependent.Sum Methods readsPrec :: Int -> ReadS (DSum tag f) Source # readList :: ReadS [DSum tag f] Source # readPrec :: ReadPrec (DSum tag f) Source # readListPrec :: ReadPrec [DSum tag f] Source #
(GShow tag, Has' Show tag f) => Show (DSum tag f) Source # |
Instance details Defined in Data.Dependent.Sum Methods showsPrec :: Int -> DSum tag f -> ShowS Source # show :: DSum tag f -> String Source # showList :: [DSum tag f] -> ShowS Source #
(GEq tag, Has' Eq tag f) => Eq (DSum tag f) Source # |
Instance details Defined in Data.Dependent.Sum Methods (==) :: DSum tag f -> DSum tag f -> Bool Source # (/=) :: DSum tag f -> DSum tag f -> Bool Source #
(GCompare tag, Has' Eq tag f, Has' Ord tag f) => Ord (DSum tag f) Source # |

Instance details

Defined in Data.Dependent.Sum

Methods

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

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

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

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

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

max :: DSum tag f -> DSum tag f -> DSum tag f Source #

min :: DSum tag f -> DSum tag f -> DSum tag f Source #

(==>) :: forall (f :: Type -> Type) tag a. Applicative f => tag a -> a -> DSum tag f infixr 1 Source #

Convenience helper. Uses `pure` to lift `a` into `f a`.

type ShowTag (tag :: k' -> Type) (f :: k' -> Type) = (GShow tag, Has' Show tag f) Source #

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

showTaggedPrec :: forall {k'} tag f (a :: k'). (GShow tag, Has' Show tag f) => tag a -> Int -> f a -> ShowS Source #

type ReadTag (tag :: k' -> Type) (f :: k' -> Type) = (GRead tag, Has' Read tag f) Source #

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

readTaggedPrec :: forall {k'} tag f (a :: k'). (GRead tag, Has' Read tag f) => tag a -> Int -> ReadS (f a) Source #

type EqTag (tag :: k' -> Type) (f :: k' -> Type) = (GEq tag, Has' Eq tag f) Source #

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

eqTaggedPrec :: forall {k'} tag f (a :: k'). (GEq tag, Has' Eq tag f) => tag a -> tag a -> f a -> f a -> Bool Source #

eqTagged :: forall {k'} tag f (a :: k'). EqTag tag f => tag a -> tag a -> f a -> f a -> Bool Source #

type OrdTag (tag :: k' -> Type) (f :: k' -> Type) = (GCompare tag, Has' Eq tag f, Has' Ord tag f) Source #

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

compareTaggedPrec :: forall {k'} tag f (a :: k'). (GCompare tag, Has' Eq tag f, Has' Ord tag f) => tag a -> tag a -> f a -> f a -> Ordering Source #

compareTagged :: forall {k'} tag f (a :: k'). OrdTag tag f => tag a -> tag a -> f a -> f a -> Ordering Source #