git.iko.soy/type-level-sets
on dab85ce help sign in
e368927
swap
0 ahead, 41 behind
9 files changed+128−539
since splitsnapshots
unifiedsplit
.gitignore−1 README+21−42 changelog.md−5 example.hs+13−26 example2.hs−30 src/Data/Type/Map.hs−261 src/Data/Type/Set.hs+65−87 stack.yaml−29 type-level-sets.cabal+29−58
.gitignoredeleted−1
@@ -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
2−subsets/submaps, and splitting sets/maps. This library was originally built based on
3−"Embedding effect systems in Haskell" (Dominic Orchard,
1+This library provides type-level sets to Haskell, with a value level counterpart, and operations for taking the union, computing
2+subsets, and split sets. Also included is a "mapping" type constructor that pairs symbols with types. This can be used to represent
3+sets of variable-type pairs, which is used in the paper "Embedding effect systems in Haskell" (Dominic Orchard,
44Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf>) to embed effect sets.
55
66The following shows an example:
77
8− {-# LANGUAGE DataKinds, TypeOperators, 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:
8+ {-# LANGUAGE DataKinds, TypeOperators #-}
329
33− *Main> foobar
34− {w :-> 6, x :-> 2, y :-> 3, z :-> True}
10+ import Data.Type.Set
3511
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
3717
38− import GHC.TypeLits
39− import Data.Type.Set
40− type instance Cmp (Natural n) (Natural m) = CmpNat n m
18+ bar :: Set '["y" :-> Int, "w" :-> Int]
19+ bar = Ext ((Var :: (Var "y")) :-> 3) $
20+ Ext ((Var :: (Var "w")) :-> 1) $
21+ Empty
4122
42− data Natural (a :: Nat) where
43− Z :: Natural 0
44− S :: Natural n -> Natural (n + 1)
23+ -- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Int]
24+ foobar = foo `union` bar
4525
46− -- foo :: Set '[Natural 0, Natural 1, Natural 3]
47− foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))
26+The 'Set' type for 'foobar' here shows the normalised form (sorted with no duplicates).
27+The type signatures is commented out as it can be infered. Running the example we get:
4828
49− -- bar :: Set '[Natural 1, Natural 2]
50− bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))
29+ *Main> foobar
30+ {(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)}
5131
52− -- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]
53− foobar = foo `union` bar
32+Thus, we see that the first value paired with the "w" variable is dropped.
5433
5534
5635
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 #-}
22
3−import GHC.TypeLits
4−import Data.Type.Map
3+import Data.Type.Set
54
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
5+foo :: Set '["x" :-> Int, "z" :-> Int, "w" :-> Int]
6+foo = Ext ((Var :: (Var "x")) :-> 2) $
7+ Ext ((Var :: (Var "z")) :-> 4) $
8+ Ext ((Var :: (Var "w")) :-> 5) $
9+ Empty
1110
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
11+bar :: Set '["y" :-> Int, "w" :-> Int]
12+bar = Ext ((Var :: (Var "y")) :-> 3) $
13+ Ext ((Var :: (Var "w")) :-> 1) $
14+ Empty
2515
2616-- 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
17+-- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Integer, "z" :-> Int]
18+foobar = foo `union` bar
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,
2− MultiParamTypeClasses, FlexibleInstances, PolyKinds,
3− FlexibleContexts, UndecidableInstances, ConstraintKinds,
4− ScopedTypeVariables, TypeInType #-}
1+{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,
2+ MultiParamTypeClasses, FlexibleInstances, PolyKinds, FlexibleContexts,
3+ UndecidableInstances, ConstraintKinds, OverlappingInstances, ScopedTypeVariables #-}
54
6−module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
7− Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..),
5+module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
6+ Sort, Sortable, Append(..), Split(..), Cmp,
87 Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
9− Delete(..), Proxy(..), remove, Remove, (:\),
10− Member(..), NonMember, MemberP(..)) where
8+ (:->)(..), Var(..)) where
119
1210import GHC.TypeLits
1311import Data.Type.Bool
1412import Data.Type.Equality
13+import Data.Proxy
1514
16−data Proxy (p :: k) = Proxy
17−
18−-- Value-level 'Set' representation, essentially a list
19−data Set (n :: [k]) where
20− {--| Construct an empty set -}
15+{-| Core Set definition, in terms of lists -}
16+data Set (n :: [*]) where
2117 Empty :: Set '[]
22− {--| Extend a set with an element -}
2318 Ext :: e -> Set s -> Set (e ': s)
2419
2520instance Show (Set '[]) where
2621 show Empty = "{}"
2722
2823instance (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) ++ "}"
3025
3126class Show' t where
3227 show' :: t -> String
@@ -35,10 +30,6 @@ instance Show' (Set '[]) where
3530instance (Show' (Set s), Show e) => Show' (Set (e ': s)) where
3631 show' (Ext e s) = ", " ++ show e ++ (show' s)
3732
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−
4233{-| At the type level, normalise the list form to the set form -}
4334type AsSet s = Nub (Sort s)
4435
@@ -50,68 +41,54 @@ asSet x = nub (quicksort x)
5041type IsSet s = (s ~ Nub (Sort s))
5142
5243{-| Useful properties to be able to refer to someties -}
53−type SetProperties f = (Union f '[] ~ f, Split f '[] f,
54− Union '[] f ~ f, Split '[] f f,
44+type SetProperties f = (Union f '[] ~ f, Split f '[] f,
45+ Union '[] f ~ f, Split '[] f f,
5546 Union f f ~ f, Split f f f,
5647 Unionable f '[], Unionable '[] f)
5748
5849{-- Union --}
5950
6051{-| Union of sets -}
61−type Union s t = Nub (Sort (s :++ t))
52+type Union s t = Nub (Sort (Append s t))
6253
6354union :: (Unionable s t) => Set s -> Set t -> Set (Union s t)
6455union s t = nub (quicksort (append s t))
6556
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)))
6758
6859{-| List append (essentially set disjoint union) -}
69−type family (:++) (x :: [k]) (y :: [k]) :: [k] where
70− '[] :++ xs = xs
71− (x ': xs) :++ ys = x ': (xs :++ ys)
60+type family Append (s :: [k]) (t :: [k]) :: [k] where
61+ Append '[] t = t
62+ Append (x ': xs) ys = x ': (Append xs ys)
7263
73−append :: Set s -> Set t -> Set (s :++ t)
64+append :: Set s -> Set t -> Set (Append s t)
7465append Empty x = x
7566append (Ext e xs) ys = Ext e (append xs ys)
7667
77−{-| Delete elements from a set -}
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)
68+{-| Useful alias for append -}
69+type (s :: [k]) :++ (t :: [k]) = Append s t
9570
9671{-| Splitting a union a set, given the sets we want to split it into -}
9772class Split s t st where
9873 -- where st ~ Union s t
99− split :: Set st -> (Set s, Set t)
74+ split :: Set st -> (Set s, Set t)
10075
10176instance Split '[] '[] '[] where
10277 split Empty = (Empty, Empty)
10378
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
10580 split (Ext x st) = let (s, t) = split st
10681 in (Ext x s, Ext x t)
10782
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
10984 split (Ext x st) = let (s, t) = split st
110− in (Ext x s, t)
85+ in (Ext x s, t)
11186
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
11388 split (Ext x st) = let (s, t) = split st
114− in (s, Ext x t)
89+ in (s, Ext x t)
90+
91+
11592
11693{-| Remove duplicates from a sorted list -}
11794type family Nub t where
@@ -121,7 +98,7 @@ type family Nub t where
12198 Nub (e ': f ': s) = e ': Nub (f ': s)
12299
123100{-| 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,
125102 but should be given per-application, e.g., custom 'merging' behaviour may be required -}
126103
127104class Nubable t where
@@ -136,7 +113,7 @@ instance Nubable '[e] where
136113instance Nubable (e ': s) => Nubable (e ': e ': s) where
137114 nub (Ext _ (Ext e s)) = nub (Ext e s)
138115
139−instance {-# OVERLAPS #-} (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
116+instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
140117 Nubable (f ': s)) => Nubable (e ': f ': s) where
141118 nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))
142119
@@ -145,13 +122,13 @@ instance {-# OVERLAPS #-} (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
145122class Subset s t where
146123 subset :: Set t -> Set s
147124
148−instance Subset '[] '[] where
125+instance Subset '[] '[] where
149126 subset xs = Empty
150127
151−instance {-# OVERLAPPABLE #-} Subset s t => Subset s (x ': t) where
152− subset (Ext _ xs) = subset xs
128+instance Subset '[] (x ': t) where
129+ subset xs = Empty
153130
154−instance {-# OVERLAPS #-} Subset s t => Subset (x ': s) (x ': t) where
131+instance Subset s t => Subset (x ': s) (x ': t) where
155132 subset (Ext x xs) = Ext x (subset xs)
156133
157134
@@ -164,17 +141,8 @@ data Flag = FMin | FMax
164141
165142type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where
166143 Filter f p '[] = '[]
167− 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)
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+ 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)
178146
179147{-| Value-level quick sort that respects the type-level ordering -}
180148class Sortable xs where
@@ -198,11 +166,11 @@ instance FilterV f p '[] where
198166
199167instance (Conder ((Cmp x p) == LT), FilterV FMin p xs) => FilterV FMin p (x ': xs) where
200168 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)
202170
203171instance (Conder (((Cmp x p) == GT) || ((Cmp x p) == EQ)), FilterV FMax p xs) => FilterV FMax p (x ': xs) where
204172 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)
206174
207175class Conder g where
208176 cond :: Proxy g -> Set s -> Set t -> Set (If g s t)
@@ -217,20 +185,30 @@ instance Conder False where
217185
218186type family Cmp (a :: k) (b :: k) :: Ordering
219187
220−{-| Membership of an element in a set, with an acommanying
221− value-level function that returns a bool -}
222−class Member a s where
223− member :: Proxy a -> Set s -> Bool
224−
225−instance {-# OVERLAPS #-} Member a (a ': s) where
226− member _ (Ext x _) = True
227−
228−instance {-# OVERLAPPABLE #-} Member a s => Member a (b ': s) where
229− member a (Ext _ xs) = member a xs
230−
231−type family MemberP a s :: Bool where
232− MemberP a '[] = False
233− MemberP a (a ': s) = True
234− MemberP a (b ': s) = MemberP a s
235−
236−type NonMember a s = MemberP a s ~ False
188+{-| Pair a symbol (represetning a variable) with a type -}
189+infixl 2 :->
190+data (k :: Symbol) :-> (v :: *) = (Var k) :-> v
191+
192+data Var (k :: Symbol) where Var :: Var k
193+ {-| Some special defaults for some common names -}
194+ X :: Var "x"
195+ Y :: Var "y"
196+ Z :: Var "z"
197+
198+
199+instance (Show (Var k), Show v) => Show (k :-> v) where
200+ show (k :-> v) = "(" ++ show k ++ " :-> " ++ show v ++ ")"
201+instance Show (Var "x") where
202+ show X = "x"
203+ show Var = "Var"
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 @@
11name: 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.
2+version: 0.5
3+synopsis: Type-level sets (with value-level counterparts and various operations)
4+description:
5+ This package provides type-level sets (no duplicates, sorted to provide a nomral form) via 'Set',
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)
78 .
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.
9+ Here is a brief example:
1010 .
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
2611 >
27− > bar :: Map '["y" :-> Int, "w" :-> Int]
28− > bar = Ext (Var :: (Var "y")) 3
29− > $ Ext (Var :: (Var "w")) 1
30− > $ Empty
12+ > import Data.Type.Set
3113 >
32− > -- foobar :: Map '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Bool]
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+ >
25+ > -- foobar :: Set '["w" :-> Int, "x" :-> Int, "y" :-> Int, "z" :-> Int]
3326 > foobar = foo `union` bar
3427 .
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).
3629 The type signatures is commented out as it can be infered. Running the example we get:
3730 .
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
31+ > >>> foobar
32+ > [(Var :-> 1), (Var :-> 2), (Var :-> 3), (Var :-> 4)]
6033 .
61− Note the types here are all inferred.
34+ Thus, we see that the first value paired with the \"w\" variable is dropped.
6235 .
6336license: BSD3
6437license-file: LICENSE
6538category: Type System, Data Structures
66−copyright: 2013-18 University of Kent
39+copyright: 2013-14 University of Cambridge
6740author: Dominic Orchard
6841maintainer: Dominic Orchard
6942stability: experimental
7043build-type: Simple
7144cabal-version: >= 1.6
72−tested-with: GHC >= 8.2.2
45+tested-with: GHC == 7.8.2
7346
74−extra-source-files: example.hs, example2.hs, changelog.md
47+extra-source-files: example.hs
7548
7649
7750source-repository head
@@ -80,11 +53,9 @@ source-repository head
8053
8154library
8255 hs-source-dirs: src
83− other-extensions: TypeInType
8456
8557
8658 exposed-modules: Data.Type.Set
87− Data.Type.Map
88−
59+
8960 build-depends: base < 5,
90− ghc-prim
61+ ghc-prim