git.iko.soy/type-level-sets
on master help sign in
swap
e36892747 ahead, 0 behind
.gitignorenew file+1
since splitsnapshots
unifiedsplit
@@ -0,0 +1 @@
1+.stack-work
README+44−24
@@ -1,36 +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
6−Here is some example code!
6+The following shows an example:
7
7
8−<code>
9− {-# 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
10
15
11− import Data.Type.Set
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
12
21
13− -- foo :: Set '["x" :-> Integer, "z" :-> Integer]
22+ bar :: Map '["y" :-> Int, "w" :-> Int]
14− foo = Ext ((Var :: (Var "x")) :-> 2) $
23+ bar = Ext (Var :: (Var "y")) 3
15− Ext ((Var :: (Var "z")) :-> 4) $
24+ $ Ext (Var :: (Var "w")) 1
16− Empty
25+ $ Empty
17
26
18− -- bar :: Set '["y" :-> Integer, "w" :-> Integer]
27+ -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool]
19− bar = Ext ((Var :: (Var "y")) :-> 3) $
28+ foobar = foo `union` bar
20− Ext ((Var :: (Var "w")) :-> 1) $
21− Empty
22
29
23− -- foobar :: Set '["w" :-> Integer, "x" :-> Integer, "y" :-> Integer, "z" :-> Integer]
30+The 'Map' type for 'foobar' here shows the normalised form (sorted with no duplicates).
24− foobar = foo `union` bar
31+The type signatures is commented out as it can be infered. Running the example we get:
25−</code>
26
32
27−Note, the type signatures are commented out here as they can be inferred.
28−Example execution:
29−
30−<code>
31 *Main> foobar
33 *Main> foobar
32− {(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)}
34+ {w :-> 6, x :-> 2, y :-> 3, z :-> True}
33−</code>
35+
36+Thus, we see that values for 'w' are added.
37+
38+ import GHC.TypeLits
39+ import Data.Type.Set
40+ type instance Cmp (Natural n) (Natural m) = CmpNat n m
41+
42+ data Natural (a :: Nat) where
43+ Z :: Natural 0
44+ S :: Natural n -> Natural (n + 1)
45+
46+ -- foo :: Set '[Natural 0, Natural 1, Natural 3]
47+ foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))
48+
49+ -- bar :: Set '[Natural 1, Natural 2]
50+ bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))
51+
52+ -- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]
53+ foobar = foo `union` bar
34
54
35
55
36
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.hsnew file+31
@@ -0,0 +1,31 @@
1+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, MultiParamTypeClasses #-}
2+
3+import GHC.TypeLits
4+import Data.Type.Map
5+
6+-- Specify that key-value pairs on Ints combine to an Int
7+type instance Combine Int Int = Int
8+-- Specify that Int values for matching keys should be added
9+instance Combinable Int Int where
10+ combine x y = x + y
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+
21+bar :: Map '["y" :-> Int, "w" :-> Int]
22+bar = Ext (Var :: (Var "y")) 3 $
23+ Ext (Var :: (Var "w")) 1 $
24+ Empty
25+
26+-- GHC can easily infer this type, so an explicit signature not necessary
27+-- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]
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+90−66
@@ -1,28 +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− AllowAmbiguousTypes #-}
4+ ScopedTypeVariables, TypeInType #-}
5
5
6−module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
6+module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
7− Sort, Sortable, Append(..), Split(..), Cmp,
7+ Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..),
8 Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
8 Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
9− (:->)(..), Var(..)) where
9+ Delete(..), Proxy(..), remove, Remove, (:\),
10+ Member(..), NonMember, MemberP(..)) where
10
11
11import GHC.TypeLits
12import GHC.TypeLits
12import Data.Type.Bool
13import Data.Type.Bool
13import Data.Type.Equality
14import Data.Type.Equality
14−import Data.Proxy
15
15
16−{-| Core Set definition, in terms of lists -}
16+data Proxy (p :: k) = Proxy
17+
18+-- Value-level 'Set' representation, essentially a list
17−data Set (n :: [*]) where
19+data Set (n :: [k]) where
20+ {--| Construct an empty set -}
18 Empty :: Set '[]
21 Empty :: Set '[]
22+ {--| Extend a set with an element -}
19 Ext :: e -> Set s -> Set (e ': s)
23 Ext :: e -> Set s -> Set (e ': s)
20
24
21instance Show (Set '[]) where
25instance Show (Set '[]) where
22 show Empty = "{}"
26 show Empty = "{}"
23
27
24instance (Show e, Show' (Set s)) => Show (Set (e ': s)) where
28instance (Show e, Show' (Set s)) => Show (Set (e ': s)) where
25− show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}"
29+ show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}"
26
30
27class Show' t where
31class Show' t where
28 show' :: t -> String
32 show' :: t -> String
@@ -31,6 +35,10 @@ instance Show' (Set '[]) where
31instance (Show' (Set s), Show e) => Show' (Set (e ': s)) where
35instance (Show' (Set s), Show e) => Show' (Set (e ': s)) where
32 show' (Ext e s) = ", " ++ show e ++ (show' s)
36 show' (Ext e s) = ", " ++ show e ++ (show' s)
33
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+
34{-| 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 -}
35type AsSet s = Nub (Sort s)
43type AsSet s = Nub (Sort s)
36
44
@@ -42,54 +50,68 @@ asSet x = nub (quicksort x)
42type IsSet s = (s ~ Nub (Sort s))
50type IsSet s = (s ~ Nub (Sort s))
43
51
44{-| Useful properties to be able to refer to someties -}
52{-| Useful properties to be able to refer to someties -}
45−type SetProperties f = (Union f '[] ~ f, Split f '[] f,
53+type SetProperties f = (Union f '[] ~ f, Split f '[] f,
46− Union '[] f ~ f, Split '[] f f,
54+ Union '[] f ~ f, Split '[] f f,
47 Union f f ~ f, Split f f f,
55 Union f f ~ f, Split f f f,
48 Unionable f '[], Unionable '[] f)
56 Unionable f '[], Unionable '[] f)
49
57
50{-- Union --}
58{-- Union --}
51
59
52{-| Union of sets -}
60{-| Union of sets -}
53−type Union s t = Nub (Sort (Append s t))
61+type Union s t = Nub (Sort (s :++ t))
54
62
55union :: (Unionable s t) => Set s -> Set t -> Set (Union s t)
63union :: (Unionable s t) => Set s -> Set t -> Set (Union s t)
56union s t = nub (quicksort (append s t))
64union s t = nub (quicksort (append s t))
57
65
58−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)))
59
67
60{-| List append (essentially set disjoint union) -}
68{-| List append (essentially set disjoint union) -}
61−type family Append (s :: [k]) (t :: [k]) :: [k] where
69+type family (:++) (x :: [k]) (y :: [k]) :: [k] where
62− Append '[] t = t
70+ '[] :++ xs = xs
63− Append (x ': xs) ys = x ': (Append xs ys)
71+ (x ': xs) :++ ys = x ': (xs :++ ys)
64
72
65−append :: Set s -> Set t -> Set (Append s t)
73+append :: Set s -> Set t -> Set (s :++ t)
66append Empty x = x
74append Empty x = x
67append (Ext e xs) ys = Ext e (append xs ys)
75append (Ext e xs) ys = Ext e (append xs ys)
68
76
69−{-| Useful alias for append -}
77+{-| Delete elements from a set -}
70−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)
71
95
72{-| 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 -}
73class Split s t st where
97class Split s t st where
74 -- where st ~ Union s t
98 -- where st ~ Union s t
75− split :: Set st -> (Set s, Set t)
99+ split :: Set st -> (Set s, Set t)
76
100
77instance Split '[] '[] '[] where
101instance Split '[] '[] '[] where
78 split Empty = (Empty, Empty)
102 split Empty = (Empty, Empty)
79
103
80−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
81 split (Ext x st) = let (s, t) = split st
105 split (Ext x st) = let (s, t) = split st
82 in (Ext x s, Ext x t)
106 in (Ext x s, Ext x t)
83
107
84−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
85 split (Ext x st) = let (s, t) = split st
109 split (Ext x st) = let (s, t) = split st
86− in (Ext x s, t)
110+ in (Ext x s, t)
87
111
88−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
89 split (Ext x st) = let (s, t) = split st
113 split (Ext x st) = let (s, t) = split st
90− in (s, Ext x t)
114+ in (s, Ext x t)
91−
92−
93
115
94{-| Remove duplicates from a sorted list -}
116{-| Remove duplicates from a sorted list -}
95type family Nub t where
117type family Nub t where
@@ -99,7 +121,7 @@ type family Nub t where
99 Nub (e ': f ': s) = e ': Nub (f ': s)
121 Nub (e ': f ': s) = e ': Nub (f ': s)
100
122
101{-| Value-level counterpart to the type-level 'Nub'
123{-| Value-level counterpart to the type-level 'Nub'
102− 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,
103 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 -}
104
126
105class Nubable t where
127class Nubable t where
@@ -111,7 +133,10 @@ instance Nubable '[] where
111instance Nubable '[e] where
133instance Nubable '[e] where
112 nub (Ext x Empty) = Ext x Empty
134 nub (Ext x Empty) = Ext x Empty
113
135
136+instance Nubable (e ': s) => Nubable (e ': e ': s) where
137+ nub (Ext _ (Ext e s)) = nub (Ext e s)
138+
114−instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
139+instance {-# OVERLAPS #-} (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
115 Nubable (f ': s)) => Nubable (e ': f ': s) where
140 Nubable (f ': s)) => Nubable (e ': f ': s) where
116 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))
117
142
@@ -120,13 +145,13 @@ instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
120class Subset s t where
145class Subset s t where
121 subset :: Set t -> Set s
146 subset :: Set t -> Set s
122
147
123−instance Subset '[] '[] where
148+instance Subset '[] '[] where
124 subset xs = Empty
149 subset xs = Empty
125
150
126−instance Subset '[] (x ': t) where
151+instance {-# OVERLAPPABLE #-} Subset s t => Subset s (x ': t) where
127− subset xs = Empty
152+ subset (Ext _ xs) = subset xs
128
153
129−instance Subset s t => Subset (x ': s) (x ': t) where
154+instance {-# OVERLAPS #-} Subset s t => Subset (x ': s) (x ': t) where
130 subset (Ext x xs) = Ext x (subset xs)
155 subset (Ext x xs) = Ext x (subset xs)
131
156
132
157
@@ -139,8 +164,17 @@ data Flag = FMin | FMax
139
164
140type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where
165type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where
141 Filter f p '[] = '[]
166 Filter f p '[] = '[]
142− 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)
143− 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)
144
178
145{-| Value-level quick sort that respects the type-level ordering -}
179{-| Value-level quick sort that respects the type-level ordering -}
146class Sortable xs where
180class Sortable xs where
@@ -164,11 +198,11 @@ instance FilterV f p '[] where
164
198
165instance (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
166 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)))
167− (Ext x (filterV f p xs)) (filterV f p xs)
201+ (Ext x (filterV f p xs)) (filterV f p xs)
168
202
169instance (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
170 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))))
171− (Ext x (filterV f p xs)) (filterV f p xs)
205+ (Ext x (filterV f p xs)) (filterV f p xs)
172
206
173class Conder g where
207class Conder g where
174 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)
@@ -183,30 +217,20 @@ instance Conder False where
183
217
184type family Cmp (a :: k) (b :: k) :: Ordering
218type family Cmp (a :: k) (b :: k) :: Ordering
185
219
186−{-| Pair a symbol (represetning a variable) with a type -}
220+{-| Membership of an element in a set, with an acommanying
187−infixl 2 :->
221+ value-level function that returns a bool -}
188−data (k :: Symbol) :-> (v :: *) = (Var k) :-> v
222+class Member a s where
189−
223+ member :: Proxy a -> Set s -> Bool
190−data Var (k :: Symbol) where Var :: Var k
224+
191− {-| Some special defaults for some common names -}
225+instance {-# OVERLAPS #-} Member a (a ': s) where
192− X :: Var "x"
226+ member _ (Ext x _) = True
193− Y :: Var "y"
227+
194− Z :: Var "z"
228+instance {-# OVERLAPPABLE #-} Member a s => Member a (b ': s) where
195−
229+ member a (Ext _ xs) = member a xs
196−
230+
197−instance (Show (Var k), Show v) => Show (k :-> v) where
231+type family MemberP a s :: Bool where
198− show (k :-> v) = "(" ++ show k ++ " :-> " ++ show v ++ ")"
232+ MemberP a '[] = False
199−instance Show (Var "x") where
233+ MemberP a (a ': s) = True
200− show X = "x"
234+ MemberP a (b ': s) = MemberP a s
201− show Var = "Var"
235+
202−instance Show (Var "y") where
236+type NonMember a s = MemberP a s ~ False
203− show Y = "y"
204− show Var = "Var"
205−instance Show (Var "z") where
206− show Z = "z"
207− show Var = "Var"
208−instance Show (Var v) where
209− show _ = "Var"
210−
211−{-| Symbol comparison -}
212−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.cabalnew file+90
@@ -0,0 +1,90 @@
1+name: type-level-sets
2+version: 0.8.9.0
3+synopsis: Type-level sets and finite maps (with value-level counterparts)
4+description:
5+ This package provides type-level sets (no duplicates, sorted to provide a normal form) via 'Set' and type-level
6+ finite maps via 'Map', with value-level counterparts.
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+ .
11+ Here is a brief example for finite maps:
12+ .
13+ >
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
26+ >
27+ > bar :: Map '["y" :-> Int, "w" :-> Int]
28+ > bar = Ext (Var :: (Var "y")) 3
29+ > $ Ext (Var :: (Var "w")) 1
30+ > $ Empty
31+ >
32+ > -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool]
33+ > foobar = foo `union` bar
34+ .
35+ The 'Map' type for 'foobar' here shows the normalised form (sorted with no duplicates).
36+ The type signatures is commented out as it can be infered. Running the example we get:
37+ .
38+ > >>> foobar
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
60+ .
61+ Note the types here are all inferred.
62+ .
63+license: BSD3
64+license-file: LICENSE
65+category: Type System, Data Structures
66+copyright: 2013-18 University of Kent
67+author: Dominic Orchard
68+maintainer: Dominic Orchard
69+stability: experimental
70+build-type: Simple
71+cabal-version: >= 1.6
72+tested-with: GHC >= 8.2.2
73+
74+extra-source-files: example.hs, example2.hs, changelog.md
75+
76+
77+source-repository head
78+ type: git
79+ location: https://github.com/dorchard/type-level-sets
80+
81+library
82+ hs-source-dirs: src
83+ other-extensions: TypeInType
84+
85+
86+ exposed-modules: Data.Type.Set
87+ Data.Type.Map
88+
89+ build-depends: base < 5,
90+ ghc-prim