A list whose length is statically known.

Type parameter n, of kind Nat, is the length of the list.

Prepend an element to a list.

'a' <:> singleton 'b' === mk2 'a' 'b'

Append two lists.

mk2 'a' 'b' <++> mk3 'c' 'd' 'e' === mk5 'a' 'b' 'c' 'd' 'e'

Length of a list.

length (mk3 'a' 'b' 'c') === 3

Head of a non-empty list.

head (mk3 'a' 'b' 'c') === 'a'

Head of a list.

headMay (empty :: NList 0 Int) === Nothing
headMay (mk3 'a' 'b' 'c') === Just 'a'

Tail of a non-empty list.

tail (singleton 'a') === empty
tail (mk3 'a' 'b' 'c') === mk2 'b' 'c'

Tail of a list. Returns an empty list if the input is empty.

tail' (empty :: NList 0 ()) === empty
tail' (singleton 'a') === empty
tail' (mk3 'a' 'b' 'c') === mk2 'b' 'c'

Tail of a list. Returns Nothing if the input is empty.

tailMay (empty :: NList 0 ()) === Nothing
tailMay (singleton 'a') === Just empty
tailMay (mk3 'a' 'b' 'c') === Just (mk2 'b' 'c')

The last element of a non-empty list.

last (mk3 'a' 'b' 'c') === 'c'

The last element of a list.

lastMay (empty :: NList 0 Int) === Nothing
lastMay (mk3 'a' 'b' 'c') === Just 'c'

All elements of a non-empty list except the last one.

init (singleton 'a') === empty
init (mk3 'a' 'b' 'c') === mk2 'a' 'b'

All elements of a list except the last one. Returns an empty list if the input is empty.

init' (empty :: NList 0 ()) === empty
init' (singleton 'a') === empty
init' (mk3 'a' 'b' 'c') === mk2 'a' 'b'

All elements of a list except the last one. Returns Nothing if the input is empty.

initMay (empty :: NList 0 ()) === Nothing
initMay (singleton 'a') === Just empty
initMay (mk3 'a' 'b' 'c') === Just (mk2 'a' 'b')

Decompose a list into head and tail.

uncons (singleton 'a') === ('a', empty)
uncons (mk3 'a' 'b' 'c') === ('a', mk2 'b' 'c')

Convert an NList into a regular list.

toList (mk3 'a' 'b' 'c') === "abc"

Return the first k elements of a list whose length is at least k.

take @0 (mk3 'a' 'b' 'c') === empty
take @2 (mk3 'a' 'b' 'c') === mk2 'a' 'b'
take @3 (mk3 'a' 'b' 'c') === mk3 'a' 'b' 'c'

Drop the first k elements of a list whose length is at least k.

drop @0 (mk3 'a' 'b' 'c') === mk3 'a' 'b' 'c'
drop @2 (mk3 'a' 'b' 'c') === singleton 'c'
drop @3 (mk3 'a' 'b' 'c') === empty

Return the first k elements, paired with the remaining elements, of a list whose length is at least k.

splitAt @0 (mk3 'a' 'b' 'c') === (empty, mk3 'a' 'b' 'c')
splitAt @2 (mk3 'a' 'b' 'c') === (mk2 'a' 'b', singleton 'c')
splitAt @3 (mk3 'a' 'b' 'c') === (mk3 'a' 'b' 'c', empty)

Return the element at index k (starting from 0) in a list with at least k+1 elements.

kth @0 (mk4 'a' 'b' 'c' 'd') === 'a'
kth @3 (mk4 'a' 'b' 'c' 'd') === 'd'

Reverse a list.

reverse (mk3 'a' 'b' 'c') === mk3 'c' 'b' 'a'

Take an element and a list, and insert the element in between elements of the list.

intersperse (',') empty === empty
intersperse (',') (singleton 'a') === singleton 'a'
intersperse (',') (mk3 'a' 'b' 'c') === mk5 'a' ',' 'b' ',' 'c'

Transpose the rows and columns of a two dimensional list.

transpose (mk2 (mk3 1 2 3) (mk3 4 5 6)) === mk3 (mk2 1 4) (mk2 2 5) (mk2 3 6)

Concatenate the sublists of a two-dimensional list.

concat (mk2 (mk3 1 2 3) (mk3 4 5 6)) === mk6 1 2 3 4 5 6

Stably sort a list.

sort (mk6 1 4 2 8 5 7) === mk6 1 2 4 5 7 8

Sort a list by applying a function to each element and comparing the results.

sortOn negate (mk6 1 4 2 8 5 7) === mk6 8 7 5 4 2 1

Non-overloaded version of sort.

sortBy (\x y -> compare (-x) (-y)) (mk6 1 4 2 8 5 7) === mk6 8 7 5 4 2 1

Zip two lists of the same length.

zip (mk2 1 2) (mk2 'a' 'b') === mk2 (1, 'a') (2, 'b')

Zip with a function.

zipWith (+) (mk2 1 2) (mk2 3 4) === mk2 4 6

Unzip a list of pairs.

unzip (mk2 (1, 'a') (2, 'b')) === ((mk2 1 2), (mk2 'a' 'b'))

Return a list containing n copies of the given element.

replicate @3 'a' === mk3 'a' 'a' 'a'

The empty list.

length empty === 0

A singleton list.

length (singleton 'a' :: NList 1 Char) === 1

toList (mk1 'a') === "a"

toList (mk2 'a' 'b') === "ab"

toList (mk3 'a' 'b' 'c') === "abc"

toList (mk4 'a' 'b' 'c' 'd') === "abcd"

toList (mk5 'a' 'b' 'c' 'd' 'e') === "abcde"

toList (mk6 'a' 'b' 'c' 'd' 'e' 'f') === "abcdef"

toList (mk7 'a' 'b' 'c' 'd' 'e' 'f' 'g') === "abcdefg"

toList (mk8 'a' 'b' 'c' 'd' 'e' 'f' 'g' 'h') === "abcdefgh"

toList (mk9 'a' 'b' 'c' 'd' 'e' 'f' 'g' 'h' 'i') === "abcdefghi"

toList (mk10 'a' 'b' 'c' 'd' 'e' 'f' 'g' 'h' 'i' 'j') === "abcdefghij"

Typeclass for converting tuples to NLists.

Typeclass for converting NLists to tuples.

The Pred type family is used to maintain the invariant that n is a KnownNat (i.e., n >= 0) for all List n a.