@@ -1,6 +1,6 @@
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 it polykinded and
2+-- from __Data.Singletons.Prelude.List__ because works with __[*]__
3−-- works with __[*]__ as well
3+-- and relies on GHC's type equality (~)
5module TypeFun.Data.List where
5module TypeFun.Data.List where
@@ -62,17 +62,30 @@ type family IsPrefixOfBool (a :: [k]) (b :: [k]) :: Bool where
62 IsPrefixOfBool (a ': as) (a ': bs) = IsPrefixOfBool as bs
62 IsPrefixOfBool (a ': as) (a ': bs) = IsPrefixOfBool as bs
63 IsPrefixOfBool as bs = 'False
63 IsPrefixOfBool as bs = 'False
65+-- | Checks that element 'a' occurs in a list just once
65type ElementIsUniq a s = If (Equal (S Z) (Count a s))
66type ElementIsUniq a s = If (Equal (S Z) (Count a s))
66 (() :: Constraint)
67 (() :: Constraint)
67 (ElementIsNotUniqInList a s)
68 (ElementIsNotUniqInList a s)
70+-- | Count elements in a list
69type family Count (a :: k) (s :: [k]) :: N where
71type family Count (a :: k) (s :: [k]) :: N where
70 Count a '[] = 'Z
72 Count a '[] = 'Z
71 Count a (a ': as) = 'S (Count a as)
73 Count a (a ': as) = 'S (Count a as)
72 Count a (b ': as) = Count a as
74 Count a (b ': as) = Count a as
76+-- | Checks that all elements in list are unique
74type UniqElements a = UniqElements' a a
77type UniqElements a = UniqElements' a a
76type family UniqElements' (a :: [k]) (self :: [k]) :: Constraint where
79type family UniqElements' (a :: [k]) (self :: [k]) :: Constraint where
77 UniqElements' '[] self = ()
80 UniqElements' '[] self = ()
78 UniqElements' (a ': as) self = (ElementIsUniq a self, UniqElements' as self)
81 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)