@@ -1,21 +1,96 @@
11-- | Collection of type families on type lists. This module differs
22-- from __Data.Singletons.Prelude.List__ because works with __[*]__
3−-- and relies on GHC's type equality (~)
4−
5−module TypeFun.Data.List where
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+ -- * Elements lookup
13+ , IndexOf
14+ , IndexOf'
15+ , Index
16+ , Elem
17+ , NotElem
18+ , Count
19+ -- * Operations with lists
20+ , SubList
21+ , NotSubList
22+ , IsPrefixOf
23+ , IsNotPrefixOf
24+ , IsPrefixOfBool
25+ -- * Uniqueness checking
26+ , ElementIsUniq
27+ , UniqElements
28+ , UniqElements'
29+ ) where
630
731import Data.Type.Bool
832import GHC.Exts
933import GHC.TypeLits
1034import TypeFun.Data.Eq
11−import TypeFun.Data.List.Errors
1235import TypeFun.Data.Maybe
1336import TypeFun.Data.Peano
1437
38+------------------------------------------------------------------------
39+-- NOTE: Errors type classes. These type classes are not in separate --
40+-- module because in this case user could import them and instantiate --
41+-- by mistake. The name of typeclass is an error message in fact. We --
42+-- have not any way to fail constraint explicitly, so this hack was --
43+-- introduced. --
44+------------------------------------------------------------------------
45+
46+class ElementNotFoundInList a s
47+
48+class ElementIsInList a s
49+
50+class ListIsNotPrefixOf a b
51+
52+class ListIsPrefixOf a b
53+
54+class ElementIsNotUniqInList a s
55+
56+----------------------
57+-- main module code --
58+----------------------
59+
60+
1561type family Length (a :: [k]) :: N where
1662 Length '[] = 'Z
1763 Length (a ': as) = 'S (Length as)
1864
65+type family Drop (c :: N) (s :: [k]) :: [k] where
66+ Drop 'Z s = s
67+ Drop ('S c) '[] = '[]
68+ Drop ('S c) (a ': as) = Drop c as
69+
70+type family Take (c :: N) (s :: [k]) :: [k] where
71+ Take 'Z s = '[]
72+ Take ('S c) '[] = '[]
73+ Take ('S c) (a ': as) = a ': (Take c as)
74+
75+-- | Remove first argument type from anywhere in a list.
76+type family Delete (a :: k) (s :: [k]) :: [k] where
77+ Delete a '[] = '[]
78+ Delete a (a ': as) = Delete a as
79+ Delete a (b ': as) = b ': (Delete a as)
80+
81+type IndexOf a s = IndexOf' Z a s
82+
83+type family IndexOf' (acc :: N) (a :: k) (s :: [k]) :: Maybe N where
84+ IndexOf' acc a '[] = 'Nothing
85+ IndexOf' acc a (a ': as) = 'Just acc
86+ IndexOf' acc a (b ': as) = IndexOf' (S acc) a as
87+
88+type family Index (idx :: N) (s :: [k]) :: Maybe k where
89+ Index idx '[] = 'Nothing
90+ Index Z (a ': as) = 'Just a
91+ Index (S idx) (a ': as) = Index idx as
92+
93+
1994-- | Generates unresolvable constraint if fists element is not
2095-- contained inside of second
2196type Elem a s = NothingToConstr (IndexOf a s)
@@ -25,6 +100,12 @@ type Elem a s = NothingToConstr (IndexOf a s)
25100type NotElem a s = JustToConstr (IndexOf a s)
26101 (ElementIsInList a s)
27102
103+-- | Count elements in a list
104+type family Count (a :: k) (s :: [k]) :: N where
105+ Count a '[] = 'Z
106+ Count a (a ': as) = 'S (Count a as)
107+ Count a (b ': as) = Count a as
108+
28109-- | Constanints that first argument is a sublist of second. Reduces
29110-- to __(Elem a1 b, Elem a2 b, Elem a3 b, ...)__
30111type family SubList (a :: [k]) (b :: [k]) :: Constraint where
@@ -35,18 +116,6 @@ type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where
35116 NotSubList '[] bs = ()
36117 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)
37118
38−type IndexOf a s = IndexOf' Z a s
39−
40−type family IndexOf' (acc :: N) (a :: k) (s :: [k]) :: Maybe N where
41− IndexOf' acc a '[] = 'Nothing
42− IndexOf' acc a (a ': as) = 'Just acc
43− IndexOf' acc a (b ': as) = IndexOf' (S acc) a as
44−
45−type family Index (idx :: N) (s :: [k]) :: Maybe k where
46− Index idx '[] = 'Nothing
47− Index Z (a ': as) = 'Just a
48− Index (S idx) (a ': as) = Index idx as
49−
50119type IsPrefixOf a b = ( If (IsPrefixOfBool a b)
51120 (() :: Constraint)
52121 (ListIsNotPrefixOf a b)
@@ -67,11 +136,6 @@ type ElementIsUniq a s = If (Equal (S Z) (Count a s))
67136 (() :: Constraint)
68137 (ElementIsNotUniqInList a s)
69138
70−-- | Count elements in a list
71−type family Count (a :: k) (s :: [k]) :: N where
72− Count a '[] = 'Z
73− Count a (a ': as) = 'S (Count a as)
74− Count a (b ': as) = Count a as
75139
76140-- | Checks that all elements in list are unique
77141type UniqElements a = UniqElements' a a
@@ -79,18 +143,3 @@ type UniqElements a = UniqElements' a a
79143type family UniqElements' (a :: [k]) (self :: [k]) :: Constraint where
80144 UniqElements' '[] self = ()
81145 UniqElements' (a ': as) self = (ElementIsUniq a self, UniqElements' as self)
82−
83−type family Drop (c :: N) (s :: [k]) :: [k] where
84− Drop 'Z s = s
85− Drop ('S c) '[] = '[]
86− Drop ('S c) (a ': as) = Drop c as
87−
88−type family Take (c :: N) (s :: [k]) :: [k] where
89− Take 'Z s = '[]
90− Take ('S c) '[] = '[]
91− Take ('S c) (a ': as) = a ': (Take c as)
92−
93−type family Delete (a :: k) (s :: [k]) :: [k] where
94− Delete a '[] = '[]
95− Delete a (a ': as) = Delete a as
96− Delete a (b ': as) = b ': (Delete a as)