@@ -1,6 +1,6 @@
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
2+-- from __Data.Singletons.Prelude.List__ because works with __[*]__
3+-- and relies on GHC's type equality (~)
44
55module TypeFun.Data.List where
66
@@ -62,17 +62,30 @@ type family IsPrefixOfBool (a :: [k]) (b :: [k]) :: Bool where
6262 IsPrefixOfBool (a ': as) (a ': bs) = IsPrefixOfBool as bs
6363 IsPrefixOfBool as bs = 'False
6464
65+-- | Checks that element 'a' occurs in a list just once
6566type ElementIsUniq a s = If (Equal (S Z) (Count a s))
6667 (() :: Constraint)
6768 (ElementIsNotUniqInList a s)
6869
70+-- | Count elements in a list
6971type family Count (a :: k) (s :: [k]) :: N where
7072 Count a '[] = 'Z
7173 Count a (a ': as) = 'S (Count a as)
7274 Count a (b ': as) = Count a as
7375
76+-- | Checks that all elements in list are unique
7477type UniqElements a = UniqElements' a a
7578
7679type family UniqElements' (a :: [k]) (self :: [k]) :: Constraint where
7780 UniqElements' '[] self = ()
7881 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)