type-fun-0.0.1: 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 :: N Source

Equations

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

type family Drop c s :: [k] Source

Equations

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

type family Take c s :: [k] Source

Equations

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

type family Delete a s :: [k] 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 a :: [k] 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 :++: b :: [k] Source

Equations

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

# Elements lookup

type family IndexOfMay' acc a s :: Maybe N 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 b :: [Maybe N] Source

Equations

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

type family IndicesOf a b :: [N] 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 s :: Maybe k Source

Equations

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

type family IndicesMay idxs a :: [Maybe k] Source

Equations

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

type family Indices idxs a :: [k] 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 s :: N 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 b :: Constraint 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 b :: Constraint 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 b :: Bool 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 b :: [k] 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] Source

Equations

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

type family AppendUniq a s :: [k] 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

# 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 self :: Constraint Source

Equations

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