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.