Small shots of lambda calculus, part III

Last time, we talked about pairs and more complex arithmetic, and we previously discussed the basics of lambda calculus and simple arithmetic.

This time we’re going to talk about lists.

There are several different ways to define lists in lambda calculus. One way is as a more complicated pair. We use cons and nil to construct lists:

> cons h t f x = f h t
> nil      f x = x

And we use head and tail to get the first item and all but the first items, respectively:

> head_ x l = l (\h t -> h)
> head = head_ 0
> tail_ x l = l (\h t -> t)
> tail = tail_ nil

Here are a few examples of using them in our imaginary lambda calculus interpreter:

>>> cons 1 nil
cons 1 nil

>>> head (cons 1 nil)
1

>>> tail (cons 1 nil)
nil

>>> head nil
0

>>> tail nil
nil

This is all well and good, but it’s kind of boring. These lists are basically no different from pairs and, in order to do anything useful such as mappings and folds, we have to go jump through hoops of complexity.

Perhaps this is best, for otherwise we might’ve been content with this representation for lists and not have found the other viable representation, which I consider to be the most elegant.

An empty list is nil:

> nil f x = x

Note that nil is unchanged, and that nil has the same definition as 0.

To construct the list we use cons:

> cons h t f x = f h (t f x)

This is very similar to the succ function we defined in Part 1. To understand how it works, we should look at some sample lists. (Note our list shorthand: comma separated list of values encased in square brackets.)

>>> [] f x
x

>>> [1] f x
f 1 x

>>> [1,2] f x
f 1 (f 2 x)

>>> [1,2,3] f x
f 1 (f 2 (f 3 x))

Compare this to the way numbers are defined:

>>> 0 f x
x

>>> 1 f x
f x

>>> 2 f x
f (f x)

>>> 3 f x
f (f (f x))

It’s hard to argue that there’s a more natural way of expressing lists in lambda calculus.*

It’s easy to get the head value:

> head_ x l = l (\h v -> h) x
> head = head_ 0

>>> head []
0

>>> head [1]
1

>>> head [1,2]
1

But getting the tail is hard, like getting the predecessor of a number:

> tail_ x l = 1st (l (\h p -> pair (2nd p) (cons h (2nd p))) (pair x nil))
> tail = tail_ nil

>>> tail []
[]

>>> tail [1]
[]

>>> tail [1,2]
[2]

>>> tail [1,2,3]
[2,3]

Actually tail works just like pred, but instead of doing succ each iteration, it does cons h.

Some properties and predicates:

> length l = l (\h n -> succ n) 0
> nil?   l = l (\h b -> false) true
> sum    l = l add 0

>>> length []
0

>>> length [1,2,3,4]
4

>>> nil? []
true

>>> nil? [1,2,3,4]
false

>>> sum []
0

>>> sum [1,2,3,4]
10

We should also define map (which passes a function through all items of a list):

> map f l = l (\h v -> cons (f h) v) nil

>>> map (add 5) []
[]

>>> map (add 5) [3]
[8]

>>> map (\x -> mul x x) [1,2,3,4,5]
[1,4,9,16,25]

That’s it for today. Tell me what else you’d like to know about Lambda Calculus (in the comments on reddit).

Footnotes

* - By the way, this list representation corresponds to Haskell’s foldr.