@@ -1,27 +1,32 @@
1−{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,
2− MultiParamTypeClasses, FlexibleInstances, PolyKinds, FlexibleContexts,
3− UndecidableInstances, ConstraintKinds, ScopedTypeVariables #-}
1+{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,
2+ MultiParamTypeClasses, FlexibleInstances, PolyKinds,
3+ FlexibleContexts, UndecidableInstances, ConstraintKinds,
4+ ScopedTypeVariables, TypeInType #-}
45
5−module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
6− Sort, Sortable, Append(..), Split(..), Cmp,
6+module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
7+ Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..),
78 Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
8− (:->)(..), Var(..), Delete(..)) where
9+ Delete(..), Proxy(..), remove, Remove, (:\),
10+ Member(..), NonMember, MemberP(..)) where
911
1012import GHC.TypeLits
1113import Data.Type.Bool
1214import Data.Type.Equality
13−import Data.Proxy
1415
15−{-| Core Set definition, in terms of lists -}
16−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 -}
1721 Empty :: Set '[]
22+ {--| Extend a set with an element -}
1823 Ext :: e -> Set s -> Set (e ': s)
1924
2025instance Show (Set '[]) where
2126 show Empty = "{}"
2227
2328instance (Show e, Show' (Set s)) => Show (Set (e ': s)) where
24− show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}"
29+ show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}"
2530
2631class Show' t where
2732 show' :: t -> String
@@ -30,6 +35,10 @@ instance Show' (Set '[]) where
3035instance (Show' (Set s), Show e) => Show' (Set (e ': s)) where
3136 show' (Ext e s) = ", " ++ show e ++ (show' s)
3237
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+
3342{-| At the type level, normalise the list form to the set form -}
3443type AsSet s = Nub (Sort s)
3544
@@ -41,54 +50,68 @@ asSet x = nub (quicksort x)
4150type IsSet s = (s ~ Nub (Sort s))
4251
4352{-| Useful properties to be able to refer to someties -}
44−type SetProperties f = (Union f '[] ~ f, Split f '[] f,
45− Union '[] f ~ f, Split '[] f f,
53+type SetProperties f = (Union f '[] ~ f, Split f '[] f,
54+ Union '[] f ~ f, Split '[] f f,
4655 Union f f ~ f, Split f f f,
4756 Unionable f '[], Unionable '[] f)
4857
4958{-- Union --}
5059
5160{-| Union of sets -}
52−type Union s t = Nub (Sort (Append s t))
61+type Union s t = Nub (Sort (s :++ t))
5362
5463union :: (Unionable s t) => Set s -> Set t -> Set (Union s t)
5564union s t = nub (quicksort (append s t))
5665
57−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)))
5867
5968{-| List append (essentially set disjoint union) -}
60−type family Append (s :: [k]) (t :: [k]) :: [k] where
61− Append '[] t = t
62− 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)
6372
64−append :: Set s -> Set t -> Set (Append s t)
73+append :: Set s -> Set t -> Set (s :++ t)
6574append Empty x = x
6675append (Ext e xs) ys = Ext e (append xs ys)
6776
68−{-| Useful alias for append -}
69−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)
7095
7196{-| Splitting a union a set, given the sets we want to split it into -}
7297class Split s t st where
7398 -- where st ~ Union s t
74− split :: Set st -> (Set s, Set t)
99+ split :: Set st -> (Set s, Set t)
75100
76101instance Split '[] '[] '[] where
77102 split Empty = (Empty, Empty)
78103
79−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
80105 split (Ext x st) = let (s, t) = split st
81106 in (Ext x s, Ext x t)
82107
83−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
84109 split (Ext x st) = let (s, t) = split st
85− in (Ext x s, t)
110+ in (Ext x s, t)
86111
87−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
88113 split (Ext x st) = let (s, t) = split st
89− in (s, Ext x t)
90−
91−
114+ in (s, Ext x t)
92115
93116{-| Remove duplicates from a sorted list -}
94117type family Nub t where
@@ -98,7 +121,7 @@ type family Nub t where
98121 Nub (e ': f ': s) = e ': Nub (f ': s)
99122
100123{-| Value-level counterpart to the type-level 'Nub'
101− 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,
102125 but should be given per-application, e.g., custom 'merging' behaviour may be required -}
103126
104127class Nubable t where
@@ -113,7 +136,7 @@ instance Nubable '[e] where
113136instance Nubable (e ': s) => Nubable (e ': e ': s) where
114137 nub (Ext _ (Ext e s)) = nub (Ext e s)
115138
116−instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
139+instance {-# OVERLAPS #-} (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
117140 Nubable (f ': s)) => Nubable (e ': f ': s) where
118141 nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))
119142
@@ -122,13 +145,13 @@ instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
122145class Subset s t where
123146 subset :: Set t -> Set s
124147
125−instance Subset '[] '[] where
148+instance Subset '[] '[] where
126149 subset xs = Empty
127150
128−instance Subset '[] (x ': t) where
129− subset xs = Empty
151+instance {-# OVERLAPPABLE #-} Subset s t => Subset s (x ': t) where
152+ subset (Ext _ xs) = subset xs
130153
131−instance Subset s t => Subset (x ': s) (x ': t) where
154+instance {-# OVERLAPS #-} Subset s t => Subset (x ': s) (x ': t) where
132155 subset (Ext x xs) = Ext x (subset xs)
133156
134157
@@ -141,8 +164,8 @@ data Flag = FMin | FMax
141164
142165type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where
143166 Filter f p '[] = '[]
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)
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)
146169
147170type family DeleteFromList (e :: elem) (list :: [elem]) where
148171 DeleteFromList elem '[] = '[]
@@ -175,11 +198,11 @@ instance FilterV f p '[] where
175198
176199instance (Conder ((Cmp x p) == LT), FilterV FMin p xs) => FilterV FMin p (x ': xs) where
177200 filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy ((Cmp x p) == LT)))
178− (Ext x (filterV f p xs)) (filterV f p xs)
201+ (Ext x (filterV f p xs)) (filterV f p xs)
179202
180203instance (Conder (((Cmp x p) == GT) || ((Cmp x p) == EQ)), FilterV FMax p xs) => FilterV FMax p (x ': xs) where
181204 filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy (((Cmp x p) == GT) || ((Cmp x p) == EQ))))
182− (Ext x (filterV f p xs)) (filterV f p xs)
205+ (Ext x (filterV f p xs)) (filterV f p xs)
183206
184207class Conder g where
185208 cond :: Proxy g -> Set s -> Set t -> Set (If g s t)
@@ -194,30 +217,20 @@ instance Conder False where
194217
195218type family Cmp (a :: k) (b :: k) :: Ordering
196219
197−{-| Pair a symbol (representing a variable) with a type -}
198−infixl 2 :->
199−data (k :: Symbol) :-> (v :: *) = (Var k) :-> v
200−
201−data Var (k :: Symbol) where Var :: Var k
202− {- Some special defaults for some common names -}
203− X :: Var "x"
204− Y :: Var "y"
205− Z :: Var "z"
206−
207−
208−instance (Show (Var k), Show v) => Show (k :-> v) where
209− show (k :-> v) = "(" ++ show k ++ " :-> " ++ show v ++ ")"
210−instance Show (Var "x") where
211− show X = "x"
212− show Var = "Var"
213−instance Show (Var "y") where
214− show Y = "y"
215− show Var = "Var"
216−instance Show (Var "z") where
217− show Z = "z"
218− show Var = "Var"
219−instance Show (Var v) where
220− show _ = "Var"
221−
222−{-| Symbol comparison -}
223−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