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 :: N
- type family Drop c s :: [k]
- type family Take c s :: [k]
- type family Delete a s :: [k]
- type family Remove i a :: [k]
- type family a :++: b :: [k]
- type IndexOf a s = FromJust (IndexOfMay a s)
- type IndexOfMay a s = IndexOfMay' Z a s
- type family IndexOfMay' acc a s :: Maybe N
- type family IndicesOfMay a b :: [Maybe N]
- type family IndicesOf a b :: [N]
- type Index idx s = FromJust (IndexMay idx s)
- type family IndexMay idx s :: Maybe k
- type family IndicesMay idxs a :: [Maybe k]
- type family Indices idxs a :: [k]
- 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 s :: N
- type family SubList a b :: Constraint
- type family NotSubList a b :: Constraint
- 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 b :: Bool
- type family Union a b :: [k]
- type family UnionList l :: [k]
- type family AppendUniq a s :: [k]
- type Intersect a b = Indices (CatMaybes (IndicesOfMay a b)) b
- type family Substract a b :: [k]
- 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 self :: Constraint
- 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
Elements lookup
type IndexOf a s = FromJust (IndexOfMay a s) Source
type IndexOfMay a s = IndexOfMay' Z a s Source
type family IndexOfMay' acc a s :: Maybe N 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 b :: [Maybe N] Source
IndicesOfMay `[]` bs = `[]` | |
IndicesOfMay (a : as) bs = IndexOfMay a bs : IndicesOfMay as bs |
type family IndicesMay idxs a :: [Maybe k] 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 b :: Constraint 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 b :: Constraint 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 b :: Bool 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 b :: [k] 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 s :: [k] 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
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
UniqElements' `[]` self = () | |
UniqElements' (a : as) self = (ElementIsUniq a self, UniqElements' as self) |