Safe Haskell	None
Language	Haskell2010

TypeFun.Data.List

Contents

Primitive operations on lists
Elements lookup
Operations with lists
Set operations
Uniqueness checking
Unsafe helpers

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 IndexOf a s = FromJust (IndexOfMay a s) Source #

type IndexOfMay a s = IndexOfMay' Z a s Source #

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 #

Constanints 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 #