Copyright | (c) Artem Chirkin |
---|---|

License | BSD3 |

Safe Haskell | None |

Language | Haskell2010 |

Provides type-level operations on lists.

## Synopsis

- type (++) (as :: [k]) (bs :: [k]) = Concat as bs
- type (+:) (ns :: [k]) (n :: k) = Snoc ns n
- type (:+) (a :: k) (as :: [k]) = a ': as
- type Empty = '[] :: [k]
- type Cons (a :: k) (as :: [k]) = a ': as
- type Snoc (xs :: [k]) (x :: k) = RunList (Snoc' xs x :: List k) :: [k]
- type family Head (xs :: [k]) :: k where ...
- type family Tail (xs :: [k]) :: [k] where ...
- type family Last (xs :: [k]) :: k where ...
- type family Init (xs :: [k]) = (ys :: [k]) | ys -> k where ...
- type family Concat (as :: [k]) (bs :: [k]) :: [k] where ...
- type family StripPrefix (as :: [k]) (asbs :: [k]) :: [k] where ...
- type family StripSuffix (bs :: [k]) (asbs :: [k]) :: [k] where ...
- type Reverse (xs :: [k]) = RunList (Reverse' xs :: List k) :: [k]
- type family Take (n :: Nat) (xs :: [k]) :: [k] where ...
- type family Drop (n :: Nat) (xs :: [k]) :: [k] where ...
- type family Length (xs :: [k]) :: Nat where ...
- type family All (f :: k -> Constraint) (xs :: [k]) :: Constraint where ...
- type family Map (f :: a -> b) (xs :: [a]) :: [b] where ...
- type family UnMap (f :: a -> b) (xs :: [b]) :: [a] where ...
- type family Elem (x :: k) (xs :: [k]) :: Constraint where ...
- class (bs ~ Snoc as a, as ~ Init bs, a ~ Last bs, SnocListCtx as a bs, ConcatList as '[a] bs) => SnocList (as :: [k]) (a :: k) (bs :: [k]) | as a -> bs, bs -> as a, as -> k, a -> a, bs -> k
- class (as ~ Reverse bs, bs ~ Reverse as, ReverseList bs as, ReverseListCtx as bs) => ReverseList (as :: [k]) (bs :: [k]) | as -> bs, bs -> as, as -> k, bs -> k
- class (asbs ~ Concat as bs, as ~ StripSuffix bs asbs, bs ~ StripPrefix as asbs, ConcatListCtx1 as bs asbs, ConcatListCtx2 as bs asbs (bs == asbs)) => ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) | as bs -> asbs, as asbs -> bs, as -> k, bs -> k, asbs -> k
- inferStripSuffix :: forall as bs asbs. as ~ StripSuffix bs asbs => Dict (ConcatList as bs asbs)
- inferStripPrefix :: forall as bs asbs. bs ~ StripPrefix as asbs => Dict (ConcatList as bs asbs)
- inferConcat :: forall as bs asbs. asbs ~ Concat as bs => Dict (ConcatList as bs asbs)
- inferTypeableCons :: forall ys x xs. (Typeable ys, ys ~ (x ': xs)) => Dict (Typeable x, Typeable xs)

# Basic operations

type (++) (as :: [k]) (bs :: [k]) = Concat as bs infixr 5 Source #

Infix-style synonym for concatenation

type Cons (a :: k) (as :: [k]) = a ': as Source #

Appending a list, represents an `Op`

counterpart of `(':)`

.

type Snoc (xs :: [k]) (x :: k) = RunList (Snoc' xs x :: List k) :: [k] Source #

Appending a list on the other side (injective).

type family Head (xs :: [k]) :: k where ... Source #

Extract the first element of a list, which must be non-empty.

Head (x ': _) = x |

type family Tail (xs :: [k]) :: [k] where ... Source #

Extract the elements after the head of a list, which must be non-empty.

Tail (_ ': xs) = xs |

type family Last (xs :: [k]) :: k where ... Source #

Extract the last element of a list, which must be non-empty.

type family Init (xs :: [k]) = (ys :: [k]) | ys -> k where ... Source #

Extract all but last elements of a list, which must be non-empty.

type family StripPrefix (as :: [k]) (asbs :: [k]) :: [k] where ... Source #

Remove prefix `as`

from a list `asbs`

if `as`

is a prefix; fail otherwise.

StripPrefix as as = '[] | |

StripPrefix '[] bs = bs | |

StripPrefix (a ': as) (a ': asbs) = StripPrefix as asbs |

type family StripSuffix (bs :: [k]) (asbs :: [k]) :: [k] where ... Source #

Remove suffix `bs`

from a list `asbs`

if `bs`

is a suffix; fail otherwise.

StripSuffix '[] as = as | |

StripSuffix bs bs = '[] | |

StripSuffix bs (a ': asbs) = a ': StripSuffix bs asbs |

type Reverse (xs :: [k]) = RunList (Reverse' xs :: List k) :: [k] Source #

Reverse elements of a list (injective).

type family Take (n :: Nat) (xs :: [k]) :: [k] where ... Source #

`Take n xs`

returns the prefix of a list of length `max n (length xs)`

.

type family Drop (n :: Nat) (xs :: [k]) :: [k] where ... Source #

`Drop n xs`

drops up to `n`

elements of `xs`

.

# Operations on elements

type family All (f :: k -> Constraint) (xs :: [k]) :: Constraint where ... Source #

All elements of a type list must satisfy the same constraint.

type family Map (f :: a -> b) (xs :: [a]) :: [b] where ... Source #

Map a functor over the elements of a type list.

type family UnMap (f :: a -> b) (xs :: [b]) :: [a] where ... Source #

Unmap a functor over the elements of a type list.

type family Elem (x :: k) (xs :: [k]) :: Constraint where ... Source #

Check if an item is a member of a list.

# Classes that simplify inference of type equalities

class (bs ~ Snoc as a, as ~ Init bs, a ~ Last bs, SnocListCtx as a bs, ConcatList as '[a] bs) => SnocList (as :: [k]) (a :: k) (bs :: [k]) | as a -> bs, bs -> as a, as -> k, a -> a, bs -> k Source #

Represent a decomposition of a list by appending an element to its end.

class (as ~ Reverse bs, bs ~ Reverse as, ReverseList bs as, ReverseListCtx as bs) => ReverseList (as :: [k]) (bs :: [k]) | as -> bs, bs -> as, as -> k, bs -> k Source #

Represent two lists that are `Reverse`

of each other

#### Instances

ReverseList ('[] :: [k]) ('[] :: [k]) Source # | |

Defined in Data.Type.List.Classes |

class (asbs ~ Concat as bs, as ~ StripSuffix bs asbs, bs ~ StripPrefix as asbs, ConcatListCtx1 as bs asbs, ConcatListCtx2 as bs asbs (bs == asbs)) => ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) | as bs -> asbs, as asbs -> bs, as -> k, bs -> k, asbs -> k Source #

Represent a triple of lists forming a relation `(as ++ bs) ~ asbs`

NB: functional dependency `bs asbs -> as`

does not seem to be possible,
because dependency checking happens before constraints checking
and does not take constraints into account.

inferStripSuffix :: forall as bs asbs. as ~ StripSuffix bs asbs => Dict (ConcatList as bs asbs) Source #

Derive `ConcatList`

given `StripSuffix`

inferStripPrefix :: forall as bs asbs. bs ~ StripPrefix as asbs => Dict (ConcatList as bs asbs) Source #

Derive `ConcatList`

given `StripPrefix`

inferConcat :: forall as bs asbs. asbs ~ Concat as bs => Dict (ConcatList as bs asbs) Source #

Derive `ConcatList`

given `Concat`