Data.Vect

(++) : (xs : Vect m elem) -> (ys : Vect n elem) -> Vect (m + n) elem

Append two vectors

[1,2,3,4] ++ [5,6]

Fixity

Left associative, precedence 7

data Elem : a -> Vect k a -> Type

A proof that some element is found in a vector

Here : Elem x (x :: xs)

There : (later : Elem x xs) -> Elem x (y :: xs)

data Vect : (len : Nat) -> (elem : Type) -> Type

Vectors: Generic lists with explicit length in the type

len

the length of the list

elem

the type of elements

Nil : Vect 0 elem

Empty vector

(::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem

A non-empty vector of length S len, consisting of a head element and
the rest of the list, of length len.

Fixity

Left associative, precedence 7

catMaybes : Vect n (Maybe elem) -> (p : Nat ** Vect p elem)

Filter out Nothings from Vect

catMaybes [Just 1, Just 2, Nothing, Nothing, Just 5]

concat : (xss : Vect m (Vect n elem)) -> Vect (m * n) elem

Flatten a vector of equal-length vectors

concat [[1,2,3], [4,5,6]]

delete : Eq elem => elem -> Vect len elem -> (p : Nat ** Vect p elem)

Delete first element from list equal to the given one

delete 2 (fromList [1,2,2,3,4,4])

deleteAt : Fin (S len) -> Vect (S len) elem -> Vect len elem

Construct a new vector consisting of all but the indicated element

deleteAt 1 [1,2,3,4]

deleteBy : (elem -> elem -> Bool) -> elem -> Vect len elem -> (p : Nat ** Vect p elem)

Delete first element from list according to some test

deleteBy (<) 3 (fromList [1,2,2,3,4,4])

diag : Vect len (Vect len elem) -> Vect len elem

Get diagonal elements

diag [[1,2,3], [4,5,6], [7,8,9]]

drop : (n : Nat) -> Vect (n + m) elem -> Vect m elem

Remove the first n elements of a Vect

n

the number of elements to remove

drop 2 [1,2,3,4]

dropDrop : (n : Nat) -> (m : Nat) -> (xs : Vect (n + m + l) a) -> (ys : Vect (n + (m + l)) a) -> xs ~=~ ys -> drop (n + m) xs = drop m (drop n ys)

drop (n + m) = drop m . drop n

dropElem : (xs : Vect (S k) t) -> (p : Elem x xs) -> Vect k t

Remove the element at the given position.

xs

The vector to be removed from

p

A proof that the element to be removed is in the vector

dropPrefix : (ns : Vect n a) -> (ms : Vect m a) -> drop n (ns ++ ms) = ms

Adding a prefix and then dropping the prefix does nothing. Or,
adding a suffix and then taking the suffix gets the suffix.

dropTakeTakeDrop : (n : Nat) -> (m : Nat) -> (xs : Vect (n + m + l) a) -> (ys : Vect (n + (m + l)) a) -> xs ~=~ ys -> drop n (take (n + m) xs) = take m (drop n ys)

drop n . take (n + m) = take m . drop n.

Or: there are two ways to extract a subsequence.

dropUpto : (x : Nat) -> Vect n elem -> Vect (minus n (minimum x n)) elem

Drop up to the first n elements of a Vect if they exist.

n

the maximum number of elements to remove.

dropUpto 10 [1,2,3,4]

dropWhile : (p : elem -> Bool) -> Vect len elem -> (q : Nat ** Vect q elem)

Remove the longest prefix of a Vect such that all removed elements satisfy some
Boolean predicate.

p

the predicate

dropWhile (<3) [1,2,3,4]

elem : Eq elem => (x : elem) -> (xs : Vect len elem) -> Bool

Use the default Boolean equality on elements to search for an item

x

what to search for

xs

where to search

elem 3 [1,2,3,4]

elemBy : (p : elem -> elem -> Bool) -> (e : elem) -> (xs : Vect len elem) -> Bool

Search for an item using a user-provided test

p

the equality test

e

the item to search for

xs

the vector to search in

elemBy (==) 2 [1,2,3,4]

elemIndex : Eq elem => elem -> Vect m elem -> Maybe (Fin m)

Find the index of the first element of the vector equal to the given one.

elemIndex 3 [1,2,3,4]

elemIndexBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> Maybe (Fin m)

Find the index of the first element of the vector that satisfies some test

elemIndexBy (==) 3 [1,2,3,4]

elemIndices : Eq elem => elem -> Vect m elem -> List (Fin m)

Find the indices of all elements uquals to the given one

elemIndices 3 [1,2,3,4,3]

elemIndicesBy : (elem -> elem -> Bool) -> elem -> Vect m elem -> List (Fin m)

Find the indices of all elements that satisfy some test

elemIndicesBy (<=) 3 [1,2,3,4]

exactLength : (len : Nat) -> (xs : Vect m a) -> Maybe (Vect len a)

If the given Vect is the required length, return a Vect with that
length in its type, otherwise return Nothing

len

the required length

xs

the vector with the desired length

filter : (elem -> Bool) -> Vect len elem -> (p : Nat ** Vect p elem)

Find all elements of a vector that satisfy some test

filter (< 3) (fromList [1,2,3,4])

find : (p : elem -> Bool) -> (xs : Vect len elem) -> Maybe elem

Find the first element of the vector that satisfies some test

p

the test to satisfy

find (== 3) [1,2,3,4]

findIndex : (elem -> Bool) -> Vect len elem -> Maybe (Fin len)

Find the index of the first element of the vector that satisfies some test

findIndex (== 3) [1,2,3,4]

findIndices : (elem -> Bool) -> Vect m elem -> List (Fin m)

Find the indices of all elements that satisfy some test

findIndices (< 3) [1,2,3,4]

foldl1 : (t -> t -> t) -> Vect (S n) t -> t

Foldl without seeding the accumulator

foldl1 (-) (fromList [1,2,3])

foldr1 : (t -> t -> t) -> Vect (S n) t -> t

Foldr without seeding the accumulator

foldr1 (-) (fromList [1,2,3])

foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc

fromList : (l : List elem) -> Vect (length l) elem

Convert a list to a vector.

The length of the list should be statically known.

fromList [1,2,3,4]

fromList' : Vect len elem -> (l : List elem) -> Vect (length l + len) elem

hasAny : Eq elem => Vect m elem -> Vect len elem -> Bool

Check if any element of xs is found in elems using the default Boolean equality test

hasAny [2,5] [1,2,3,4]

hasAnyBy : (p : elem -> elem -> Bool) -> (elems : Vect m elem) -> (xs : Vect len elem) -> Bool

Check if any element of xs is found in elems by a user-provided comparison

p

the comparison operator

elems

the vector to search

xs

what to search for

hasAnyBy (==) [2,5] [1,2,3,4]

head : Vect (S len) elem -> elem

Only the first element of the vector

head [1,2,3,4]

index : Fin len -> Vect len elem -> elem

Extract a particular element from a vector

index 1 [1,2,3,4]

indexReplicate : (x : a) -> (n : Nat) -> (i : Fin n) -> index i (replicate n x) = x

indexTranspose : (x : Fin o) -> (y : Fin i) -> (xss : Vect o (Vect i a)) -> index y (index x xss) = index x (index y (transpose xss))

indexZipWith : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> (i : Fin n) -> index i (zipWith f as bs) = f (index i as) (index i bs)

init : Vect (S len) elem -> Vect len elem

All but the last element of the vector

init [1,2,3,4]

insertAt : Fin (S len) -> elem -> Vect len elem -> Vect (S len) elem

Insert an element at a particular index

insertAt 1 8 [1,2,3,4]

intersperse : (sep : elem) -> (xs : Vect len elem) -> Vect (len + pred len) elem

Alternate an element between the other elements of a vector

sep

the element to intersperse

xs

the vector to separate with sep

intersperse 0 [1,2,3,4]

isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)

A decision procedure for Elem

isPrefixOf : Eq elem => Vect m elem -> Vect len elem -> Bool

Verify vector prefix

isPrefixOf (fromList [1,2]) (fromList [1,2,3,4])

isPrefixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool

Verify vector prefix

isPrefixOfBy (==) (fromList [1,2]) (fromList [1,2,3,4])

isSuffixOf : Eq elem => Vect m elem -> Vect len elem -> Bool

Verify vector suffix

isSuffixOf (fromList [3,4]) (fromList [1,2,3,4])

isSuffixOfBy : (elem -> elem -> Bool) -> Vect m elem -> Vect len elem -> Bool

Verify vector suffix

isSuffixOfBy (==) (fromList [3,4]) (fromList [1,2,3,4])

last : Vect (S len) elem -> elem

The last element of the vector

last [1,2,3,4]

length : (xs : Vect len elem) -> Nat

Calculate the length of a Vect.

Note: this is only useful if you don't already statically know the length
and you want to avoid matching the implicit argument for erasure reasons.

len

the length (provably equal to the return value)

xs

the vector

lookup : Eq key => key -> Vect n (key, val) -> Maybe val

Find the assocation of some key using the default Boolean equality test

lookup 3 [(1, 'a'), (2, 'b'), (3, 'c')]

lookupBy : (p : key -> key -> Bool) -> (e : key) -> (xs : Vect n (key, val)) -> Maybe val

Find the association of some key with a user-provided comparison

p

the comparison operator for keys (True if they match)

e

the key to look for

lookupBy (==) 2 [(1, 'a'), (2, 'b'), (3, 'c')]

mapElem : Elem x xs -> Elem (f x) (map f xs)

mapMaybe : (f : a -> Maybe b) -> (xs : Vect len a) -> (m : Nat ** Vect m b)

Map a partial function across a vector, returning those elements for which
the function had a value.

The first projection of the resulting pair (ie the length) will always be
at most the length of the input vector. This is not, however, guaranteed
by the type.

f

the partial function (expressed by returning Maybe)

xs

the vector to check for results

mapMaybe ((find (=='a')) . unpack) (fromList ["abc","ade","bgh","xyz"])

maybeToVect : Maybe elem -> (p : Nat ** Vect p elem)

Convert Maybe type into Vect

maybeToVect (Just 2)

merge : Ord elem => Vect n elem -> Vect m elem -> Vect (n + m) elem

mergeBy : (elem -> elem -> Ordering) -> (xs : Vect n elem) -> (ys : Vect m elem) -> Vect (n + m) elem

Merge two ordered vectors

mergeBy compare (fromList [1,3,5]) (fromList [2,3,4,5,6])

neitherHereNorThere : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))

An item not in the head and not in the tail is not in the Vect at all

noEmptyElem : Elem x [] -> Void

Nothing can be in an empty Vect

nub : Eq elem => Vect len elem -> (p : Nat ** Vect p elem)

Make the elements of some vector unique by the default Boolean equality

nub (fromList [1,2,2,3,4,4])

nubBy : (elem -> elem -> Bool) -> Vect len elem -> (p : Nat ** Vect p elem)

Make the elements of some vector unique by some test

nubBy (==) (fromList [1,2,2,3,4,4])

overLength : (len : Nat) -> (xs : Vect m a) -> Maybe (p : Nat ** Vect (plus p len) a)

If the given Vect is at least the required length, return a Vect with
at least that length in its type, otherwise return Nothing

len

the required length

xs

the vector with the desired length

partition : (elem -> Bool) -> Vect len elem -> ((p : Nat ** Vect p elem), (q : Nat ** Vect q elem))

A tuple where the first element is a Vect of the n elements passing given test
and the second element is a Vect of the remaining elements of the original.

partition (== 2) (fromList [1,2,3,2,4])

range : Vect len (Fin len)

replaceAt : Fin len -> elem -> Vect len elem -> Vect len elem

Replace an element at a particlar index with another

replaceAt 1 8 [1,2,3,4]

replaceByElem : (xs : Vect k t) -> Elem x xs -> t -> Vect k t

replaceElem : (xs : Vect k t) -> Elem x xs -> (y : t) -> (ys : Vect k t ** Elem y ys)

replicate : (len : Nat) -> (x : elem) -> Vect len elem

Repeat some value some number of times.

len

the number of times to repeat it

x

the value to repeat

replicate 4 1

reverse : Vect len elem -> Vect len elem

Reverse the order of the elements of a vector

reverse [1,2,3,4]

scanl : (res -> elem -> res) -> res -> Vect len elem -> Vect (S len) res

The scanl function is similar to foldl, but returns all the intermediate
accumulator states in the form of a vector.

scanl (-) 0 (fromList [1,2,3])

scanl1 : (elem -> elem -> elem) -> Vect len elem -> Vect len elem

The scanl1 function is a variant of scanl that doesn't require an explicit
starting value.
It assumes the first element of the vector to be the starting value and then
starts the fold with the element following it.

scanl1 (-) (fromList [1,2,3])

splitAt : (n : Nat) -> (xs : Vect (n + m) elem) -> (Vect n elem, Vect m elem)

A tuple where the first element is a Vect of the n first elements and
the second element is a Vect of the remaining elements of the original.
It is equivalent to (take n xs, drop n xs) (splitAtTakeDrop),
but is more efficient.

n

the index to split at

xs

the Vect to split in two

splitAt 2 (fromList [1,2,3,4])

splitAtTakeDrop : (n : Nat) -> (xs : Vect (n + m) a) -> splitAt n xs = (take n xs, drop n xs)

tail : Vect (S len) elem -> Vect len elem

All but the first element of the vector

tail [1,2,3,4]

take : (n : Nat) -> Vect (n + m) elem -> Vect n elem

Get the first n elements of a Vect

n

the number of elements to take

take 2 [1,2,3,4]

takeDropConcat : (n : Nat) -> (xs : Vect (n + m) a) -> take n xs ++ drop n xs = xs

A Vect may be restored from its components.

takePrefix : (ns : Vect n a) -> (ms : Vect m a) -> take n (ns ++ ms) = ns

Adding a prefix and then taking the prefix gets the prefix. Or,
adding a suffix and then dropping the suffix does nothing.

takeTake : (n : Nat) -> (m : Nat) -> (xs : Vect (n + m + l) a) -> (ys : Vect (n + (m + l)) a) -> xs ~=~ ys -> take n (take (n + m) xs) = take n ys

take n . take (n + m) = take n

takeUpto : (x : Nat) -> Vect n elem -> Vect (minimum x n) elem

Take up to the first n elements of a Vect if they exist.

n

the maximum number of elements to take

takeUpto 10 [1,2,3,4]

takeWhile : (p : elem -> Bool) -> Vect len elem -> (q : Nat ** Vect q elem)

Take the longest prefix of a Vect such that all elements satisfy some
Boolean predicate.

p

the predicate

takeWhile (<3) [1,2,3,4]

transpose : Vect m (Vect n elem) -> Vect n (Vect m elem)

Transpose a Vect of Vects, turning rows into columns and vice versa.

This is like zipping all the inner Vects together and is equivalent to traverse id (transposeTraverse).

As the types ensure rectangularity, this is an involution, unlike Prelude.List.transpose.

transpose [[1,2], [3,4], [5,6], [7,8]]

transposeCons : (xs : Vect o a) -> (xss : Vect o (Vect i a)) -> transpose (zipWith (::) xs xss) = xs :: transpose xss

transposeTraverse : (xss : Vect o (Vect i a)) -> transpose xss = traverse id xss

traverseIdCons : (xs : Vect o a) -> (xss : Vect o (Vect i a)) -> traverse id (pure (::) <*> xs <*> xss) = xs :: traverse id xss

unzip : (xs : Vect n (a, b)) -> (Vect n a, Vect n b)

Convert a vector of pairs to a pair of vectors

unzip (fromList [(1,2), (1,2)])

unzip3 : (xs : Vect n (a, b, c)) -> (Vect n a, Vect n b, Vect n c)

Convert a vector of three-tuples to a triplet of vectors

unzip3 (fromList [(1,2,3), (1,2,3)])

updateAt : (i : Fin len) -> (f : elem -> elem) -> (xs : Vect len elem) -> Vect len elem

Replace the element at a particular index with the result of applying a function to it

i

the index to replace at

f

the update function

xs

the vector to replace in

updateAt 1 (+10) [1,2,3,4]

vectAppendAssociative : (xs : Vect xLen elem) -> (ys : Vect yLen elem) -> (zs : Vect zLen elem) -> xs ++ ys ++ zs = (xs ++ ys) ++ zs

vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> x :: xs = x :: ys

vectInjective1 : x :: xs ~=~ y :: ys -> x ~=~ y

vectInjective2 : x :: xs ~=~ y :: ys -> xs ~=~ ys

vectMustBeNil : (xs : Vect 0 a) -> xs = []

vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs

vectToMaybe : Vect len elem -> Maybe elem

Convert first element of Vect (if exists) into Maybe.

vectToMaybe [2]

zip : (xs : Vect n a) -> (ys : Vect n b) -> Vect n (a, b)

Combine two equal-length vectors pairwise

zip (fromList [1,2,3,4]) (fromList [1,2,3,4])

zip3 : (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n (a, b, c)

Combine three equal-length vectors elementwise into a vector of tuples

zip3 (fromList [1,2,3,4]) (fromList [1,2,3,4]) (fromList [1,2,3,4])

zipWith : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c

Combine two equal-length vectors pairwise with some function.

f

the function to combine elements with

xs

the first vector of elements

ys

the second vector of elements

zipWith (+) (fromList [1,2,3,4]) (fromList [5,6,7,8])

zipWith3 : (a -> b -> c -> d) -> (xs : Vect n a) -> (ys : Vect n b) -> (zs : Vect n c) -> Vect n d

Combine three equal-length vectors into a vector with some function

zipWith3 (\x,y,z => x+y+z) (fromList [1,2,3,4]) (fromList [5,6,7,8]) (fromList [1,1,1,1])

zipWithIsLiftA2 : (f : a -> b -> c) -> (as : Vect n a) -> (bs : Vect n b) -> zipWith f as bs = pure f <*> as <*> bs

zipWithIsLiftA3 : (f : a -> b -> c -> d) -> (as : Vect n a) -> (bs : Vect n b) -> (cs : Vect n c) -> zipWith3 f as bs cs = pure f <*> as <*> bs <*> cs