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
