Lists and List Comprehensions

  1. Continuing to encode lists in terms of their left-folds, how should we write head? This is challenging.

Here is a hint / solution

Consider the list [a, b, c]. It will be encoded as \f z. f (f (f z a) b) c. We don't know what will be the result of f z a, but let's call this m a, for some function m. We want f (m a) b to also be m a, and f (m a) c to again also be m a. So that we get the same result whether we query [a], or [a, b], or [a, b, c], or whatever. We could get the result that f (m a) b was m a if f were the K combinator (\x y. x). But it can't be that easy, because we also need f z a to be m a, which will have to somehow represent a, rather than another head the list might have had, and if f were just K, then f z a would instead be z. (And we can't choose a fixed z that would be give the right answer for all lists, with varying heads.)

Perhaps we can instead have (1) m a be a function that accepts b (and later, c) as arguments and ignores them. Whereas (2) z is a function that accepts a as an argument and doesn't ignore it, but rather uses it to generate m a.

Let's try to handle (1) first. Naively, it looks like what we want is for m a to be something like \b. m a. But the problem is that we don't know (yet) how to have lambda expressions that "include themselves". So here's a workaround. Instead of having m a be a function that takes a single argument b, let's make it a function that takes two arguments, m and b. It should apply its m argument to a and ignore its b argument. This is straightforward to write:

\n b. n a

That's what m a should be, so m should be \a. \n b. n a. And if we check:

(m a) m b
((\a. \n b. n a) a) (\a. \n b. n a) b ~~>
(\n b. n a) (\a. \n b. n a) b ~~>
(\b. (\a. \n b. n a) a) b ~~>
(\b. (\n b. n a)) b ~~>
(\n b. n a) <~~>
m a

Looks good. So f needs to be a function that accepts an argument w (after the first stage, this will be m a), and an argument b, and applies w to m and to b. In other words, f should be:

\w b. w m b

with m understood as above. The head function will involve left-folding that f function over the list.

Now let's deal with (2). We have to choose an appropriate z so that f z a, in other words, z m a, results in m a. Here we can just let z be I.

How are we doing so far? The result of left-folding the f and z we've specified over:

[a, b, c]

will be m a, that is, \n b. n a, and the result of left-folding them over the empty list [] will just be z, that is I.

To finish up, we just have to massage these results into the form we want our head function to return. If we just feed m a two arguments, the first being I and the second being anything, we will get the result a. And if we look at the other result, gotten by left-folding over [], it is I. If we feed it two arguments, the first being I and the second being something else, we will get the something else as our result. So we can let the something else be whatever we choose to be the result of head []. I will let it be the variable err.

Pulling it all together then:

let m = \a. \n b. n a in
let f = \w b. w m b in
let head = \xs. (xs f I) I err in

You can test it with:

let empty = \f z. z in
let abc = \f z. f (f (f z a) b) c in
head abc  ; or try: head empty