@@ -1,35 +1,56 @@
1−This library provides type-level sets to Haskell, with a value level counterpart, and operations for taking the union, computing
2−subsets, and split sets. Also included is a "mapping" type constructor that pairs symbols with types. This can be used to represent
3−sets of variable-type pairs, which is used in the paper "Embedding effect systems in Haskell" (Dominic Orchard,
1+This library provides type-level sets and finite maps to Haskell, with a value level counterpart, and operations for taking the union, computing
2+subsets/submaps, and splitting sets/maps. This library was originally built based on
3+"Embedding effect systems in Haskell" (Dominic Orchard,
44Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf>) to embed effect sets.
55
66The following shows an example:
77
8− {-# LANGUAGE DataKinds, TypeOperators #-}
8+ {-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, MultiParamTypeClasses #-}
9+ import Data.Type.Map
10+
11+ -- Specifies how to combine duplicate key-value pairs for Int values
12+ type instance Combine Int Int = Int
13+ instance Combinable Int Int where
14+ combine x y = x + y
15+
16+ foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int]
17+ foo = Ext (Var :: (Var "x")) 2
18+ $ Ext (Var :: (Var "z")) True
19+ $ Ext (Var :: (Var "w")) 5
20+ Empty
21+
22+ bar :: Map '["y" :-> Int, "w" :-> Int]
23+ bar = Ext (Var :: (Var "y")) 3
24+ $ Ext (Var :: (Var "w")) 1
25+ $ Empty
26+
27+ -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool]
28+ foobar = foo `union` bar
29+
30+The 'Map' type for 'foobar' here shows the normalised form (sorted with no duplicates).
31+The type signatures is commented out as it can be infered. Running the example we get:
932
10− import Data.Type.Set
33+ *Main> foobar
34+ {w :-> 6, x :-> 2, y :-> 3, z :-> True}
1135
12− foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]
13− foo = Ext ((Var :: (Var "x")) :-> 2) $
14− Ext ((Var :: (Var "z")) :-> 4) $
15− Ext ((Var :: (Var "w")) :-> 5) $
16− Empty
36+Thus, we see that values for 'w' are added.
1737
18− bar :: Set '["y" :-> Int, "w" :-> Int]
19− bar = Ext ((Var :: (Var "y")) :-> 3) $
20− Ext ((Var :: (Var "w")) :-> 1) $
21− Empty
38+ import GHC.TypeLits
39+ import Data.Type.Set
40+ type instance Cmp (Natural n) (Natural m) = CmpNat n m
2241
23− -- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Int]
24− foobar = foo `union` bar
42+ data Natural (a :: Nat) where
43+ Z :: Natural 0
44+ S :: Natural n -> Natural (n + 1)
2545
26−The 'Set' type for 'foobar' here shows the normalised form (sorted with no duplicates).
27−The type signatures is commented out as it can be infered. Running the example we get:
46+ -- foo :: Set '[Natural 0, Natural 1, Natural 3]
47+ foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))
2848
29− *Main> foobar
30− {(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)}
49+ -- bar :: Set '[Natural 1, Natural 2]
50+ bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))
3151
32−Thus, we see that the first value paired with the "w" variable is dropped.
52+ -- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]
53+ foobar = foo `union` bar
3354
3455
3556