@@ -1,12 +1,13 @@
11{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,
22 MultiParamTypeClasses, FlexibleInstances, PolyKinds,
33 FlexibleContexts, UndecidableInstances, ConstraintKinds,
4− ScopedTypeVariables #-}
4+ ScopedTypeVariables, TypeInType #-}
55
66module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
77 Sort, Sortable, (:++), Split(..), Cmp, Filter, Flag(..),
88 Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
9− Delete(..), Proxy(..)) where
9+ Delete(..), Proxy(..), remove, Remove, (:\),
10+ Member(..), NonMember, MemberP(..)) where
1011
1112import GHC.TypeLits
1213import Data.Type.Bool
@@ -15,7 +16,7 @@ import Data.Type.Equality
1516data Proxy (p :: k) = Proxy
1617
1718-- Value-level 'Set' representation, essentially a list
18−data Set (n :: [*]) where
19+data Set (n :: [k]) where
1920 {--| Construct an empty set -}
2021 Empty :: Set '[]
2122 {--| Extend a set with an element -}
@@ -73,6 +74,25 @@ append :: Set s -> Set t -> Set (s :++ t)
7374append Empty x = x
7475append (Ext e xs) ys = Ext e (append xs ys)
7576
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)
95+
7696{-| Splitting a union a set, given the sets we want to split it into -}
7797class Split s t st where
7898 -- where st ~ Union s t
@@ -93,8 +113,6 @@ instance {-# OVERLAPS #-} (Split s t st) => Split s (x ': t) (x ': st) where
93113 split (Ext x st) = let (s, t) = split st
94114 in (s, Ext x t)
95115
96−
97−
98116{-| Remove duplicates from a sorted list -}
99117type family Nub t where
100118 Nub '[] = '[]
@@ -130,10 +148,10 @@ class Subset s t where
130148instance Subset '[] '[] where
131149 subset xs = Empty
132150
133−instance Subset s t => Subset s (x ': t) where
151+instance {-# OVERLAPPABLE #-} Subset s t => Subset s (x ': t) where
134152 subset (Ext _ xs) = subset xs
135153
136−instance Subset s t => Subset (x ': s) (x ': t) where
154+instance {-# OVERLAPS #-} Subset s t => Subset (x ': s) (x ': t) where
137155 subset (Ext x xs) = Ext x (subset xs)
138156
139157
@@ -198,3 +216,21 @@ instance Conder False where
198216{-| Open-family for the ordering operation in the sort -}
199217
200218type family Cmp (a :: k) (b :: k) :: Ordering
219+
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