@@ -1,32 +1,28 @@
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(..),
6+module Data.Type.Set (Set(..), Union, Unionable, union, quicksort, append,
7+ Sort, Sortable, Append(..), Split(..), Cmp,
88 Nub, Nubable(..), AsSet, asSet, IsSet, Subset(..),
9− Delete(..), Proxy(..), remove, Remove, (:\),
10− Member(..), NonMember, MemberP(..)) where
9+ (:->)(..), Var(..)) where
1110
1211import GHC.TypeLits
1312import Data.Type.Bool
1413import Data.Type.Equality
14+import Data.Proxy
1515
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 -}
16+{-| Core Set definition, in terms of lists -}
17+data Set (n :: [*]) where
2118 Empty :: Set '[]
22− {--| Extend a set with an element -}
2319 Ext :: e -> Set s -> Set (e ': s)
2420
2521instance Show (Set '[]) where
2622 show Empty = "{}"
2723
2824instance (Show e, Show' (Set s)) => Show (Set (e ': s)) where
29− show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}"
25+ show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}"
3026
3127class Show' t where
3228 show' :: t -> String
@@ -35,10 +31,6 @@ instance Show' (Set '[]) where
3531instance (Show' (Set s), Show e) => Show' (Set (e ': s)) where
3632 show' (Ext e s) = ", " ++ show e ++ (show' s)
3733
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−
4234{-| At the type level, normalise the list form to the set form -}
4335type AsSet s = Nub (Sort s)
4436
@@ -50,68 +42,54 @@ asSet x = nub (quicksort x)
5042type IsSet s = (s ~ Nub (Sort s))
5143
5244{-| 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,
45+type SetProperties f = (Union f '[] ~ f, Split f '[] f,
46+ Union '[] f ~ f, Split '[] f f,
5547 Union f f ~ f, Split f f f,
5648 Unionable f '[], Unionable '[] f)
5749
5850{-- Union --}
5951
6052{-| Union of sets -}
61−type Union s t = Nub (Sort (s :++ t))
53+type Union s t = Nub (Sort (Append s t))
6254
6355union :: (Unionable s t) => Set s -> Set t -> Set (Union s t)
6456union s t = nub (quicksort (append s t))
6557
66−type Unionable s t = (Sortable (s :++ t), Nubable (Sort (s :++ t)))
58+type Unionable s t = (Sortable (Append s t), Nubable (Sort (Append s t)))
6759
6860{-| 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)
61+type family Append (s :: [k]) (t :: [k]) :: [k] where
62+ Append '[] t = t
63+ Append (x ': xs) ys = x ': (Append xs ys)
7264
73−append :: Set s -> Set t -> Set (s :++ t)
65+append :: Set s -> Set t -> Set (Append s t)
7466append Empty x = x
7567append (Ext e xs) ys = Ext e (append xs ys)
7668
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)
69+{-| Useful alias for append -}
70+type (s :: [k]) :++ (t :: [k]) = Append s t
9571
9672{-| Splitting a union a set, given the sets we want to split it into -}
9773class Split s t st where
9874 -- where st ~ Union s t
99− split :: Set st -> (Set s, Set t)
75+ split :: Set st -> (Set s, Set t)
10076
10177instance Split '[] '[] '[] where
10278 split Empty = (Empty, Empty)
10379
104−instance {-# OVERLAPPABLE #-} Split s t st => Split (x ': s) (x ': t) (x ': st) where
80+instance Split s t st => Split (x ': s) (x ': t) (x ': st) where
10581 split (Ext x st) = let (s, t) = split st
10682 in (Ext x s, Ext x t)
10783
108−instance {-# OVERLAPS #-} Split s t st => Split (x ': s) t (x ': st) where
84+instance Split s t st => Split (x ': s) t (x ': st) where
10985 split (Ext x st) = let (s, t) = split st
110− in (Ext x s, t)
86+ in (Ext x s, t)
11187
112−instance {-# OVERLAPS #-} (Split s t st) => Split s (x ': t) (x ': st) where
88+instance (Split s t st) => Split s (x ': t) (x ': st) where
11389 split (Ext x st) = let (s, t) = split st
114− in (s, Ext x t)
90+ in (s, Ext x t)
91+
92+
11593
11694{-| Remove duplicates from a sorted list -}
11795type family Nub t where
@@ -121,7 +99,7 @@ type family Nub t where
12199 Nub (e ': f ': s) = e ': Nub (f ': s)
122100
123101{-| Value-level counterpart to the type-level 'Nub'
124− Note: the value-level case for equal types is not define here,
102+ Note: the value-level case for equal types is not define here,
125103 but should be given per-application, e.g., custom 'merging' behaviour may be required -}
126104
127105class Nubable t where
@@ -133,10 +111,7 @@ instance Nubable '[] where
133111instance Nubable '[e] where
134112 nub (Ext x Empty) = Ext x Empty
135113
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)),
114+instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
140115 Nubable (f ': s)) => Nubable (e ': f ': s) where
141116 nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))
142117
@@ -145,13 +120,13 @@ instance {-# OVERLAPS #-} (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
145120class Subset s t where
146121 subset :: Set t -> Set s
147122
148−instance Subset '[] '[] where
123+instance Subset '[] '[] where
149124 subset xs = Empty
150125
151−instance {-# OVERLAPPABLE #-} Subset s t => Subset s (x ': t) where
152− subset (Ext _ xs) = subset xs
126+instance Subset '[] (x ': t) where
127+ subset xs = Empty
153128
154−instance {-# OVERLAPS #-} Subset s t => Subset (x ': s) (x ': t) where
129+instance Subset s t => Subset (x ': s) (x ': t) where
155130 subset (Ext x xs) = Ext x (subset xs)
156131
157132
@@ -164,17 +139,8 @@ data Flag = FMin | FMax
164139
165140type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where
166141 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)
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)
178144
179145{-| Value-level quick sort that respects the type-level ordering -}
180146class Sortable xs where
@@ -198,11 +164,11 @@ instance FilterV f p '[] where
198164
199165instance (Conder ((Cmp x p) == LT), FilterV FMin p xs) => FilterV FMin p (x ': xs) where
200166 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)
167+ (Ext x (filterV f p xs)) (filterV f p xs)
202168
203169instance (Conder (((Cmp x p) == GT) || ((Cmp x p) == EQ)), FilterV FMax p xs) => FilterV FMax p (x ': xs) where
204170 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)
171+ (Ext x (filterV f p xs)) (filterV f p xs)
206172
207173class Conder g where
208174 cond :: Proxy g -> Set s -> Set t -> Set (If g s t)
@@ -217,20 +183,30 @@ instance Conder False where
217183
218184type family Cmp (a :: k) (b :: k) :: Ordering
219185
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
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