@@ -1,28 +1,32 @@
1−{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,
2− MultiParamTypeClasses, FlexibleInstances, PolyKinds, FlexibleContexts,
3− UndecidableInstances, ConstraintKinds, OverlappingInstances, ScopedTypeVariables,
4− AllowAmbiguousTypes #-}
1+{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,
2+ MultiParamTypeClasses, FlexibleInstances, PolyKinds,
3+ FlexibleContexts, UndecidableInstances, ConstraintKinds,
4+ ScopedTypeVariables, TypeInType #-}
55
6−module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
7− Sort, Sortable, Append(..), Split(..), Cmp,
6+module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
7+ Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..),
88 Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
9− (:->)(..), Var(..)) where
9+ Delete(..), Proxy(..), remove, Remove, (:\),
10+ Member(..), NonMember, MemberP(..)) where
1011
1112import GHC.TypeLits
1213import Data.Type.Bool
1314import Data.Type.Equality
14−import Data.Proxy
1515
16−{-| Core Set definition, in terms of lists -}
17−data Set (n :: [*]) where
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 -}
1821 Empty :: Set '[]
22+ {--| Extend a set with an element -}
1923 Ext :: e -> Set s -> Set (e ': s)
2024
2125instance Show (Set '[]) where
2226 show Empty = "{}"
2327
2428instance (Show e, Show' (Set s)) => Show (Set (e ': s)) where
25− show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}"
29+ show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}"
2630
2731class Show' t where
2832 show' :: t -> String
@@ -31,6 +35,10 @@ instance Show' (Set '[]) where
3135instance (Show' (Set s), Show e) => Show' (Set (e ': s)) where
3236 show' (Ext e s) = ", " ++ show e ++ (show' s)
3337
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+
3442{-| At the type level, normalise the list form to the set form -}
3543type AsSet s = Nub (Sort s)
3644
@@ -42,54 +50,68 @@ asSet x = nub (quicksort x)
4250type IsSet s = (s ~ Nub (Sort s))
4351
4452{-| Useful properties to be able to refer to someties -}
45−type SetProperties f = (Union f '[] ~ f, Split f '[] f,
46− Union '[] f ~ f, Split '[] f f,
53+type SetProperties f = (Union f '[] ~ f, Split f '[] f,
54+ Union '[] f ~ f, Split '[] f f,
4755 Union f f ~ f, Split f f f,
4856 Unionable f '[], Unionable '[] f)
4957
5058{-- Union --}
5159
5260{-| Union of sets -}
53−type Union s t = Nub (Sort (Append s t))
61+type Union s t = Nub (Sort (s :++ t))
5462
5563union :: (Unionable s t) => Set s -> Set t -> Set (Union s t)
5664union s t = nub (quicksort (append s t))
5765
58−type Unionable s t = (Sortable (Append s t), Nubable (Sort (Append s t)))
66+type Unionable s t = (Sortable (s :++ t), Nubable (Sort (s :++ t)))
5967
6068{-| List append (essentially set disjoint union) -}
61−type family Append (s :: [k]) (t :: [k]) :: [k] where
62− Append '[] t = t
63− Append (x ': xs) ys = x ': (Append xs ys)
69+type family (:++) (x :: [k]) (y :: [k]) :: [k] where
70+ '[] :++ xs = xs
71+ (x ': xs) :++ ys = x ': (xs :++ ys)
6472
65−append :: Set s -> Set t -> Set (Append s t)
73+append :: Set s -> Set t -> Set (s :++ t)
6674append Empty x = x
6775append (Ext e xs) ys = Ext e (append xs ys)
6876
69−{-| Useful alias for append -}
70−type (s :: [k]) :++ (t :: [k]) = Append s t
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)
7195
7296{-| Splitting a union a set, given the sets we want to split it into -}
7397class Split s t st where
7498 -- where st ~ Union s t
75− split :: Set st -> (Set s, Set t)
99+ split :: Set st -> (Set s, Set t)
76100
77101instance Split '[] '[] '[] where
78102 split Empty = (Empty, Empty)
79103
80−instance Split s t st => Split (x ': s) (x ': t) (x ': st) where
104+instance {-# OVERLAPPABLE #-} Split s t st => Split (x ': s) (x ': t) (x ': st) where
81105 split (Ext x st) = let (s, t) = split st
82106 in (Ext x s, Ext x t)
83107
84−instance Split s t st => Split (x ': s) t (x ': st) where
108+instance {-# OVERLAPS #-} Split s t st => Split (x ': s) t (x ': st) where
85109 split (Ext x st) = let (s, t) = split st
86− in (Ext x s, t)
110+ in (Ext x s, t)
87111
88−instance (Split s t st) => Split s (x ': t) (x ': st) where
112+instance {-# OVERLAPS #-} (Split s t st) => Split s (x ': t) (x ': st) where
89113 split (Ext x st) = let (s, t) = split st
90− in (s, Ext x t)
91−
92−
114+ in (s, Ext x t)
93115
94116{-| Remove duplicates from a sorted list -}
95117type family Nub t where
@@ -99,7 +121,7 @@ type family Nub t where
99121 Nub (e ': f ': s) = e ': Nub (f ': s)
100122
101123{-| Value-level counterpart to the type-level 'Nub'
102− Note: the value-level case for equal types is not define here,
124+ Note: the value-level case for equal types is not define here,
103125 but should be given per-application, e.g., custom 'merging' behaviour may be required -}
104126
105127class Nubable t where
@@ -111,7 +133,10 @@ instance Nubable '[] where
111133instance Nubable '[e] where
112134 nub (Ext x Empty) = Ext x Empty
113135
114−instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
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)),
115140 Nubable (f ': s)) => Nubable (e ': f ': s) where
116141 nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))
117142
@@ -120,13 +145,13 @@ instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
120145class Subset s t where
121146 subset :: Set t -> Set s
122147
123−instance Subset '[] '[] where
148+instance Subset '[] '[] where
124149 subset xs = Empty
125150
126−instance Subset '[] (x ': t) where
127− subset xs = Empty
151+instance {-# OVERLAPPABLE #-} Subset s t => Subset s (x ': t) where
152+ subset (Ext _ xs) = subset xs
128153
129−instance Subset s t => Subset (x ': s) (x ': t) where
154+instance {-# OVERLAPS #-} Subset s t => Subset (x ': s) (x ': t) where
130155 subset (Ext x xs) = Ext x (subset xs)
131156
132157
@@ -139,8 +164,17 @@ data Flag = FMin | FMax
139164
140165type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where
141166 Filter f p '[] = '[]
142− Filter FMin p (x ': xs) = If (Cmp x p == LT) (x ': (Filter FMin p xs)) (Filter FMin p xs)
143− Filter FMax p (x ': xs) = If (Cmp x p == GT || Cmp x p == EQ) (x ': (Filter FMax p xs)) (Filter FMax p xs)
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)
144178
145179{-| Value-level quick sort that respects the type-level ordering -}
146180class Sortable xs where
@@ -164,11 +198,11 @@ instance FilterV f p '[] where
164198
165199instance (Conder ((Cmp x p) == LT), FilterV FMin p xs) => FilterV FMin p (x ': xs) where
166200 filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy ((Cmp x p) == LT)))
167− (Ext x (filterV f p xs)) (filterV f p xs)
201+ (Ext x (filterV f p xs)) (filterV f p xs)
168202
169203instance (Conder (((Cmp x p) == GT) || ((Cmp x p) == EQ)), FilterV FMax p xs) => FilterV FMax p (x ': xs) where
170204 filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy (((Cmp x p) == GT) || ((Cmp x p) == EQ))))
171− (Ext x (filterV f p xs)) (filterV f p xs)
205+ (Ext x (filterV f p xs)) (filterV f p xs)
172206
173207class Conder g where
174208 cond :: Proxy g -> Set s -> Set t -> Set (If g s t)
@@ -183,30 +217,20 @@ instance Conder False where
183217
184218type family Cmp (a :: k) (b :: k) :: Ordering
185219
186−{-| Pair a symbol (represetning a variable) with a type -}
187−infixl 2 :->
188−data (k :: Symbol) :-> (v :: *) = (Var k) :-> v
189−
190−data Var (k :: Symbol) where Var :: Var k
191− {-| Some special defaults for some common names -}
192− X :: Var "x"
193− Y :: Var "y"
194− Z :: Var "z"
195−
196−
197−instance (Show (Var k), Show v) => Show (k :-> v) where
198− show (k :-> v) = "(" ++ show k ++ " :-> " ++ show v ++ ")"
199−instance Show (Var "x") where
200− show X = "x"
201− show Var = "Var"
202−instance Show (Var "y") where
203− show Y = "y"
204− show Var = "Var"
205−instance Show (Var "z") where
206− show Z = "z"
207− show Var = "Var"
208−instance Show (Var v) where
209− show _ = "Var"
210−
211−{-| Symbol comparison -}
212−type instance Cmp (v :-> a) (u :-> b) = CmpSymbol v u
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