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