@@ -0,0 +1,206 @@
1+{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators, TypeFamilies,
2+ MultiParamTypeClasses, FlexibleInstances, PolyKinds, FlexibleContexts,
3+ UndecidableInstances, ConstraintKinds, OverlappingInstances, ScopedTypeVariables,
4+ AllowAmbiguousTypes #-}
5+
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
9+
10+import GHC.TypeLits
11+import Data.Type.Bool
12+import Data.Type.Equality
13+import Data.Proxy
14+
15+{-| Core Set definition, in terms of lists -}
16+data Set (n :: [*]) where
17+ Empty :: Set '[]
18+ Ext :: e -> Set s -> Set (e ': s)
19+
20+instance Show (Set '[]) where
21+ show Empty = "{}"
22+
23+instance (Show e, Show' (Set s)) => Show (Set (e ': s)) where
24+ show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}"
25+
26+class Show' t where
27+ show' :: t -> String
28+instance Show' (Set '[]) where
29+ show' Empty = ""
30+instance (Show' (Set s), Show e) => Show' (Set (e ': s)) where
31+ show' (Ext e s) = ", " ++ show e ++ (show' s)
32+
33+{-| At the type level, normalise the list form to the set form -}
34+type AsSet s = Nub (Sort s)
35+
36+{-| At the value level, noramlise the list form to the set form -}
37+asSet :: (Sortable s, Nubable (Sort s)) => Set s -> Set (AsSet s)
38+asSet x = nub (quicksort x)
39+
40+{-| Predicate to check if in the set form -}
41+type IsSet s = (s ~ Nub (Sort s))
42+
43+{-| 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,
46+ Union f f ~ f, Split f f f,
47+ Unionable f '[], Unionable '[] f)
48+
49+{-- Union --}
50+
51+{-| Union of sets -}
52+type Union s t = Nub (Sort (Append s t))
53+
54+union :: (Unionable s t) => Set s -> Set t -> Set (Union s t)
55+union s t = nub (quicksort (append s t))
56+
57+type Unionable s t = (Sortable (Append s t), Nubable (Sort (Append s t)))
58+
59+{-| 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)
63+
64+append :: Set s -> Set t -> Set (Append s t)
65+append Empty x = x
66+append (Ext e xs) ys = Ext e (append xs ys)
67+
68+{-| Useful alias for append -}
69+type (s :: [k]) :++ (t :: [k]) = Append s t
70+
71+{-| Splitting a union a set, given the sets we want to split it into -}
72+class Split s t st where
73+ -- where st ~ Union s t
74+ split :: Set st -> (Set s, Set t)
75+
76+instance Split '[] '[] '[] where
77+ split Empty = (Empty, Empty)
78+
79+instance Split s t st => Split (x ': s) (x ': t) (x ': st) where
80+ split (Ext x st) = let (s, t) = split st
81+ in (Ext x s, Ext x t)
82+
83+instance Split s t st => Split (x ': s) t (x ': st) where
84+ split (Ext x st) = let (s, t) = split st
85+ in (Ext x s, t)
86+
87+instance (Split s t st) => Split s (x ': t) (x ': st) where
88+ split (Ext x st) = let (s, t) = split st
89+ in (s, Ext x t)
90+
91+
92+
93+{-| Remove duplicates from a sorted list -}
94+type family Nub t where
95+ Nub '[] = '[]
96+ Nub '[e] = '[e]
97+ Nub (e ': e ': s) = Nub (e ': s)
98+ Nub (e ': f ': s) = e ': Nub (f ': s)
99+
100+{-| Value-level counterpart to the type-level 'Nub'
101+ Note: the value-level case for equal types is not define here,
102+ but should be given per-application, e.g., custom 'merging' behaviour may be required -}
103+
104+class Nubable t where
105+ nub :: Set t -> Set (Nub t)
106+
107+instance Nubable '[] where
108+ nub Empty = Empty
109+
110+instance Nubable '[e] where
111+ nub (Ext x Empty) = Ext x Empty
112+
113+instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
114+ Nubable (f ': s)) => Nubable (e ': f ': s) where
115+ nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))
116+
117+
118+{-| Construct a subsetset 's' from a superset 't' -}
119+class Subset s t where
120+ subset :: Set t -> Set s
121+
122+instance Subset '[] '[] where
123+ subset xs = Empty
124+
125+instance Subset '[] (x ': t) where
126+ subset xs = Empty
127+
128+instance Subset s t => Subset (x ': s) (x ': t) where
129+ subset (Ext x xs) = Ext x (subset xs)
130+
131+
132+{-| Type-level quick sort for normalising the representation of sets -}
133+type family Sort (xs :: [k]) :: [k] where
134+ Sort '[] = '[]
135+ Sort (x ': xs) = ((Sort (Filter FMin x xs)) :++ '[x]) :++ (Sort (Filter FMax x xs))
136+
137+data Flag = FMin | FMax
138+
139+type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where
140+ Filter f p '[] = '[]
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)
143+
144+{-| Value-level quick sort that respects the type-level ordering -}
145+class Sortable xs where
146+ quicksort :: Set xs -> Set (Sort xs)
147+
148+instance Sortable '[] where
149+ quicksort Empty = Empty
150+
151+instance (Sortable (Filter FMin p xs),
152+ Sortable (Filter FMax p xs), FilterV FMin p xs, FilterV FMax p xs) => Sortable (p ': xs) where
153+ quicksort (Ext p xs) = ((quicksort (less p xs)) `append` (Ext p Empty)) `append` (quicksort (more p xs))
154+ where less = filterV (Proxy::(Proxy FMin))
155+ more = filterV (Proxy::(Proxy FMax))
156+
157+{- Filter out the elements less-than or greater-than-or-equal to the pivot -}
158+class FilterV (f::Flag) p xs where
159+ filterV :: Proxy f -> p -> Set xs -> Set (Filter f p xs)
160+
161+instance FilterV f p '[] where
162+ filterV _ p Empty = Empty
163+
164+instance (Conder ((Cmp x p) == LT), FilterV FMin p xs) => FilterV FMin p (x ': xs) where
165+ filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy ((Cmp x p) == LT)))
166+ (Ext x (filterV f p xs)) (filterV f p xs)
167+
168+instance (Conder (((Cmp x p) == GT) || ((Cmp x p) == EQ)), FilterV FMax p xs) => FilterV FMax p (x ': xs) where
169+ filterV f@Proxy p (Ext x xs) = cond (Proxy::(Proxy (((Cmp x p) == GT) || ((Cmp x p) == EQ))))
170+ (Ext x (filterV f p xs)) (filterV f p xs)
171+
172+class Conder g where
173+ cond :: Proxy g -> Set s -> Set t -> Set (If g s t)
174+
175+instance Conder True where
176+ cond _ s t = s
177+
178+instance Conder False where
179+ cond _ s t = t
180+
181+{-| Open-family for the ordering operation in the sort -}
182+
183+type family Cmp (a :: k) (b :: k) :: Ordering
184+
185+{-| Pair a symbol (represetning a variable) with a type -}
186+infixl 2 :->
187+data (k :: Symbol) :-> (v :: *) = (Var k) :-> v
188+
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"
194+
195+
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"
204+
205+{-| Symbol comparison -}
206+type instance Cmp (v :-> a) (u :-> b) = CmpSymbol v u