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

Empty list, same as '[].

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

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

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

Appending a list on the other side (injective).

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

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

Equations

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 (_ ': xs) = xs

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

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

Equations

Last '[x] = x

Last (_ ': xs) = Last xs

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

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

Equations

Init ('[x] :: [k]) = '[] :: [k]

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

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

Append two lists.

Equations

Concat as '[] = as

Concat '[] bs = bs

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

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

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

StripSuffix bs bs = '[]

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

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

Reverse elements of a list (injective).

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 UnMap (f :: a -> b) (xs :: [b]) :: [a] where ...

Unmap a functor over the elements of a type list.

Equations

UnMap f '[] = '[]

UnMap f (f x ': ys) = x ': UnMap f ys

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

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

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

Represent two lists that are Reverse of each other

Instances

ReverseList ('[] :: [k]) ('[] :: [k])

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

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)

Derive ConcatList given StripSuffix

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

Derive ConcatList given StripPrefix

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

Derive ConcatList given Concat

Data.Typeable

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

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