mirror of
https://github.com/obsidiansystems/dependent-sum.git
synced 2024-09-11 07:45:28 +03:00
Syntax highlighting in README
This commit is contained in:
parent
e515ad2c5f
commit
657cb78c2e
36
README.md
36
README.md
@ -3,24 +3,32 @@ dependent-sum [![Build Status](https://travis-ci.org/obsidiansystems/dependent-s
|
||||
|
||||
This library defines a dependent sum type:
|
||||
|
||||
data DSum tag f = forall a. !(tag a) :=> f a
|
||||
```haskell
|
||||
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
|
||||
```haskell
|
||||
data Tag a where
|
||||
StringKey :: Tag String
|
||||
IntKey :: Tag Int
|
||||
```
|
||||
|
||||
Then, we have the following valid expressions of type `DSum Tag []`:
|
||||
|
||||
StringKey :=> ["hello!"]
|
||||
IntKey :=> [42]
|
||||
```haskell
|
||||
StringKey :=> ["hello!"]
|
||||
IntKey :=> [42]
|
||||
```
|
||||
|
||||
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
|
||||
```haskell
|
||||
toString :: DSum Tag [] -> [String]
|
||||
toString (StringKey :=> strs) = strs
|
||||
toString (IntKey :=> ints) = show ints
|
||||
```
|
||||
|
||||
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")`.
|
||||
|
||||
@ -33,10 +41,12 @@ In order to support basic type classes from the `Prelude` for `DSum`, there are
|
||||
|
||||
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)
|
||||
```haskell
|
||||
(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.
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user