There are many different implementations of vectors in lambda calculus, wikipedia covers pairs as nodes and right-fold lists, here I will be using right-fold lists because they are much more intuitive.

Vectors look like this:

``````\f\x f 0 (f 1 (f 2 x))
``````

They look similar to church numbers except `f` takes two arguments, the element and then the result of the next application.

But what can you do with these vectors? A lot actually.

Concatenating two vectors is the same as adding two numbers:

``````concat = \a\b
\f\x a f (b f x)
``````

Which basically works by setting x (the tail) to the vector you want to append.

Say you wanted to take a vector but add 1 to each element, to do this you want to use a map function:

``````map (\f\x f 0 (f 1 (f 2 x))) succ
``````

Gives us:

``````\f\x f 1 (f 2 (f 3 x))
``````

The implementation of map is fairly simple:

``````map = \s\fn
\f\x s (\nm\nx f (fn nm) nx) x
``````

This works by turning `\f\x f 0 (f 1 (f 2 x))` into `\f\x f (fn 0) (f (fn 1) (f (fn 2) x))` and in our example fn was `succ` so each element turned into it's successor.

One of the most useful functions for vectors is `fold` which lets you iterate a vector while keeping some state, it is used multiple times in other vector functions.

``````fold = \v\iv\l
v (\e\nx
\st nx (l st e)
) (\st iv) iv
``````

For example, `fold (\f\x f 0 (f 1 (f 2 x))) iv l` gives you `l (l (l iv 0) 1) 2`

I wrote many vector functions including insertion, deletion, matching, slicing, equality, etc. all of which have been thoroughly tested and you can find them here: https://lab.pxtst.com/PixelToast/llama/blob/master/stl/stdvec.lf