Data.Type.List

Provides type-level operations on lists.

Basic operations

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

Infix-style synonym for concatenation

type (+:) (ns :: [k]) (n :: k) = Snoc ns n infixl 6

Synonym for a type-level Snoc.

type (:+) (a :: k) (as :: [k]) = a ': as infixr 5

Synonym for a type-level Cons.

type Empty = '[]

Empty list, same as '[].

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

Appending a list, represents an Op counterpart of (':).

type family Snoc (xs :: [k]) (x :: k) = (ys :: [k]) where ...

Appending a list on the other side.

Equations

Snoc (x ': xs) y = x ': Snoc xs y

Snoc '[] y = '[y]

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

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

Equations

Head ('[] :: [k]) = TypeError (ListError k "Head: empty type-level list.")

Head (x ': _) = x

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

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

Equations

Tail ('[] :: [k]) = TypeError (ListError k "Tail: empty type-level list.")

Tail (_ ': xs) = xs

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

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

Equations

Last ('[] :: [k]) = TypeError (ListError k "Last: empty type-level list.")

Last '[x] = x

Last (_ ': xs) = Last xs

type family Init (xs :: [k]) :: [k] where ...

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

Equations

Init ('[] :: [k]) = TypeError (ListError k "Init: empty type-level list.")

Init '[x] = '[]

Init (x ': xs) = x ': Init xs

type family Concat (as :: [k]) (bs :: [k]) :: [k] where ...

Append two lists.

Equations

Concat '[] bs = bs

Concat as '[] = as

Concat (a ': as) bs = a ': Concat as bs

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

Remove prefix as from a list asbs if as is a prefix; fail otherwise.

Equations

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

Remove suffix bs from a list asbs if bs is a suffix; fail otherwise.

Equations

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

Returns the elements of a list in reverse order.

Equations

Reverse '[] = '[]

Reverse (x ': xs) = Snoc (Reverse xs) x

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

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

Equations

Take 0 _ = '[]

Take n (x ': xs) = x ': Take (n - 1) xs

Take _ '[] = '[]

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

Drop n xs drops up to n elements of xs.

Equations

Drop 0 xs = xs

Drop n (_ ': xs) = Drop (n - 1) xs

Drop _ '[] = '[]

type family Length (xs :: [k]) :: Nat where ...

Number of elements in a list.

Equations

Length '[] = 0

Length (x ': xs) = Length xs + 1

Operations on elements

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

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

Equations

All _ '[] = ()

All f (x ': xs) = (f x, All f xs)

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

Map a functor over the elements of a type list.

Equations

Map f '[] = '[]

Map f (x ': xs) = f x ': Map f xs

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

Check if an item is a member of a list.

Equations

Elem x (x ': xs) = ()

Elem x (_ ': xs) = Elem x xs

Concatenation and its evidence

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

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

Derive ConcatList given StripSuffix

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

Derive ConcatList given StripPrefix

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

Derive ConcatList given Concat

Data.Typeable

inferTypeableCons :: forall (k :: Type) (ys :: [k]) (x :: k) (xs :: [k]). (Typeable ys, ys ~ (x ': xs)) => Dict (Typeable x, Typeable xs)

Given a Typeable list, infer this constraint for its parts.