Neat vector stuff in lambda calculus

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