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 = '[]
- type Cons (a :: k) (as :: [k]) = a ': as
- type family Snoc (xs :: [k]) (x :: k) = (ys :: [k]) where ...
- 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]) :: [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 family Reverse (xs :: [k]) :: [k] where ...
- 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 Elem (x :: k) (xs :: [k]) :: Constraint where ...
- type ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) = (asbs ~ Concat as bs, as ~ StripSuffix bs asbs, bs ~ StripPrefix as asbs)
- evStripSuffix :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]). (as ~ StripSuffix bs asbs) :- ConcatList as bs asbs
- evStripPrefix :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]). (bs ~ StripPrefix as asbs) :- ConcatList as bs asbs
- evConcat :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]). (asbs ~ Concat as bs) :- ConcatList as bs asbs
- inferTypeableCons :: forall (k :: Type) (ys :: [k]) (x :: k) (xs :: [k]). (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 family Snoc (xs :: [k]) (x :: k) = (ys :: [k]) where ... Source #

Appending a list on the other side.

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

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

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

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

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]) :: [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 '[] asbs = asbs | |

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

StripPrefix (a ': as) (b ': asbs) = TypeError ((Text "StripPrefix: the first argument is not a prefix of the second." :$$: (Text "Failed prefix: " :<>: ShowType (a ': as))) :$$: (Text "Second argument: " :<>: ShowType (b ': asbs))) | |

StripPrefix (a ': as) '[] = TypeError ((Text "StripPrefix: the first argument is longer than the second." :$$: (Text "Failed prefix: " :<>: ShowType (a ': as))) :$$: Text "The reduced second argument is empty.") |

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 bs bs = '[] | |

StripSuffix '[] asbs = asbs | |

StripSuffix (a ': bs) (b ': bs) = TypeError (Text "StripSuffix: the first argument is not a suffix of the second." :$$: (Text "Failed match: " :<>: ShowType ((a ': bs) ~ (b ': bs)))) | |

StripSuffix (b ': bs) '[] = TypeError ((Text "StripSuffix: the first argument is longer than the second." :$$: (Text "Failed suffix: " :<>: ShowType (b ': bs))) :$$: Text "The reduced second argument is empty.") | |

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

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

Returns the elements of a list in reverse order.

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 Elem (x :: k) (xs :: [k]) :: Constraint where ... Source #

Check if an item is a member of a list.

# Concatenation and its evidence

type ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) = (asbs ~ Concat as bs, as ~ StripSuffix bs asbs, bs ~ StripPrefix as asbs) Source #

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

evStripSuffix :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]). (as ~ StripSuffix bs asbs) :- ConcatList as bs asbs Source #

Derive `ConcatList`

given `StripSuffix`

evStripPrefix :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]). (bs ~ StripPrefix as asbs) :- ConcatList as bs asbs Source #

Derive `ConcatList`

given `StripPrefix`

evConcat :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]). (asbs ~ Concat as bs) :- ConcatList as bs asbs Source #

Derive `ConcatList`

given `Concat`