-
Notifications
You must be signed in to change notification settings - Fork 22
/
type-level-sets.cabal
108 lines (100 loc) · 3.29 KB
/
type-level-sets.cabal
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
name: type-level-sets
version: 0.9.0.0
synopsis: Type-level sets and finite maps (with value-level counterparts)
description:
This package provides type-level sets (no duplicates, sorted to provide a normal form) via 'Set' and type-level
finite maps via 'Map', with value-level counterparts.
.
Described in the paper \"Embedding effect systems in Haskell\" by Dominic Orchard
and Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf> (Haskell Symposium, 2014). This version now uses Quicksort to normalise the representation.
.
Here is a brief example for finite maps:
.
>
> import Data.Type.Map
>
> -- Specify how to combine duplicate key-value pairs for Int values
> type instance Combine Int Int = Int
> instance Combinable Int Int where
> combine x y = x + y
>
> foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int]
> foo = Ext (Var :: (Var "x")) 2
> $ Ext (Var :: (Var "z")) True
> $ Ext (Var :: (Var "w")) 5
> $ Empty
>
> bar :: Map '["y" :-> Int, "w" :-> Int]
> bar = Ext (Var :: (Var "y")) 3
> $ Ext (Var :: (Var "w")) 1
> $ Empty
>
> -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool]
> foobar = foo `union` bar
.
The 'Map' type for 'foobar' here shows the normalised form (sorted with no duplicates).
The type signatures is commented out as it can be infered. Running the example we get:
.
> >>> foobar
> {w :-> 6, x :-> 2, y :-> 3, z :-> True}
.
Thus, we see that the values for \"w\" are added together.
For sets, here is an example:
.
> import GHC.TypeLits
> import Data.Type.Set
> type instance Cmp (Natural n) (Natural m) = CmpNat n m
>
> data Natural (a :: Nat) where
> Z :: Natural 0
> S :: Natural n -> Natural (n + 1)
>
> -- foo :: Set '[Natural 0, Natural 1, Natural 3]
> foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))
>
> -- bar :: Set '[Natural 1, Natural 2]
> bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))
>
> -- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]
> foobar = foo `union` bar
.
Note the types here are all inferred.
.
license: BSD3
license-file: LICENSE
category: Type System, Data Structures
copyright: 2013-18 University of Kent
author: Dominic Orchard
maintainer: Dominic Orchard
stability: experimental
build-type: Simple
cabal-version: >= 1.10
tested-with: GHC >= 8.2.2
extra-source-files: changelog.md
source-repository head
type: git
location: https://github.com/dorchard/type-level-sets
library
hs-source-dirs: src
other-extensions: TypeInType
exposed-modules: Data.Type.Set
Data.Type.Map
build-depends: base < 5,
ghc-prim
test-suite tests
type: exitcode-stdio-1.0
main-is: Spec.hs
hs-source-dirs: examples, tests/hspec
other-modules:
ExampleSet
ExampleSet2
ExampleMap
MapSpec
SetSpec
build-tool-depends:
hspec-discover:hspec-discover >=2.7 && <2.10
build-depends:
type-level-sets
, hspec
, base
default-language: Haskell2010