dependent-sum-0.6: Dependent sum type

Safe HaskellSafe
LanguageHaskell98

Data.Dependent.Sum

Synopsis

Documentation

data DSum tag f Source #

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) Source # 
Instance details

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) Source # 
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 #

(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) #

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) Source # 
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 Source #

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

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 Source #

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

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) Source #

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

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 Source #

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

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

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