The difference between Lists as pairs and Lists as recursors in the Lambda Calculus

Question

I understand that there are several ways to represent lists in the lambda calculus. Using pairs I can write a list as

(t1, (t2, (t3, NIL)))

which is equivalent to the lambda term \f. f t1 (\f. t2 (\f. t3 NIL)))

and perform operations such as

head = \l.l (\h.\t.h)

How do lists as recursors work and how would I write them down?

Answer 1

List as recursors are "natural folds".

The ctors are looking like this:

nil  =               \add. \zero. zero
cons = \head. \tail. \add. \zero. add head (tail add zero)

After some optimization (inlining the bodies, beta/eta-reducing everything), the term

cons(1, cons(2, cons(3, nil)))

becomes the equivalent one

\add. \zero. add 1 (add 2 (add 3 zero))

As you can notice, the list waits for two ctor replacers (cons -> add, nil -> zero), and becomes a fold.

Applying a (+) and 0 will give us list sum, (*) and 1 - list product, cons again and some tail list will give us the tail appended to the back of initial list.

Head op is implemented like whis:

head = \l. \def. l (\x. \y. x) def

It takes a list and a default value to return if list is empty and returns the head.

The tail though is hard to implement and it will work with O(list-length).

Shortly, list as recursors are prepared folds.