@@ -1,183 +1,46 @@
11-- | Collection of type families on type lists. This module differs
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
2+-- from __Data.Singletons.Prelude.List__ because it polykinded and
3+-- works with __[*]__ as well
4+
5+module TypeFun.Data.List where
476
487import Data.Type.Bool
498import GHC.Exts
509import GHC.TypeLits
5110import TypeFun.Data.Eq
11+import TypeFun.Data.List.Internal
5212import 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)
11013
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)
14+type family Length (a :: [k]) :: Nat where
15+ Length '[] = 0
16+ Length (a ': as) = 1 + (Length as)
14917
15018-- | Generates unresolvable constraint if fists element is not
15119-- contained inside of second
152−type Elem a s = NothingToConstr (IndexOfMay a s)
20+type Elem a s = NothingToConstr (IndexOf a s)
15321 (ElementNotFoundInList a s)
15422
15523-- | Reverse of 'Elem'
156−type NotElem a s = JustToConstr (IndexOfMay a s)
24+type NotElem a s = JustToConstr (IndexOf a s)
15725 (ElementIsInList a s)
15826
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−
16527-- | Constanints that first argument is a sublist of second. Reduces
16628-- to __(Elem a1 b, Elem a2 b, Elem a3 b, ...)__
16729type family SubList (a :: [k]) (b :: [k]) :: Constraint where
16830 SubList '[] bs = ()
16931 SubList (a ': as) bs = (Elem a bs, SubList as bs)
17032
171−subListId
172− :: forall proxy l r
173− . proxy l
174− -> (SubList l l => r) -> r
175−subListId _ = unsafeCoerce id
176−
17733type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where
17834 NotSubList '[] bs = ()
17935 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)
18036
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+
18144type IsPrefixOf a b = ( If (IsPrefixOfBool a b)
18245 (() :: Constraint)
18346 (ListIsNotPrefixOf a b)
@@ -193,38 +56,15 @@ type family IsPrefixOfBool (a :: [k]) (b :: [k]) :: Bool where
19356 IsPrefixOfBool (a ': as) (a ': bs) = IsPrefixOfBool as bs
19457 IsPrefixOfBool as bs = 'False
19558
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))
59+type ElementIsUniq a s = If (Equal 1 (Count a s))
22460 (() :: Constraint)
22561 (ElementIsNotUniqInList a s)
22662
227−-- | Checks that all elements in list are unique
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+
22868type UniqElements a = UniqElements' a a
22969
23070type family UniqElements' (a :: [k]) (self :: [k]) :: Constraint where