git.iko.soy/type-level-sets
on master help sign in
swap
e36892738 ahead, 0 behind
.gitignorenew file+1
since splitsnapshots
unifiedsplit
@@ -0,0 +1 @@
1+.stack-work
README+42−21
@@ -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
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, and split sets. Also included is a "mapping" type constructor that pairs symbols with types. This can be used to represent
2+subsets/submaps, and splitting sets/maps. This library was originally built based on
3−sets of variable-type pairs, which is used in the paper "Embedding effect systems in Haskell" (Dominic Orchard,
3+"Embedding effect systems in Haskell" (Dominic Orchard,
4Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf>) to embed effect sets.
4Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf>) to embed effect sets.
5
5
6The following shows an example:
6The following shows an example:
7
7
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:
9
32
10− import Data.Type.Set
33+ *Main> foobar
34+ {w :-> 6, x :-> 2, y :-> 3, z :-> True}
11
35
12− foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]
36+Thus, we see that values for 'w' are added.
13− foo = Ext ((Var :: (Var "x")) :-> 2) $
14− Ext ((Var :: (Var "z")) :-> 4) $
15− Ext ((Var :: (Var "w")) :-> 5) $
16− Empty
17
37
18− bar :: Set '["y" :-> Int, "w" :-> Int]
38+ import GHC.TypeLits
19− bar = Ext ((Var :: (Var "y")) :-> 3) $
39+ import Data.Type.Set
20− Ext ((Var :: (Var "w")) :-> 1) $
40+ type instance Cmp (Natural n) (Natural m) = CmpNat n m
21− Empty
22
41
23− -- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Int]
42+ data Natural (a :: Nat) where
24− foobar = foo `union` bar
43+ Z :: Natural 0
44+ S :: Natural n -> Natural (n + 1)
25
45
26−The 'Set' type for 'foobar' here shows the normalised form (sorted with no duplicates).
46+ -- foo :: Set '[Natural 0, Natural 1, Natural 3]
27−The type signatures is commented out as it can be infered. Running the example we get:
47+ foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))
28
48
29− *Main> foobar
49+ -- bar :: Set '[Natural 1, Natural 2]
30− {(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)}
50+ bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))
31
51
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
33
54
34
55
35
56
changelog.mdnew file+5
@@ -0,0 +1,5 @@
1+ # v0.8.9.0
2+
3+ - GHC 8.4 and 8.6 support.
4+ - Fixed bug in the delete operation.
5+ - Non-membership predicates
example.hs+26−13
@@ -1,18 +1,31 @@
1−{-# LANGUAGE DataKinds, TypeOperators #-}
1+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, MultiParamTypeClasses #-}
2
2
3+import GHC.TypeLits
3−import Data.Type.Set
4+import Data.Type.Map
4
5
5−foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]
6+-- Specify that key-value pairs on Ints combine to an Int
6−foo = Ext ((Var :: (Var "x")) :-> 2) $
7+type instance Combine Int Int = Int
7− Ext ((Var :: (Var "z")) :-> 4) $
8+-- Specify that Int values for matching keys should be added
8− Ext ((Var :: (Var "w")) :-> 5) $
9+instance Combinable Int Int where
9− Empty
10+ combine x y = x + y
10
11
12+foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int]
13+foo = Ext (Var :: (Var "x")) 2
14+ $ Ext (Var :: (Var "z")) True
15+ $ Ext (Var :: (Var "w")) 5
16+ $ Empty
17+
18+foo' :: Map (AsMap '["z" :-> Bool, "x" :-> Int, "w" :-> Int])
19+foo' = asMap foo
20+
11−bar :: Set '["y" :-> Int, "w" :-> Int]
21+bar :: Map '["y" :-> Int, "w" :-> Int]
12−bar = Ext ((Var :: (Var "y")) :-> 3) $
22+bar = Ext (Var :: (Var "y")) 3 $
13− Ext ((Var :: (Var "w")) :-> 1) $
23+ Ext (Var :: (Var "w")) 1 $
14− Empty
24+ Empty
15
25
16-- GHC can easily infer this type, so an explicit signature not necessary
26-- GHC can easily infer this type, so an explicit signature not necessary
17−-- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]
27+-- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]
18−foobar = foo `union` bar
28+foobar = foo `union` bar
29+
30+foobarToFoo :: Map '["w" :-> Int, "x" :-> Int, "z" :-> Bool]
31+foobarToFoo = submap foobar
example2.hsnew file+30
@@ -0,0 +1,30 @@
1+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, GADTs, StandaloneDeriving #-}
2+{-# LANGUAGE FlexibleContexts #-}
3+
4+import GHC.TypeLits
5+import Data.Type.Set
6+
7+type instance Cmp (Natural n) (Natural m) = CmpNat n m
8+
9+data Natural (a :: Nat) where
10+ Z :: Natural 0
11+ S :: Natural n -> Natural (n + 1)
12+
13+deriving instance Show (Natural n)
14+
15+-- foo :: Set '[Natural 0, Natural 1, Natural 3]
16+foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))
17+
18+-- bar :: Set '[Natural 1, Natural 2]
19+bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))
20+
21+-- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]
22+foobar = foo `union` bar
23+
24+nonMemberTest :: NonMember (Natural 0) as => Set as -> ()
25+nonMemberTest set = ()
26+
27+-- nonMemberTest meep is well typed
28+meep = asSet $ Ext (S Z) (Ext (S (S Z)) Empty)
29+-- nonMemberTest morp is ill typed
30+morp = asSet $ Ext (S Z) (Ext (S (S Z)) (Ext Z Empty))
src/Data/Type/Map.hsnew file+261
@@ -0,0 +1,261 @@
1+{- This module provides type-level finite maps.
2+The implementation is similar to that shown in the paper.
3+ "Embedding effect systems in Haskell" Orchard, Petricek 2014 -}
4+
5+{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, KindSignatures,
6+ TypeFamilies, UndecidableInstances, MultiParamTypeClasses,
7+ FlexibleInstances, GADTs, FlexibleContexts, ScopedTypeVariables,
8+ ConstraintKinds, IncoherentInstances #-}
9+
10+module Data.Type.Map (Mapping(..), Union, Unionable, union, Var(..), Map(..),
11+ Combine, Combinable(..), Cmp,
12+ Nubable, nub,
13+ Lookup, Member, (:\), Split, split,
14+ IsMember, lookp, Updatable, update,
15+ IsMap, AsMap, asMap,
16+ Submap, submap) where
17+
18+import GHC.TypeLits
19+import Data.Type.Bool
20+import Data.Type.Equality
21+import Data.Type.Set (Cmp, Proxy(..), Flag(..), Sort, Filter, (:++))
22+
23+{- Throughout, type variables
24+ 'k' ranges over "keys"
25+ 'v' ranges over "values"
26+ 'kvp' ranges over "key-value-pairs"
27+ 'm', 'n' range over "maps" -}
28+
29+-- Mappings
30+infixr 4 :->
31+{-| A key-value pair -}
32+data Mapping k v = k :-> v
33+
34+{-| Union of two finite maps -}
35+type Union m n = Nub (Sort (m :++ n))
36+
37+{-| Apply 'Combine' to values with matching key (removes duplicate keys) -}
38+type family Nub t where
39+ Nub '[] = '[]
40+ Nub '[kvp] = '[kvp]
41+ Nub ((k :-> v1) ': (k :-> v2) ': m) = Nub ((k :-> Combine v1 v2) ': m)
42+ Nub (kvp1 ': kvp2 ': s) = kvp1 ': Nub (kvp2 ': s)
43+
44+{-| Open type family for combining values in a map (that have the same key) -}
45+type family Combine (a :: v) (b :: v) :: v
46+
47+{-| Delete elements from a map by key -}
48+type family (m :: [Mapping k v]) :\ (c :: k) :: [Mapping k v] where
49+ '[] :\ k = '[]
50+ ((k :-> v) ': m) :\ k = m :\ k
51+ (kvp ': m) :\ k = kvp ': (m :\ k)
52+
53+{-| Type-level lookup of elements from a map -}
54+type family Lookup (m :: [Mapping k v]) (c :: k) :: Maybe v where
55+ Lookup '[] k = Nothing
56+ Lookup ((k :-> v) ': m) k = Just v
57+ Lookup (kvp ': m) k = Lookup m k
58+
59+{-| Membership test as type function -}
60+type family Member (c :: k) (m :: [Mapping k v]) :: Bool where
61+ Member k '[] = False
62+ Member k ((k :-> v) ': m) = True
63+ Member k (kvp ': m) = Member k m
64+
65+-----------------------------------------------------------------
66+-- Value-level map with a type-level representation
67+
68+{-| Pair a symbol (representing a variable) with a type -}
69+data Var (k :: Symbol) = Var
70+
71+instance KnownSymbol k => Show (Var k) where
72+ show = symbolVal
73+
74+{-| A value-level heterogenously-typed Map (with type-level representation in terms of lists) -}
75+data Map (n :: [Mapping Symbol *]) where
76+ Empty :: Map '[]
77+ Ext :: Var k -> v -> Map m -> Map ((k :-> v) ': m)
78+
79+{-| Membership test a type class (predicate) -}
80+class IsMember v t m where
81+ {-| Value-level lookup of elements from a map, via type class predicate -}
82+ lookp :: Var v -> Map m -> t
83+
84+instance {-# OVERLAPS #-} IsMember v t ((v ':-> t) ': m) where
85+ lookp _ (Ext _ x _) = x
86+
87+instance {-# OVERLAPPABLE #-} IsMember v t m => IsMember v t (x ': m) where
88+ lookp v (Ext _ _ m) = lookp v m
89+
90+
91+{-| Updatability as a type class -}
92+class Updatable v t m n where
93+ {-| Update a map with `m` at variable `v` with a value of type `t`
94+ to produce a map of type `n` -}
95+ update :: Map m -> Var v -> t -> Map n
96+
97+instance {-# OVERLAPS #-} Updatable v t ((v ':-> s) ': m) ((v ':-> t) ': m) where
98+ update (Ext v _ m) _ x = Ext v x m
99+
100+instance Updatable v t m n => Updatable v t ((w ':-> y) ': m) ((w ':-> y) ': n) where
101+ update (Ext w y m) v x = Ext w y (update m v x)
102+
103+-- instance Updatable v t '[] '[v ':-> t] where
104+-- update Empty v x = Ext v x Empty
105+
106+instance Updatable v t s ((v ':-> t) ': s) where
107+ update xs v x = Ext v x xs
108+
109+
110+{-| Predicate to check if in normalised map form -}
111+type IsMap s = (s ~ Nub (Sort s))
112+
113+{-| At the type level, normalise the list form to the map form -}
114+type AsMap s = Nub (Sort s)
115+
116+{-| At the value level, noramlise the list form to the map form -}
117+asMap :: (Sortable s, Nubable (Sort s)) => Map s -> Map (AsMap s)
118+asMap x = nub (quicksort x)
119+
120+instance Show (Map '[]) where
121+ show Empty = "{}"
122+
123+instance (KnownSymbol k, Show v, Show' (Map s)) => Show (Map ((k :-> v) ': s)) where
124+ show (Ext k v s) = "{" ++ show k ++ " :-> " ++ show v ++ show' s ++ "}"
125+
126+class Show' t where
127+ show' :: t -> String
128+instance Show' (Map '[]) where
129+ show' Empty = ""
130+instance (KnownSymbol k, Show v, Show' (Map s)) => Show' (Map ((k :-> v) ': s)) where
131+ show' (Ext k v s) = ", " ++ show k ++ " :-> " ++ show v ++ (show' s)
132+
133+instance Eq (Map '[]) where
134+ Empty == Empty = True
135+
136+instance (Eq v, Eq (Map s)) => Eq (Map ((k :-> v) ': s)) where
137+ (Ext Var v m) == (Ext Var v' m') = v == v' && m == m'
138+
139+instance Ord (Map '[]) where
140+ compare Empty Empty = EQ
141+
142+instance (Ord v, Ord (Map s)) => Ord (Map ((k :-> v) ': s)) where
143+ compare (Ext Var v m) (Ext Var v' m') = compare v v' `mappend` compare m m'
144+
145+{-| Union of two finite maps (normalising) -}
146+union :: (Unionable s t) => Map s -> Map t -> Map (Union s t)
147+union s t = nub (quicksort (append s t))
148+
149+type Unionable s t = (Nubable (Sort (s :++ t)), Sortable (s :++ t))
150+
151+{-| Append of two finite maps (non normalising) -}
152+append :: Map s -> Map t -> Map (s :++ t)
153+append Empty x = x
154+append (Ext k v xs) ys = Ext k v (append xs ys)
155+
156+type instance Cmp (k :: Symbol) (k' :: Symbol) = CmpSymbol k k'
157+type instance Cmp (k :-> v) (k' :-> v') = CmpSymbol k k'
158+
159+{-| Value-level quick sort that respects the type-level ordering -}
160+class Sortable xs where
161+ quicksort :: Map xs -> Map (Sort xs)
162+
163+instance Sortable '[] where
164+ quicksort Empty = Empty
165+
166+instance (Sortable (Filter FMin (k :-> v) xs)
167+ , Sortable (Filter FMax (k :-> v) xs)
168+ , FilterV FMin k v xs
169+ , FilterV FMax k v xs) => Sortable ((k :-> v) ': xs) where
170+ quicksort (Ext k v xs) =
171+ quicksort (less k v xs) `append` Ext k v Empty `append` quicksort (more k v xs)
172+ where
173+ less = filterV (Proxy::(Proxy FMin))
174+ more = filterV (Proxy::(Proxy FMax))
175+
176+{- Filter out the elements less-than or greater-than-or-equal to the pivot -}
177+class FilterV (f::Flag) k v xs where
178+ filterV :: Proxy f -> Var k -> v -> Map xs -> Map (Filter f (k :-> v) xs)
179+
180+instance FilterV f k v '[] where
181+ filterV _ k v Empty = Empty
182+
183+instance (Conder (Cmp x (k :-> v) == LT), FilterV FMin k v xs) => FilterV FMin k v (x ': xs) where
184+ filterV f@Proxy k v (Ext k' v' xs) =
185+ cond (Proxy::(Proxy (Cmp x (k :-> v) == LT)))
186+ (Ext k' v' (filterV f k v xs))
187+ (filterV f k v xs)
188+
189+instance
190+ (Conder ((Cmp x (k :-> v) == GT) || (Cmp x (k :-> v) == EQ)), FilterV FMax k v xs)
191+ => FilterV FMax k v (x ': xs) where
192+ filterV f@Proxy k v (Ext k' v' xs) =
193+ cond (Proxy::(Proxy ((Cmp x (k :-> v) == GT) || (Cmp x (k :-> v) == EQ))))
194+ (Ext k' v' (filterV f k v xs))
195+ (filterV f k v xs)
196+
197+class Combinable t t' where
198+ combine :: t -> t' -> Combine t t'
199+
200+class Nubable t where
201+ nub :: Map t -> Map (Nub t)
202+
203+instance Nubable '[] where
204+ nub Empty = Empty
205+
206+instance Nubable '[e] where
207+ nub (Ext k v Empty) = Ext k v Empty
208+
209+instance {-# OVERLAPPABLE #-}
210+ (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
211+ Nubable (f ': s)) => Nubable (e ': f ': s) where
212+ nub (Ext k v (Ext k' v' s)) = Ext k v (nub (Ext k' v' s))
213+
214+instance {-# OVERLAPS #-}
215+ (Combinable v v', Nubable ((k :-> Combine v v') ': s))
216+ => Nubable ((k :-> v) ': (k :-> v') ': s) where
217+ nub (Ext k v (Ext k' v' s)) = nub (Ext k (combine v v') s)
218+
219+
220+class Conder g where
221+ cond :: Proxy g -> Map s -> Map t -> Map (If g s t)
222+
223+instance Conder True where
224+ cond _ s t = s
225+
226+instance Conder False where
227+ cond _ s t = t
228+
229+
230+{-| Splitting a union of maps, given the maps we want to split it into -}
231+class Split s t st where
232+ -- where st ~ Union s t
233+ split :: Map st -> (Map s, Map t)
234+
235+instance Split '[] '[] '[] where
236+ split Empty = (Empty, Empty)
237+
238+instance {-# OVERLAPPABLE #-} Split s t st => Split (x ': s) (x ': t) (x ': st) where
239+ split (Ext k v st) = let (s, t) = split st
240+ in (Ext k v s, Ext k v t)
241+
242+instance {-# OVERLAPS #-} Split s t st => Split (x ': s) t (x ': st) where
243+ split (Ext k v st) = let (s, t) = split st
244+ in (Ext k v s, t)
245+
246+instance {-# OVERLAPS #-} (Split s t st) => Split s (x ': t) (x ': st) where
247+ split (Ext k v st) = let (s, t) = split st
248+ in (s, Ext k v t)
249+
250+{-| Construct a submap 's' from a supermap 't' -}
251+class Submap s t where
252+ submap :: Map t -> Map s
253+
254+instance Submap '[] '[] where
255+ submap xs = Empty
256+
257+instance {-# OVERLAPPABLE #-} Submap s t => Submap s (x ': t) where
258+ submap (Ext _ _ xs) = submap xs
259+
260+instance {-# OVERLAPS #-} Submap s t => Submap (x ': s) (x ': t) where
261+ submap (Ext k v xs) = Ext k v (submap xs)
src/Data/Type/Set.hs+86−64
@@ -1,27 +1,32 @@
1−{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,
1+{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,
2− MultiParamTypeClasses, FlexibleInstances, PolyKinds, FlexibleContexts,
2+ MultiParamTypeClasses, FlexibleInstances, PolyKinds,
3− UndecidableInstances, ConstraintKinds, OverlappingInstances, ScopedTypeVariables #-}
3+ FlexibleContexts, UndecidableInstances, ConstraintKinds,
4+ ScopedTypeVariables, TypeInType #-}
4
5
5−module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
6+module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
6− Sort, Sortable, Append(..), Split(..), Cmp,
7+ Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..),
7 Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
8 Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
8− (:->)(..), Var(..)) where
9+ Delete(..), Proxy(..), remove, Remove, (:\),
10+ Member(..), NonMember, MemberP(..)) where
9
11
10import GHC.TypeLits
12import GHC.TypeLits
11import Data.Type.Bool
13import Data.Type.Bool
12import Data.Type.Equality
14import Data.Type.Equality
13−import Data.Proxy
14
15
15−{-| Core Set definition, in terms of lists -}
16+data Proxy (p :: k) = Proxy
17+
18+-- Value-level 'Set' representation, essentially a list
16−data Set (n :: [*]) where
19+data Set (n :: [k]) where
20+ {--| Construct an empty set -}
17 Empty :: Set '[]
21 Empty :: Set '[]
22+ {--| Extend a set with an element -}
18 Ext :: e -> Set s -> Set (e ': s)
23 Ext :: e -> Set s -> Set (e ': s)
19
24
20instance Show (Set '[]) where
25instance Show (Set '[]) where
21 show Empty = "{}"
26 show Empty = "{}"
22
27
23instance (Show e, Show' (Set s)) => Show (Set (e ': s)) where
28instance (Show e, Show' (Set s)) => Show (Set (e ': s)) where
24− show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}"
29+ show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}"
25
30
26class Show' t where
31class Show' t where
27 show' :: t -> String
32 show' :: t -> String
@@ -30,6 +35,10 @@ instance Show' (Set '[]) where
30instance (Show' (Set s), Show e) => Show' (Set (e ': s)) where
35instance (Show' (Set s), Show e) => Show' (Set (e ': s)) where
31 show' (Ext e s) = ", " ++ show e ++ (show' s)
36 show' (Ext e s) = ", " ++ show e ++ (show' s)
32
37
38+instance (Eq e, Eq (Set s)) => Eq (Set (e ': s)) where
39+ (Ext e m) == (Ext e' m') = e == e' && m == m'
40+
41+
33{-| At the type level, normalise the list form to the set form -}
42{-| At the type level, normalise the list form to the set form -}
34type AsSet s = Nub (Sort s)
43type AsSet s = Nub (Sort s)
35
44
@@ -41,54 +50,68 @@ asSet x = nub (quicksort x)
41type IsSet s = (s ~ Nub (Sort s))
50type IsSet s = (s ~ Nub (Sort s))
42
51
43{-| Useful properties to be able to refer to someties -}
52{-| Useful properties to be able to refer to someties -}
44−type SetProperties f = (Union f '[] ~ f, Split f '[] f,
53+type SetProperties f = (Union f '[] ~ f, Split f '[] f,
45− Union '[] f ~ f, Split '[] f f,
54+ Union '[] f ~ f, Split '[] f f,
46 Union f f ~ f, Split f f f,
55 Union f f ~ f, Split f f f,
47 Unionable f '[], Unionable '[] f)
56 Unionable f '[], Unionable '[] f)
48
57
49{-- Union --}
58{-- Union --}
50
59
51{-| Union of sets -}
60{-| Union of sets -}
52−type Union s t = Nub (Sort (Append s t))
61+type Union s t = Nub (Sort (s :++ t))
53
62
54union :: (Unionable s t) => Set s -> Set t -> Set (Union s t)
63union :: (Unionable s t) => Set s -> Set t -> Set (Union s t)
55union s t = nub (quicksort (append s t))
64union s t = nub (quicksort (append s t))
56
65
57−type Unionable s t = (Sortable (Append s t), Nubable (Sort (Append s t)))
66+type Unionable s t = (Sortable (s :++ t), Nubable (Sort (s :++ t)))
58
67
59{-| List append (essentially set disjoint union) -}
68{-| List append (essentially set disjoint union) -}
60−type family Append (s :: [k]) (t :: [k]) :: [k] where
69+type family (:++) (x :: [k]) (y :: [k]) :: [k] where
61− Append '[] t = t
70+ '[] :++ xs = xs
62− Append (x ': xs) ys = x ': (Append xs ys)
71+ (x ': xs) :++ ys = x ': (xs :++ ys)
63
72
64−append :: Set s -> Set t -> Set (Append s t)
73+append :: Set s -> Set t -> Set (s :++ t)
65append Empty x = x
74append Empty x = x
66append (Ext e xs) ys = Ext e (append xs ys)
75append (Ext e xs) ys = Ext e (append xs ys)
67
76
68−{-| Useful alias for append -}
77+{-| Delete elements from a set -}
69−type (s :: [k]) :++ (t :: [k]) = Append s t
78+type family (m :: [k]) :\ (x :: k) :: [k] where
79+ '[] :\ x = '[]
80+ (x ': xs) :\ x = xs :\ x
81+ (y ': xs) :\ x = y ': (xs :\ x)
82+
83+class Remove s t where
84+ remove :: Set s -> Proxy t -> Set (s :\ t)
85+
86+instance Remove '[] t where
87+ remove Empty Proxy = Empty
88+
89+instance {-# OVERLAPS #-} Remove xs x => Remove (x ': xs) x where
90+ remove (Ext _ xs) x@Proxy = remove xs x
91+
92+instance {-# OVERLAPPABLE #-} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
93+ => Remove (y ': xs) x where
94+ remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
70
95
71{-| Splitting a union a set, given the sets we want to split it into -}
96{-| Splitting a union a set, given the sets we want to split it into -}
72class Split s t st where
97class Split s t st where
73 -- where st ~ Union s t
98 -- where st ~ Union s t
74− split :: Set st -> (Set s, Set t)
99+ split :: Set st -> (Set s, Set t)
75
100
76instance Split '[] '[] '[] where
101instance Split '[] '[] '[] where
77 split Empty = (Empty, Empty)
102 split Empty = (Empty, Empty)
78
103
79−instance Split s t st => Split (x ': s) (x ': t) (x ': st) where
104+instance {-# OVERLAPPABLE #-} Split s t st => Split (x ': s) (x ': t) (x ': st) where
80 split (Ext x st) = let (s, t) = split st
105 split (Ext x st) = let (s, t) = split st
81 in (Ext x s, Ext x t)
106 in (Ext x s, Ext x t)
82
107
83−instance Split s t st => Split (x ': s) t (x ': st) where
108+instance {-# OVERLAPS #-} Split s t st => Split (x ': s) t (x ': st) where
84 split (Ext x st) = let (s, t) = split st
109 split (Ext x st) = let (s, t) = split st
85− in (Ext x s, t)
110+ in (Ext x s, t)
86
111
87−instance (Split s t st) => Split s (x ': t) (x ': st) where
112+instance {-# OVERLAPS #-} (Split s t st) => Split s (x ': t) (x ': st) where
88 split (Ext x st) = let (s, t) = split st
113 split (Ext x st) = let (s, t) = split st
89− in (s, Ext x t)
114+ in (s, Ext x t)
90−
91−
92
115
93{-| Remove duplicates from a sorted list -}
116{-| Remove duplicates from a sorted list -}
94type family Nub t where
117type family Nub t where
@@ -98,7 +121,7 @@ type family Nub t where
98 Nub (e ': f ': s) = e ': Nub (f ': s)
121 Nub (e ': f ': s) = e ': Nub (f ': s)
99
122
100{-| Value-level counterpart to the type-level 'Nub'
123{-| Value-level counterpart to the type-level 'Nub'
101− Note: the value-level case for equal types is not define here,
124+ Note: the value-level case for equal types is not define here,
102 but should be given per-application, e.g., custom 'merging' behaviour may be required -}
125 but should be given per-application, e.g., custom 'merging' behaviour may be required -}
103
126
104class Nubable t where
127class Nubable t where
@@ -113,7 +136,7 @@ instance Nubable '[e] where
113instance Nubable (e ': s) => Nubable (e ': e ': s) where
136instance Nubable (e ': s) => Nubable (e ': e ': s) where
114 nub (Ext _ (Ext e s)) = nub (Ext e s)
137 nub (Ext _ (Ext e s)) = nub (Ext e s)
115
138
116−instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
139+instance {-# OVERLAPS #-} (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
117 Nubable (f ': s)) => Nubable (e ': f ': s) where
140 Nubable (f ': s)) => Nubable (e ': f ': s) where
118 nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))
141 nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))
119
142
@@ -122,13 +145,13 @@ instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
122class Subset s t where
145class Subset s t where
123 subset :: Set t -> Set s
146 subset :: Set t -> Set s
124
147
125−instance Subset '[] '[] where
148+instance Subset '[] '[] where
126 subset xs = Empty
149 subset xs = Empty
127
150
128−instance Subset s t => Subset s (x ': t) where
151+instance {-# OVERLAPPABLE #-} Subset s t => Subset s (x ': t) where
129 subset (Ext _ xs) = subset xs
152 subset (Ext _ xs) = subset xs
130
153
131−instance Subset s t => Subset (x ': s) (x ': t) where
154+instance {-# OVERLAPS #-} Subset s t => Subset (x ': s) (x ': t) where
132 subset (Ext x xs) = Ext x (subset xs)
155 subset (Ext x xs) = Ext x (subset xs)
133
156
134
157
@@ -141,8 +164,17 @@ data Flag = FMin | FMax
141
164
142type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where
165type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where
143 Filter f p '[] = '[]
166 Filter f p '[] = '[]
144− Filter FMin p (x ': xs) = If (Cmp x p == LT) (x ': (Filter FMin p xs)) (Filter FMin p xs)
167+ Filter FMin p (x ': xs) = If (Cmp x p == LT) (x ': (Filter FMin p xs)) (Filter FMin p xs)
145− Filter FMax p (x ': xs) = If (Cmp x p == GT || Cmp x p == EQ) (x ': (Filter FMax p xs)) (Filter FMax p xs)
168+ Filter FMax p (x ': xs) = If (Cmp x p == GT || Cmp x p == EQ) (x ': (Filter FMax p xs)) (Filter FMax p xs)
169+
170+type family DeleteFromList (e :: elem) (list :: [elem]) where
171+ DeleteFromList elem '[] = '[]
172+ DeleteFromList elem (x ': xs) = If (Cmp elem x == EQ)
173+ xs
174+ (x ': DeleteFromList elem xs)
175+
176+type family Delete elem set where
177+ Delete elem (Set xs) = Set (DeleteFromList elem xs)
146
178
147{-| Value-level quick sort that respects the type-level ordering -}
179{-| Value-level quick sort that respects the type-level ordering -}
148class Sortable xs where
180class Sortable xs where
@@ -166,11 +198,11 @@ instance FilterV f p '[] where
166
198
167instance (Conder ((Cmp x p) == LT), FilterV FMin p xs) => FilterV FMin p (x ': xs) where
199instance (Conder ((Cmp x p) == LT), FilterV FMin p xs) => FilterV FMin p (x ': xs) where
168 filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy ((Cmp x p) == LT)))
200 filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy ((Cmp x p) == LT)))
169− (Ext x (filterV f p xs)) (filterV f p xs)
201+ (Ext x (filterV f p xs)) (filterV f p xs)
170
202
171instance (Conder (((Cmp x p) == GT) || ((Cmp x p) == EQ)), FilterV FMax p xs) => FilterV FMax p (x ': xs) where
203instance (Conder (((Cmp x p) == GT) || ((Cmp x p) == EQ)), FilterV FMax p xs) => FilterV FMax p (x ': xs) where
172 filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy (((Cmp x p) == GT) || ((Cmp x p) == EQ))))
204 filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy (((Cmp x p) == GT) || ((Cmp x p) == EQ))))
173− (Ext x (filterV f p xs)) (filterV f p xs)
205+ (Ext x (filterV f p xs)) (filterV f p xs)
174
206
175class Conder g where
207class Conder g where
176 cond :: Proxy g -> Set s -> Set t -> Set (If g s t)
208 cond :: Proxy g -> Set s -> Set t -> Set (If g s t)
@@ -185,30 +217,20 @@ instance Conder False where
185
217
186type family Cmp (a :: k) (b :: k) :: Ordering
218type family Cmp (a :: k) (b :: k) :: Ordering
187
219
188−{-| Pair a symbol (representing a variable) with a type -}
220+{-| Membership of an element in a set, with an acommanying
189−infixl 2 :->
221+ value-level function that returns a bool -}
190−data (k :: Symbol) :-> (v :: *) = (Var k) :-> v
222+class Member a s where
191−
223+ member :: Proxy a -> Set s -> Bool
192−data Var (k :: Symbol) where Var :: Var k
224+
193− {- Some special defaults for some common names -}
225+instance {-# OVERLAPS #-} Member a (a ': s) where
194− X :: Var "x"
226+ member _ (Ext x _) = True
195− Y :: Var "y"
227+
196− Z :: Var "z"
228+instance {-# OVERLAPPABLE #-} Member a s => Member a (b ': s) where
197−
229+ member a (Ext _ xs) = member a xs
198−
230+
199−instance (Show (Var k), Show v) => Show (k :-> v) where
231+type family MemberP a s :: Bool where
200− show (k :-> v) = "(" ++ show k ++ " :-> " ++ show v ++ ")"
232+ MemberP a '[] = False
201−instance Show (Var "x") where
233+ MemberP a (a ': s) = True
202− show X = "x"
234+ MemberP a (b ': s) = MemberP a s
203− show Var = "Var"
235+
204−instance Show (Var "y") where
236+type NonMember a s = MemberP a s ~ False
205− show Y = "y"
206− show Var = "Var"
207−instance Show (Var "z") where
208− show Z = "z"
209− show Var = "Var"
210−instance Show (Var v) where
211− show _ = "Var"
212−
213−{-| Symbol comparison -}
214−type instance Cmp (v :-> a) (u :-> b) = CmpSymbol v u
stack.yamlnew file+29
@@ -0,0 +1,29 @@
1+# For more information, see: https://github.com/commercialhaskell/stack/wiki/stack.yaml
2+
3+# Specifies the GHC version and set of packages available (e.g., lts-3.5, nightly-2015-09-21, ghc-7.10.2)
4+resolver: lts-12.7
5+
6+# Local packages, usually specified by relative directory name
7+packages:
8+- '.'
9+
10+# Packages to be pulled from upstream that are not in the resolver (e.g., acme-missiles-0.3)
11+extra-deps: []
12+
13+# Override default flag values for local packages and extra-deps
14+flags: {}
15+
16+# Control whether we use the GHC we find on the path
17+# system-ghc: true
18+
19+# Require a specific version of stack, using version ranges
20+# require-stack-version: -any # Default
21+# require-stack-version: >= 0.1.4.0
22+
23+# Override the architecture used by stack, especially useful on Windows
24+# arch: i386
25+# arch: x86_64
26+
27+# Extra directories used by stack for building
28+# extra-include-dirs: [/path/to/dir]
29+# extra-lib-dirs: [/path/to/dir]
type-level-sets.cabal+59−30
@@ -1,50 +1,77 @@
1name: type-level-sets
1name: type-level-sets
2−version: 0.5
2+version: 0.8.9.0
3−synopsis: Type-level sets (with value-level counterparts and various operations)
3+synopsis: Type-level sets and finite maps (with value-level counterparts)
4−description:
4+description:
5− This package provides type-level sets (no duplicates, sorted to provide a nomral form) via 'Set',
5+ This package provides type-level sets (no duplicates, sorted to provide a normal form) via 'Set' and type-level
6− with value-level counterparts. Described in the paper \"Embedding effect systems in Haskell\" by Dominic Orchard
6+ finite maps via 'Map', with value-level counterparts.
7− and Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf> (Haskell Symposium, 2014)
8 .
7 .
8+ Described in the paper \"Embedding effect systems in Haskell\" by Dominic Orchard
9+ 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.
10+ .
9− Here is a brief example:
11+ Here is a brief example for finite maps:
10 .
12 .
11 >
13 >
12− > import Data.Type.Set
14+ > import Data.Type.Map
15+ >
16+ > -- Specify how to combine duplicate key-value pairs for Int values
17+ > type instance Combine Int Int = Int
18+ > instance Combinable Int Int where
19+ > combine x y = x + y
20+ >
21+ > foo :: Map '["x" :-> Int, "z" :-> Bool, "w" :-> Int]
22+ > foo = Ext (Var :: (Var "x")) 2
23+ > $ Ext (Var :: (Var "z")) True
24+ > $ Ext (Var :: (Var "w")) 5
25+ > $ Empty
13 >
26 >
14− > foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]
15− > foo = Ext ((Var :: (Var "x")) :-> 2) $
16− > Ext ((Var :: (Var "z")) :-> 4) $
17− > Ext ((Var :: (Var "w")) :-> 5) $
18− > Empty
19− >
20− > bar :: Set '["y" :-> Int, "w" :-> Int]
27+ > bar :: Map '["y" :-> Int, "w" :-> Int]
21− > bar = Ext ((Var :: (Var "y")) :-> 3) $
28+ > bar = Ext (Var :: (Var "y")) 3
22− > Ext ((Var :: (Var "w")) :-> 1) $
29+ > $ Ext (Var :: (Var "w")) 1
23− > Empty
30+ > $ Empty
24− >
31+ >
25− > -- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Int]
32+ > -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool]
26 > foobar = foo `union` bar
33 > foobar = foo `union` bar
27 .
34 .
28− The 'Set' type for 'foobar' here shows the normalised form (sorted with no duplicates).
35+ The 'Map' type for 'foobar' here shows the normalised form (sorted with no duplicates).
29 The type signatures is commented out as it can be infered. Running the example we get:
36 The type signatures is commented out as it can be infered. Running the example we get:
30 .
37 .
31− > >>> foobar
38+ > >>> foobar
32− > [(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)]
39+ > {w :-> 6, x :-> 2, y :-> 3, z :-> True}
40+ .
41+ Thus, we see that the values for \"w\" are added together.
42+ For sets, here is an example:
43+ .
44+ > import GHC.TypeLits
45+ > import Data.Type.Set
46+ > type instance Cmp (Natural n) (Natural m) = CmpNat n m
47+ >
48+ > data Natural (a :: Nat) where
49+ > Z :: Natural 0
50+ > S :: Natural n -> Natural (n + 1)
51+ >
52+ > -- foo :: Set '[Natural 0, Natural 1, Natural 3]
53+ > foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))
54+ >
55+ > -- bar :: Set '[Natural 1, Natural 2]
56+ > bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))
57+ >
58+ > -- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]
59+ > foobar = foo `union` bar
33 .
60 .
34− Thus, we see that the first value paired with the \"w\" variable is dropped.
61+ Note the types here are all inferred.
35 .
62 .
36license: BSD3
63license: BSD3
37license-file: LICENSE
64license-file: LICENSE
38category: Type System, Data Structures
65category: Type System, Data Structures
39−copyright: 2013-14 University of Cambridge
66+copyright: 2013-18 University of Kent
40author: Dominic Orchard
67author: Dominic Orchard
41maintainer: Dominic Orchard
68maintainer: Dominic Orchard
42stability: experimental
69stability: experimental
43build-type: Simple
70build-type: Simple
44cabal-version: >= 1.6
71cabal-version: >= 1.6
45−tested-with: GHC == 7.8.2
72+tested-with: GHC >= 8.2.2
46
73
47−extra-source-files: example.hs
74+extra-source-files: example.hs, example2.hs, changelog.md
48
75
49
76
50source-repository head
77source-repository head
@@ -53,9 +80,11 @@ source-repository head
53
80
54library
81library
55 hs-source-dirs: src
82 hs-source-dirs: src
83+ other-extensions: TypeInType
56
84
57
85
58 exposed-modules: Data.Type.Set
86 exposed-modules: Data.Type.Set
59−
87+ Data.Type.Map
88+
60− build-depends: base >= 4.7.0.0 && < 5,
89+ build-depends: base < 5,
61− ghc-prim
90+ ghc-prim