Lists

What Is a List?

A list in lambda calculus is built from the same pairs we already have. The idea is simple: each node is a PAIR containing two things:

1. An element -- the data at this position
2. The rest of the list -- another pair, or a marker for "empty"

A list like [a, b, c] becomes nested pairs:

PAIR a (PAIR b (PAIR c NIL))

Each pair holds one element and a pointer to the remaining list. The last pair points to NIL, a special marker meaning "nothing more."

No new machinery. Just pairs, nested inside each other, with a sentinel at the end.

NIL

Every list ends somewhere. We need a marker that says "this is the end -- there are no more elements." That marker is NIL, the empty list.

Without NIL, we would have no way to tell where a list stops. The last pair would point to... what? NIL gives us a definite answer: a special term that is not a pair, that signals termination.

Think of it like the period at the end of a sentence. Without it, you would never know when the sentence ends.

NIL is a lambda term chosen by convention. The specific encoding varies, but its role is always the same: a recognizable marker meaning "empty."

CONS

To build a list, we need an operation that adds an element to the front. This operation is called CONS (short for "construct").

CONS takes two arguments:

• h -- the element to add (the "head")
• t -- the existing list (the "tail")

And it returns a new pair:

CONS h t = PAIR h t

That is the entire definition. CONS is just PAIR by another name. We give it a separate name because its intent is different: PAIR bundles any two values, while CONS specifically builds a list node -- an element joined to the rest of a list.

Example: CONS a NIL creates the one-element list [a], represented as PAIR a NIL.

Building a List

To build a list with multiple elements, we nest CONS calls. Each CONS adds one element to the front of an existing list.

Start from the end and work backward:

1. Start with the empty list: NIL
2. Add b to the front: CONS b NIL = PAIR b NIL
3. Add a to the front: CONS a (CONS b NIL) = PAIR a (PAIR b NIL)

The result represents [a, b]:

PAIR a (PAIR b NIL)
     |       |
     a    PAIR b NIL
              |
              b

The outermost pair holds a. Its second component holds the rest of the list -- another pair holding b, whose second component is NIL.

HEAD

Once we have a list, we need to access its elements. The first operation is HEAD, which retrieves the first element.

Since a list node is PAIR element rest, and FST extracts the first component of a pair, HEAD is simply:

HEAD = FST

Example:

• HEAD (CONS a (CONS b NIL))
• = FST (PAIR a (PAIR b NIL))
• = a

HEAD gives us the element at the front of the list -- the value that was most recently prepended with CONS.

TAIL

The companion to HEAD is TAIL, which returns everything after the first element -- the rest of the list.

Since a list node is PAIR element rest, and SND extracts the second component of a pair, TAIL is simply:

TAIL = SND

Example:

• TAIL (CONS a (CONS b NIL))
• = SND (PAIR a (PAIR b NIL))
• = PAIR b NIL
• = CONS b NIL

The result is itself a list -- the original list with the first element removed. This is how we traverse: take the TAIL to move forward, one element at a time.

HEAD of a List

HEAD = FST extracts the first element of a list. CONS = PAIR builds a list node.

Recall:

• CONS a (CONS b NIL) = PAIR a (PAIR b NIL)
• HEAD list = FST list = first component of the pair

Applying HEAD to a list returns the element at the front -- the value that was prepended last.

TAIL of a List

TAIL = SND extracts everything after the first element. CONS = PAIR builds a list node.

Recall:

• CONS a (CONS b NIL) = PAIR a (PAIR b NIL)
• TAIL list = SND list = second component of the pair

The result of TAIL is itself a list -- the original with the first element removed.

Nested Structure

Lists nest to the right. Each CONS wraps an element around the rest of the list, and "the rest" is always the second component:

[a, b, c] = CONS a (CONS b (CONS c NIL))

Expanding CONS to PAIR:

PAIR a (PAIR b (PAIR c NIL))

The structure branches rightward:

PAIR
/ \
a  PAIR
   / \
   b  PAIR
      / \
      c  NIL

Each level holds one element on the left and the remaining list on the right. HEAD peels off the left branch. TAIL follows the right branch deeper into the structure.

ISNIL

When traversing a list, we need to know when to stop. TAIL gives us the rest of the list, but eventually we reach NIL -- the empty list. We need a way to check: is this list empty or not?

The operation ISNIL tests whether a list is NIL. It returns TRUE for the empty list and FALSE for any non-empty list (a CONS node).

How ISNIL works depends on the encoding. One common approach: NIL is chosen so that applying a specific test function distinguishes it from CONS nodes. The details vary, but the purpose is always the same -- a boolean test for emptiness.

This is the list equivalent of ISZERO for Church numerals: a way to detect the base case.

Lists from Pairs

Let us take stock of the list operations:

• CONS = PAIR
• HEAD = FST
• TAIL = SND
• NIL = a chosen sentinel term

Every list operation is a pair operation with a new name. A list is nested pairs -- nothing more.

So what makes a list different from any other nested pair structure? Convention. We agree to always put the element first and the rest-of-list second. We agree that the nesting terminates with NIL. We agree to use HEAD/TAIL to access elements.

The lambda calculus does not know what a "list" is. It only knows pairs. We impose the list interpretation through disciplined use of a pattern.

Everything from Lambda

The inventory:

• TRUE, FALSE -- selectors: λx.λy.x and λx.λy.y
• Church numerals -- iteration counts: λf.λx.f (f (... x))
• PAIR, FST, SND -- bundling: closures that store two values
• CONS, HEAD, TAIL, NIL -- lists: pairs nested by convention

Every one of these is a pure lambda term. Booleans are functions. Numbers are functions. Pairs are functions. Lists are functions.

There is exactly one kind of thing in lambda calculus: a function that takes an argument and produces a result. Data is not a separate category. Data IS functions, used in a disciplined way.