git.iko.soy/type-level-sets
on e918f27 help sign in
e368927
swap
0 ahead, 48 behind
9 files changed+57−590
since splitsnapshots
unifiedsplit
.gitignore−1 README−56 changelog.md−5 example.hs−31 example2.hs−30 src/Data/Type/Map.hs−261 src/Data/Type/Set.hs+57−87 stack.yaml−29 type-level-sets.cabal−90
.gitignoredeleted−1
@@ -1 +0,0 @@
1−.stack-work
READMEdeleted−56
@@ -1,56 +0,0 @@
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,
4−Tomas Petricek <http://www.cl.cam.ac.uk/~dao29/publ/haskell14-effects.pdf>) to embed effect sets.
5−
6−The following shows an example:
7−
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:
32−
33− *Main> foobar
34− {w :-> 6, x :-> 2, y :-> 3, z :-> True}
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
54−
55−
56−
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.hsdeleted−31
@@ -1,31 +0,0 @@
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.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+57−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,
4+ AllowAmbiguousTypes #-}
55
6−module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
7− Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..),
8− Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
9− Delete(..), Proxy(..), remove, Remove, (:\),
10− Member(..), NonMember, MemberP(..)) where
6+module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
7+ Sort, Sortable, Append(..), Split(..), Cmp,
8+ Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..)) 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
@@ -133,10 +110,7 @@ instance Nubable '[] where
133110instance Nubable '[e] where
134111 nub (Ext x Empty) = Ext x Empty
135112
136−instance Nubable (e ': s) => Nubable (e ': e ': s) where
137− nub (Ext _ (Ext e s)) = nub (Ext e s)
138−
139−instance {-# OVERLAPS #-} (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
113+instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
140114 Nubable (f ': s)) => Nubable (e ': f ': s) where
141115 nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))
142116
@@ -145,13 +119,13 @@ instance {-# OVERLAPS #-} (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
145119class Subset s t where
146120 subset :: Set t -> Set s
147121
148−instance Subset '[] '[] where
122+instance Subset '[] '[] where
149123 subset xs = Empty
150124
151−instance {-# OVERLAPPABLE #-} Subset s t => Subset s (x ': t) where
152− subset (Ext _ xs) = subset xs
125+instance Subset '[] (x ': t) where
126+ subset xs = Empty
153127
154−instance {-# OVERLAPS #-} Subset s t => Subset (x ': s) (x ': t) where
128+instance Subset s t => Subset (x ': s) (x ': t) where
155129 subset (Ext x xs) = Ext x (subset xs)
156130
157131
@@ -164,17 +138,8 @@ data Flag = FMin | FMax
164138
165139type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where
166140 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)
141+ Filter FMin p (x ': xs) = If (Cmp x p == LT) (x ': (Filter FMin p xs)) (Filter FMin p xs)
142+ Filter FMax p (x ': xs) = If (Cmp x p == GT || Cmp x p == EQ) (x ': (Filter FMax p xs)) (Filter FMax p xs)
178143
179144{-| Value-level quick sort that respects the type-level ordering -}
180145class Sortable xs where
@@ -198,11 +163,11 @@ instance FilterV f p '[] where
198163
199164instance (Conder ((Cmp x p) == LT), FilterV FMin p xs) => FilterV FMin p (x ': xs) where
200165 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)
166+ (Ext x (filterV f p xs)) (filterV f p xs)
202167
203168instance (Conder (((Cmp x p) == GT) || ((Cmp x p) == EQ)), FilterV FMax p xs) => FilterV FMax p (x ': xs) where
204169 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)
170+ (Ext x (filterV f p xs)) (filterV f p xs)
206171
207172class Conder g where
208173 cond :: Proxy g -> Set s -> Set t -> Set (If g s t)
@@ -217,20 +182,25 @@ instance Conder False where
217182
218183type family Cmp (a :: k) (b :: k) :: Ordering
219184
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
185+{-| Pair a symbol (represetning a variable) with a type -}
186+infixl 2 :->
187+data (k :: Symbol) :-> (v :: *) = (Var k) :-> v
224188
225−instance {-# OVERLAPS #-} Member a (a ': s) where
226− member _ (Ext x _) = True
189+data Var (k :: Symbol) where Var :: Var k
190+ {-| Some special defaults for some common names -}
191+ X :: Var "x"
192+ Y :: Var "y"
193+ Z :: Var "z"
227194
228−instance {-# OVERLAPPABLE #-} Member a s => Member a (b ': s) where
229− member a (Ext _ xs) = member a xs
230195
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
196+instance (Show (Var k), Show v) => Show (k :-> v) where
197+ show (k :-> v) = "(" ++ show k ++ " :-> " ++ show v ++ ")"
198+instance Show (Var "x") where
199+ show _ = "x"
200+instance Show (Var "y") where
201+ show _ = "y"
202+instance Show (Var "z") where
203+ show _ = "z"
235204
236−type NonMember a s = MemberP a s ~ False
205+{-| Symbol comparison -}
206+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.cabaldeleted−90
@@ -1,90 +0,0 @@
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