@@ -1,46 +1,183 @@
11-- | Collection of type families on type lists. This module differs
2−-- from __Data.Singletons.Prelude.List__ because it polykinded and
3−-- works with __[*]__ as well
4−
5−module TypeFun.Data.List where
2+-- from __Data.Singletons.Prelude.List__ because works with __[*]__
3+-- and relies on GHC's type equality (~). The rest of required
4+-- operations like 'Reverse' or '(:++:)' you could find in singletons
5+
6+module TypeFun.Data.List
7+ ( -- * Primitive operations on lists
8+ Length
9+ , Drop
10+ , Take
11+ , Delete
12+ , Remove
13+ , (:++:)
14+ -- * Elements lookup
15+ , IndexOf
16+ , IndexOfMay
17+ , IndexOfMay'
18+ , IndicesOfMay
19+ , IndicesOf
20+ , Index
21+ , IndexMay
22+ , IndicesMay
23+ , Indices
24+ , Elem
25+ , NotElem
26+ , Count
27+ -- * Operations with lists
28+ , SubList
29+ , NotSubList
30+ , IsPrefixOf
31+ , IsNotPrefixOf
32+ , IsPrefixOfBool
33+ -- * Set operations
34+ , Union
35+ , UnionList
36+ , AppendUniq
37+ , Intersect
38+ , Substract
39+ -- * Uniqueness checking
40+ , ElementIsUniq
41+ , UniqElements
42+ , UniqElements'
43+ -- * Unsafe helpers
44+ , appendId
45+ , subListId
46+ ) where
647
748import Data.Type.Bool
849import GHC.Exts
950import GHC.TypeLits
1051import TypeFun.Data.Eq
11−import TypeFun.Data.List.Internal
1252import TypeFun.Data.Maybe
53+import TypeFun.Data.Peano
54+import Unsafe.Coerce
55+
56+------------------------------------------------------------------------
57+-- NOTE: Errors type classes. These type classes are not in separate --
58+-- module because in this case user could import them and instantiate --
59+-- by mistake. The name of typeclass is an error message in fact. We --
60+-- have not any way to fail constraint explicitly, so this hack was --
61+-- introduced. --
62+------------------------------------------------------------------------
63+
64+class ElementNotFoundInList a s
65+
66+class ElementIsInList a s
67+
68+class ListIsNotPrefixOf a b
69+
70+class ListIsPrefixOf a b
71+
72+class ElementIsNotUniqInList a s
73+
74+class IndexNotFoundInList a s
75+
76+----------------------
77+-- main module code --
78+----------------------
79+
80+
81+type family Length (a :: [k]) :: N where
82+ Length '[] = 'Z
83+ Length (a ': as) = 'S (Length as)
84+
85+type family Drop (c :: N) (s :: [k]) :: [k] where
86+ Drop 'Z s = s
87+ Drop ('S c) '[] = '[]
88+ Drop ('S c) (a ': as) = Drop c as
89+
90+type family Take (c :: N) (s :: [k]) :: [k] where
91+ Take 'Z s = '[]
92+ Take ('S c) '[] = '[]
93+ Take ('S c) (a ': as) = a ': (Take c as)
94+
95+-- | Remove first argument type from anywhere in a list.
96+type family Delete (a :: k) (s :: [k]) :: [k] where
97+ Delete a '[] = '[]
98+ Delete a (a ': as) = Delete a as
99+ Delete a (b ': as) = b ': (Delete a as)
100+
101+-- | Remove index from the list
102+type family Remove (i :: N) (a :: [k]) :: [k] where
103+ Remove i '[] = '[]
104+ Remove 'Z (a ': as) = as
105+ Remove ('S i) (a ': as) = a ': (Remove i as)
106+
107+type family (:++:) (a :: [k]) (b :: [k]) :: [k] where
108+ '[] :++: b = b
109+ (a ': as) :++: b = a ': (as :++: b)
13110
14−type family Length (a :: [k]) :: Nat where
15− Length '[] = 0
16− Length (a ': as) = 1 + (Length as)
111+appendId
112+ :: forall proxy l r
113+ . proxy l
114+ -> (l ~ (l :++: '[]) => r)
115+ -> r
116+appendId = unsafeCoerce id
117+
118+type IndexOf a s = FromJust (IndexOfMay a s)
119+
120+type IndexOfMay a s = IndexOfMay' Z a s
121+
122+type family IndexOfMay' (acc :: N) (a :: k) (s :: [k]) :: Maybe N where
123+ IndexOfMay' acc a '[] = 'Nothing
124+ IndexOfMay' acc a (a ': as) = 'Just acc
125+ IndexOfMay' acc a (b ': as) = IndexOfMay' (S acc) a as
126+
127+type family IndicesOfMay (a :: [k]) (b :: [k]) :: [Maybe N] where
128+ IndicesOfMay '[] bs = '[]
129+ IndicesOfMay (a ': as) bs = (IndexOfMay a bs) ': (IndicesOfMay as bs)
130+
131+type family IndicesOf (a :: [k]) (b :: [k]) :: [N] where
132+ IndicesOf '[] bs = '[]
133+ IndicesOf (a ': as) bs = (IndexOf a bs) ': (IndicesOf as bs)
134+
135+type Index idx s = FromJust (IndexMay idx s)
136+
137+type family IndexMay (idx :: N) (s :: [k]) :: Maybe k where
138+ IndexMay idx '[] = 'Nothing
139+ IndexMay Z (a ': as) = 'Just a
140+ IndexMay (S idx) (a ': as) = IndexMay idx as
141+
142+type family IndicesMay (idxs :: [N]) (a :: [k]) :: [Maybe k] where
143+ IndicesMay '[] as = '[]
144+ IndicesMay (i ': idxs) as = (IndexMay i as) ': (IndicesMay idxs as)
145+
146+type family Indices (idxs :: [N]) (a :: [k]) :: [k] where
147+ Indices '[] as = '[]
148+ Indices (i ': idxs) as = (Index i as) ': (Indices idxs as)
17149
18150-- | Generates unresolvable constraint if fists element is not
19151-- contained inside of second
20−type Elem a s = NothingToConstr (IndexOf a s)
152+type Elem a s = NothingToConstr (IndexOfMay a s)
21153 (ElementNotFoundInList a s)
22154
23155-- | Reverse of 'Elem'
24−type NotElem a s = JustToConstr (IndexOf a s)
156+type NotElem a s = JustToConstr (IndexOfMay a s)
25157 (ElementIsInList a s)
26158
159+-- | Count elements in a list
160+type family Count (a :: k) (s :: [k]) :: N where
161+ Count a '[] = 'Z
162+ Count a (a ': as) = 'S (Count a as)
163+ Count a (b ': as) = Count a as
164+
27165-- | Constanints that first argument is a sublist of second. Reduces
28166-- to __(Elem a1 b, Elem a2 b, Elem a3 b, ...)__
29167type family SubList (a :: [k]) (b :: [k]) :: Constraint where
30168 SubList '[] bs = ()
31169 SubList (a ': as) bs = (Elem a bs, SubList as bs)
32170
171+subListId
172+ :: forall proxy l r
173+ . proxy l
174+ -> (SubList l l => r) -> r
175+subListId _ = unsafeCoerce id
176+
33177type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where
34178 NotSubList '[] bs = ()
35179 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)
36180
37−type IndexOf a s = IndexOf' 0 a s
38−
39−type family IndexOf' (acc :: Nat) (a :: k) (s :: [k]) :: Maybe Nat where
40− IndexOf' acc a '[] = 'Nothing
41− IndexOf' acc a (a ': as) = 'Just acc
42− IndexOf' acc a (b ': as) = IndexOf' (acc + 1) a as
43−
44181type IsPrefixOf a b = ( If (IsPrefixOfBool a b)
45182 (() :: Constraint)
46183 (ListIsNotPrefixOf a b)
@@ -56,15 +193,38 @@ type family IsPrefixOfBool (a :: [k]) (b :: [k]) :: Bool where
56193 IsPrefixOfBool (a ': as) (a ': bs) = IsPrefixOfBool as bs
57194 IsPrefixOfBool as bs = 'False
58195
59−type ElementIsUniq a s = If (Equal 1 (Count a s))
196+-- | Appends elements from first list to second if they are not
197+-- presented in.
198+type family Union (a :: [k]) (b :: [k]) :: [k] where
199+ Union '[] bs = bs
200+ Union (a ': as) bs = Union as (AppendUniq a bs)
201+
202+type family UnionList (l :: [[k]]) :: [k] where
203+ UnionList '[] = '[]
204+ UnionList (a ': as) = Union a (UnionList as)
205+
206+-- | Append element to list if element is not already presented in
207+type family AppendUniq (a :: k) (s :: [k]) :: [k] where
208+ AppendUniq a (a ': bs) = a ': bs
209+ AppendUniq a (b ': bs) = b ': (AppendUniq a bs)
210+ AppendUniq a '[] = '[a]
211+
212+-- | Calculates intersection between two lists. Order of elements is
213+-- taken from first list
214+type Intersect a b = (Indices (CatMaybes (IndicesOfMay a b)) b)
215+
216+-- | Removes from first list all elements occured in second
217+type family Substract (a :: [k]) (b :: [k]) :: [k] where
218+ Substract '[] b = '[]
219+ Substract a '[] = a
220+ Substract a (b ': bs) = Substract (Delete b a) bs
221+
222+-- | Checks that element 'a' occurs in a list just once
223+type ElementIsUniq a s = If (Equal (S Z) (Count a s))
60224 (() :: Constraint)
61225 (ElementIsNotUniqInList a s)
62226
63−type family Count (a :: k) (s :: [k]) :: Nat where
64− Count a '[] = 0
65− Count a (a ': as) = 1 + (Count a as)
66− Count a (b ': as) = Count a as
67−
227+-- | Checks that all elements in list are unique
68228type UniqElements a = UniqElements' a a
69229
70230type family UniqElements' (a :: [k]) (self :: [k]) :: Constraint where