type-fun-0.1.3: Collection of widely reimplemented type families

TypeFun.Data.List

Description

Collection of type families on type lists. This module differs from Data.Singletons.Prelude.List because works with [*] and relies on GHC's type equality (~). The rest of required operations like Reverse or (:++:) you could find in singletons

Synopsis

Primitive operations on lists

type family Length (a :: [k]) :: N where ... Source #

Equations

 Length '[] = 'Z Length (a ': as) = 'S (Length as)

type family Drop (c :: N) (s :: [k]) :: [k] where ... Source #

Equations

 Drop 'Z s = s Drop ('S c) '[] = '[] Drop ('S c) (a ': as) = Drop c as

type family Take (c :: N) (s :: [k]) :: [k] where ... Source #

Equations

 Take 'Z s = '[] Take ('S c) '[] = '[] Take ('S c) (a ': as) = a ': Take c as

type family Delete (a :: k) (s :: [k]) :: [k] where ... Source #

Remove first argument type from anywhere in a list.

Equations

 Delete a '[] = '[] Delete a (a ': as) = Delete a as Delete a (b ': as) = b ': Delete a as

type family Remove (i :: N) (a :: [k]) :: [k] where ... Source #

Remove index from the list

Equations

 Remove i '[] = '[] Remove 'Z (a ': as) = as Remove ('S i) (a ': as) = a ': Remove i as

type family (a :: [k]) :++: (b :: [k]) :: [k] where ... Source #

Equations

 '[] :++: b = b (a ': as) :++: b = a ': (as :++: b)

Elements lookup

type family IndexOfMay' (acc :: N) (a :: k) (s :: [k]) :: Maybe N where ... Source #

Equations

 IndexOfMay' acc a '[] = 'Nothing IndexOfMay' acc a (a ': as) = 'Just acc IndexOfMay' acc a (b ': as) = IndexOfMay' (S acc) a as

type family IndicesOfMay (a :: [k]) (b :: [k]) :: [Maybe N] where ... Source #

Equations

 IndicesOfMay '[] bs = '[] IndicesOfMay (a ': as) bs = IndexOfMay a bs ': IndicesOfMay as bs

type family IndicesOf (a :: [k]) (b :: [k]) :: [N] where ... Source #

Equations

 IndicesOf '[] bs = '[] IndicesOf (a ': as) bs = IndexOf a bs ': IndicesOf as bs

type Index idx s = FromJust (IndexMay idx s) Source #

type family IndexMay (idx :: N) (s :: [k]) :: Maybe k where ... Source #

Equations

 IndexMay idx '[] = 'Nothing IndexMay Z (a ': as) = 'Just a IndexMay (S idx) (a ': as) = IndexMay idx as

type family IndicesMay (idxs :: [N]) (a :: [k]) :: [Maybe k] where ... Source #

Equations

 IndicesMay '[] as = '[] IndicesMay (i ': idxs) as = IndexMay i as ': IndicesMay idxs as

type family Indices (idxs :: [N]) (a :: [k]) :: [k] where ... Source #

Equations

 Indices '[] as = '[] Indices (i ': idxs) as = Index i as ': Indices idxs as

type Elem a s = NothingToConstr (IndexOfMay a s) (ElementNotFoundInList a s) Source #

Generates unresolvable constraint if fists element is not contained inside of second

type NotElem a s = JustToConstr (IndexOfMay a s) (ElementIsInList a s) Source #

Reverse of Elem

type family Count (a :: k) (s :: [k]) :: N where ... Source #

Count elements in a list

Equations

 Count a '[] = 'Z Count a (a ': as) = 'S (Count a as) Count a (b ': as) = Count a as

Operations with lists

type family SubList (a :: [k]) (b :: [k]) :: Constraint where ... Source #

Constrains that first argument is a sublist of second. Reduces to (Elem a1 b, Elem a2 b, Elem a3 b, ...)

Equations

 SubList '[] bs = () SubList (a ': as) bs = (Elem a bs, SubList as bs)

type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where ... Source #

Equations

 NotSubList '[] bs = () NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)

type IsPrefixOf a b = (If (IsPrefixOfBool a b) (() :: Constraint) (ListIsNotPrefixOf a b), SubList a b) Source #

type IsNotPrefixOf a b = If (IsPrefixOfBool a b) (ListIsPrefixOf a b) (() :: Constraint) Source #

type family IsPrefixOfBool (a :: [k]) (b :: [k]) :: Bool where ... Source #

First argument is prefix of second

Equations

 IsPrefixOfBool '[] b = 'True IsPrefixOfBool (a ': as) (a ': bs) = IsPrefixOfBool as bs IsPrefixOfBool as bs = 'False

Set operations

type family Union (a :: [k]) (b :: [k]) :: [k] where ... Source #

Appends elements from first list to second if they are not presented in.

Equations

 Union '[] bs = bs Union (a ': as) bs = Union as (AppendUniq a bs)

type family UnionList (l :: [[k]]) :: [k] where ... Source #

Equations

 UnionList '[] = '[] UnionList (a ': as) = Union a (UnionList as)

type family AppendUniq (a :: k) (s :: [k]) :: [k] where ... Source #

Append element to list if element is not already presented in

Equations

 AppendUniq a (a ': bs) = a ': bs AppendUniq a (b ': bs) = b ': AppendUniq a bs AppendUniq a '[] = '[a]

type Intersect a b = Indices (CatMaybes (IndicesOfMay a b)) b Source #

Calculates intersection between two lists. Order of elements is taken from first list

type family Substract (a :: [k]) (b :: [k]) :: [k] where ... Source #

Removes from first list all elements occured in second

Equations

 Substract '[] b = '[] Substract a '[] = a Substract a (b ': bs) = Substract (Delete b a) bs

Uniqueness checking

type ElementIsUniq a s = If (Equal (S Z) (Count a s)) (() :: Constraint) (ElementIsNotUniqInList a s) Source #

Checks that element a occurs in a list just once

type UniqElements a = UniqElements' a a Source #

Checks that all elements in list are unique

type family UniqElements' (a :: [k]) (self :: [k]) :: Constraint where ... Source #

Equations

 UniqElements' '[] self = () UniqElements' (a ': as) self = (ElementIsUniq a self, UniqElements' as self)

Unsafe helpers

appendId :: forall proxy l r. proxy l -> (l ~ (l :++: '[]) => r) -> r Source #

subListId :: forall proxy l r. proxy l -> (SubList l l => r) -> r Source #