Having covered types, let’s now turn our attention to lists. Lists are general purpose data structures for storing sequences of items. In lambda calculus, lists are represented using pairs, with the first item of the pair representing the head of the list, and the second item representing the rest of the list. A special value, nil, at as the second item of the pair terminates the list.
Pairs
Let’s start by focusing on pairs (or tuples). A pair is built from two arguments, \(a\) and \(b\), and returns a function \(f\) enclosing those two arguments:
$$ \text{def pair} = \lambda a . \lambda b . \lambda f . ((f\ a)\ b) $$
If we bind variables \(a\) and \(b\) to values \(9\) and \(5\) we can see how a pair is constructed:
$$ \begin{aligned} \text{pair 9 5} & = \lambda 9 . \lambda 5 . \lambda f . ((f\ a)\ b) \cr & = \lambda f . ((f\ 9)\ 5) \cr \end{aligned} $$
Given a pair, we can extract the first and second item using additional functions:
$$ \begin{aligned} \text{def first p} & = \lambda a . \lambda b . a \cr \text{def second p} & = \lambda a . \lambda b . b \cr \end{aligned} $$
These functions take two variables and simply return one of them. We can apply this to our pair by first creating a pair, and then applying first or second to that pair. Here we assume that \(p\) is our previously defined \(\text{pair 9 5}\).
$$ \begin{aligned} \text{p first} &= \lambda f . ((f\ 9)\ 5) \ \text{first} \cr &= ((\text{first}\ 9)\ 5) \cr &= ((\lambda a . \lambda b . a)\ 9)\ 5) \cr &= \lambda 9 . \lambda 5 . 9 \cr &= \lambda 5 . 9 \cr &= 9 \cr \end{aligned} $$
Lists
Now we can turn our attention to lists. A list is either empty, or consists of a head (any lambda expression) and a tail (another list). A list will consist of a pair made from the list’s head and tail. That is, given the head of a list \(h\) and the tail \(t\), the general representation of that list is simply the pair of \(h\) and \(t\). Here, we define a list constructor in terms of pair.
$$ \begin{aligned} \text{def list} \ h \ t & = \text{pair} \ h \ t \cr & = \lambda f . ((f\ h)\ t) \cr \end{aligned} $$
We can build up a bigger list by repeated applications of list. To do so, we need a termination value to represent the end of the list (nil). For now, you can use any arbitrary object to represent nil, we will assume such an object exists and call it \(\text{NIL}\). For example, to build up a list of three elements, we invoke the list constructor three times:
$$ \text{list} \ a \ (\text{list} \ b \ (\text{list} \ c \ \text{NIL})) $$
Summary
There isn’t really much more than that. Since lambda calculus is based solely on functions and their application, building up a list using lambda calculus is an exercise in applying functions in the correct manner to represent the data structure that you want. Once you have the data structure, you write more functions to act on that data as required. For lists, you would typically use recursive lambda functions to iterate over your list until you reach the \(\text{NIL}\) value.