dependent-sum alternatives and similar packages
Based on the "dependent" category.
Alternatively, view dependent-sum alternatives based on common mentions on social networks and blogs.
9.4 0.0 dependent-sum VS dependent-mapDependently-typed finite maps (partial dependent products)
Do you think we are missing an alternative of dependent-sum or a related project?
This library defines a dependent sum type:
data DSum tag f = forall a. !(tag a) :=> f a
By analogy to the
key => value construction for dictionary entries in many dynamic languages, we use
:=> as the constructor for dependent sums. The key is a tag that specifies the type of the value; for example, think of a GADT such as:
data Tag a where StringKey :: Tag String IntKey :: Tag Int
Then, we have the following valid expressions of type
DSum Tag :
StringKey :=> ["hello!"] IntKey :=> 
And we can write functions that consume
DSum Tag values by matching, such as:
toString :: DSum Tag  -> [String] toString (StringKey :=> strs) = strs toString (IntKey :=> ints) = show ints
==> 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
foo bar $ AString ==> "eep" is equivalent to
foo bar (AString ==> "eep").
In order to support basic type classes from the
DSum, there are also several type classes defined for "tag" types:
GEq tagis similar to an
tag aexcept that with
geq, values of types
tag bmay be compared, and in the case of equality, evidence that the types
bare equal is provided.
GCompare tagis similar to the above for
Ord, and provides
gcompare, giving a
GOrderingthat gives similar evidence of type equality when values match.
GShow tagmeans that
tag ahas (the equivalent of) a
GRead tagmeans that
tag ahas (the equivalent of) a
In order to be able to compare values of type
DSum tag f for equality, in addition to having a
GEq tag instance, we need to know that, given a value
t :: tag a, we may obtain an instance
Eq (f a), which is expressed by the use of the
Has' Eq tag f constraint from the constraints-extras package, so we have the following instances:
(GEq tag, Has' Eq tag f) => Eq (DSum tag f) (GCompare tag, Has' Eq tag f, Has' Ord tag f) => Ord (DSum tag f) (GShow tag, Has' Show tag f) => Show (DSum tag f) (GRead tag, Has' Read tag f) => Read (DSum tag f)
In order to satisfy the
Has' constraints, you'll want to use
deriveArgDict from constraints-extras, or less-commonly, write your own instance of the ArgDict class by hand, in addition to making sure that it's actually the case that for every value of your tag type, there will be a corresponding instance of Eq/Ord/Read/Show as appropriate.
For example implementations of these classes, see the generated Haddock docs or the code in the
examples directory. There is a fair amount of boilerplate. A few of the more common classes (
GShow) can be automatically derived by Template Haskell code in the