Safe Haskell | None |
---|---|

Language | Haskell2010 |

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

- type family Length (a :: [k]) :: N where ...
- type family Drop (c :: N) (s :: [k]) :: [k] where ...
- type family Take (c :: N) (s :: [k]) :: [k] where ...
- type family Delete (a :: k) (s :: [k]) :: [k] where ...
- type family Remove (i :: N) (a :: [k]) :: [k] where ...
- type family (a :: [k]) :++: (b :: [k]) :: [k] where ...
- type IndexOf a s = FromJust (IndexOfMay a s)
- type IndexOfMay a s = IndexOfMay' Z a s
- type family IndexOfMay' (acc :: N) (a :: k) (s :: [k]) :: Maybe N where ...
- type family IndicesOfMay (a :: [k]) (b :: [k]) :: [Maybe N] where ...
- type family IndicesOf (a :: [k]) (b :: [k]) :: [N] where ...
- type Index idx s = FromJust (IndexMay idx s)
- type family IndexMay (idx :: N) (s :: [k]) :: Maybe k where ...
- type family IndicesMay (idxs :: [N]) (a :: [k]) :: [Maybe k] where ...
- type family Indices (idxs :: [N]) (a :: [k]) :: [k] where ...
- type Elem a s = NothingToConstr (IndexOfMay a s) (ElementNotFoundInList a s)
- type NotElem a s = JustToConstr (IndexOfMay a s) (ElementIsInList a s)
- type family Count (a :: k) (s :: [k]) :: N where ...
- type family SubList (a :: [k]) (b :: [k]) :: Constraint where ...
- type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where ...
- type IsPrefixOf a b = (If (IsPrefixOfBool a b) (() :: Constraint) (ListIsNotPrefixOf a b), SubList a b)
- type IsNotPrefixOf a b = If (IsPrefixOfBool a b) (ListIsPrefixOf a b) (() :: Constraint)
- type family IsPrefixOfBool (a :: [k]) (b :: [k]) :: Bool where ...
- type family Union (a :: [k]) (b :: [k]) :: [k] where ...
- type family UnionList (l :: [[k]]) :: [k] where ...
- type family AppendUniq (a :: k) (s :: [k]) :: [k] where ...
- type Intersect a b = Indices (CatMaybes (IndicesOfMay a b)) b
- type family Substract (a :: [k]) (b :: [k]) :: [k] where ...
- type ElementIsUniq a s = If (Equal (S Z) (Count a s)) (() :: Constraint) (ElementIsNotUniqInList a s)
- type UniqElements a = UniqElements' a a
- type family UniqElements' (a :: [k]) (self :: [k]) :: Constraint where ...
- appendId :: forall proxy l r. proxy l -> (l ~ (l :++: '[]) => r) -> r
- subListId :: forall proxy l r. proxy l -> (SubList l l => r) -> r

# Primitive operations on lists

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

Remove first argument type from anywhere in a list.

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

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 #

IndicesOfMay '[] bs = '[] | |

IndicesOfMay (a ': as) bs = IndexOfMay a bs ': IndicesOfMay as bs |

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

IndicesMay '[] as = '[] | |

IndicesMay (i ': idxs) as = IndexMay i as ': IndicesMay 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`

# 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, ...)**

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

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

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.

Union '[] bs = bs | |

Union (a ': as) bs = Union as (AppendUniq a bs) |

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

Append element to list if element is not already presented in

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

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

UniqElements' '[] self = () | |

UniqElements' (a ': as) self = (ElementIsUniq a self, UniqElements' as self) |