@@ -1,21 +1,96 @@
1-- | Collection of type families on type lists. This module differs
1-- | Collection of type families on type lists. This module differs
2-- from __Data.Singletons.Prelude.List__ because works with __[*]__
2-- from __Data.Singletons.Prelude.List__ because works with __[*]__
3−-- and relies on GHC's type equality (~)
3+-- and relies on GHC's type equality (~). The rest of required
4−
4+-- operations like 'Reverse' or '(:++:)' you could find in singletons
5−module TypeFun.Data.List where
6+module TypeFun.Data.List
7+ ( -- * Primitive operations on lists
19+ -- * Operations with lists
25+ -- * Uniqueness checking
7import Data.Type.Bool
31import Data.Type.Bool
8import GHC.Exts
32import GHC.Exts
9import GHC.TypeLits
33import GHC.TypeLits
10import TypeFun.Data.Eq
34import TypeFun.Data.Eq
11−import TypeFun.Data.List.Errors
12import TypeFun.Data.Maybe
35import TypeFun.Data.Maybe
13import TypeFun.Data.Peano
36import TypeFun.Data.Peano
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 --
44+------------------------------------------------------------------------
46+class ElementNotFoundInList a s
48+class ElementIsInList a s
50+class ListIsNotPrefixOf a b
52+class ListIsPrefixOf a b
54+class ElementIsNotUniqInList a s
56+----------------------
57+-- main module code --
58+----------------------
15type family Length (a :: [k]) :: N where
61type family Length (a :: [k]) :: N where
16 Length '[] = 'Z
62 Length '[] = 'Z
17 Length (a ': as) = 'S (Length as)
63 Length (a ': as) = 'S (Length as)
65+type family Drop (c :: N) (s :: [k]) :: [k] where
67+ Drop ('S c) '[] = '[]
68+ Drop ('S c) (a ': as) = Drop c as
70+type family Take (c :: N) (s :: [k]) :: [k] where
72+ Take ('S c) '[] = '[]
73+ Take ('S c) (a ': as) = a ': (Take c as)
75+-- | Remove first argument type from anywhere in a list.
76+type family Delete (a :: k) (s :: [k]) :: [k] where
78+ Delete a (a ': as) = Delete a as
79+ Delete a (b ': as) = b ': (Delete a as)
81+type IndexOf a s = IndexOf' Z a s
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
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
19-- | Generates unresolvable constraint if fists element is not
94-- | Generates unresolvable constraint if fists element is not
20-- contained inside of second
95-- contained inside of second
21type Elem a s = NothingToConstr (IndexOf a s)
96type Elem a s = NothingToConstr (IndexOf a s)
@@ -25,6 +100,12 @@ type Elem a s = NothingToConstr (IndexOf a s)
25type NotElem a s = JustToConstr (IndexOf a s)
100type NotElem a s = JustToConstr (IndexOf a s)
26 (ElementIsInList a s)
101 (ElementIsInList a s)
103+-- | Count elements in a list
104+type family Count (a :: k) (s :: [k]) :: N where
106+ Count a (a ': as) = 'S (Count a as)
107+ Count a (b ': as) = Count a as
28-- | Constanints that first argument is a sublist of second. Reduces
109-- | Constanints that first argument is a sublist of second. Reduces
29-- to __(Elem a1 b, Elem a2 b, Elem a3 b, ...)__
110-- to __(Elem a1 b, Elem a2 b, Elem a3 b, ...)__
30type family SubList (a :: [k]) (b :: [k]) :: Constraint where
111type family SubList (a :: [k]) (b :: [k]) :: Constraint where
@@ -35,18 +116,6 @@ type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where
35 NotSubList '[] bs = ()
116 NotSubList '[] bs = ()
36 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)
117 NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)
38−type IndexOf a s = IndexOf' Z a s
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
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
50type IsPrefixOf a b = ( If (IsPrefixOfBool a b)
119type IsPrefixOf a b = ( If (IsPrefixOfBool a b)
51 (() :: Constraint)
120 (() :: Constraint)
52 (ListIsNotPrefixOf a b)
121 (ListIsNotPrefixOf a b)
@@ -67,11 +136,6 @@ type ElementIsUniq a s = If (Equal (S Z) (Count a s))
67 (() :: Constraint)
136 (() :: Constraint)
68 (ElementIsNotUniqInList a s)
137 (ElementIsNotUniqInList a s)
70−-- | Count elements in a list
71−type family Count (a :: k) (s :: [k]) :: N where
73− Count a (a ': as) = 'S (Count a as)
74− Count a (b ': as) = Count a as
76-- | Checks that all elements in list are unique
140-- | Checks that all elements in list are unique
77type UniqElements a = UniqElements' a a
141type UniqElements a = UniqElements' a a
@@ -79,18 +143,3 @@ type UniqElements a = UniqElements' a a
79type family UniqElements' (a :: [k]) (self :: [k]) :: Constraint where
143type family UniqElements' (a :: [k]) (self :: [k]) :: Constraint where
80 UniqElements' '[] self = ()
144 UniqElements' '[] self = ()
81 UniqElements' (a ': as) self = (ElementIsUniq a self, UniqElements' as self)
145 UniqElements' (a ': as) self = (ElementIsUniq a self, UniqElements' as self)
83−type family Drop (c :: N) (s :: [k]) :: [k] where
85− Drop ('S c) '[] = '[]
86− Drop ('S c) (a ': as) = Drop c as
88−type family Take (c :: N) (s :: [k]) :: [k] where
90− Take ('S c) '[] = '[]
91− Take ('S c) (a ': as) = a ': (Take c as)
93−type family Delete (a :: k) (s :: [k]) :: [k] where
95− Delete a (a ': as) = Delete a as
96− Delete a (b ': as) = b ': (Delete a as)