Description of lists with functions in LISP

Question

I have been given the following implementation of basic list functions in LISP:

nil = (lambda (k) (k ’none ’none))
(cons x y) = (lambda (k) (k x y))
(car l) = (l (lambda (x y) x))
(cdr l) = (l (lambda (x y) y))
(null? l) = (l (lambda (x y) (= x ’none)))

As an intent to show that data can be constructed using only pure functions.

I don't understand very well this code. For starters, what's the role of k? Can you show how I can come up with this implementation? Basically, I'm looking for some intuition on how this works and if you can show in some manner how you deduce the implementation.

Answer 1

In PL theory, this is known as (a variant of) the Church-encoding of pairs.

The idea is the following: assume for the moment you only have a language with primitive booleans (true, false, if-then-else) and primitive (first-class) functions. Pairs are not primitive, yet they can be encoded as follows.

In place of a pair $(x,y)$ we can consider the following function: $$ p(b) = {\sf if}\ b \ {\sf then}\ x \ {\sf else}\ y $$ It is immediate to verify that $p({\sf true}) = x$ and $p({\sf false}) = y$. So this function $p$ indeed encodes the information which lies inside a pair. Projections can then be defined as $$ \pi_1(p) = p({\sf true}) \qquad \pi_2(p) = p({\sf false}) $$ while the pair constructor becomes $$ cons(x,y) = \lambda b.\ {\sf if}\ b \ {\sf then}\ x \ {\sf else}\ y $$

Now, suppose we no longer have primitive booleans/conditional, but only have functions. We can still obtain something which behaves as a boolean through this encoding: $$ {\sf true} = \lambda x y. x \qquad {\sf false} = \lambda x y. y \qquad $$ and (since now a boolean $b$ is a "binary" function) $$ {\sf if}\ b \ {\sf then}\ x \ {\sf else}\ y = b x y $$ It is immediate to verify that $$ {\sf if}\ {\sf true} \ {\sf then}\ x \ {\sf else}\ y = {\sf true} x y = x $$ and the $\sf false$ analogous.

Once you combine both encodings, you get that $$ \begin{array}{l} cons(x,y) \\ = \lambda b.\ {\sf if}\ b \ {\sf then}\ x \ {\sf else}\ y \\ = \lambda b. b x y \\ \end{array} $$ and $$ {\sf car} = \pi_1 = \lambda p. p {\sf true} = \lambda p. p (\lambda x y. x) $$ and its $\sf cdr$ analogous.

The LISP encoding you have is very similar to this encoding: it only have a few more twists for encoding $\sf nil$ as well, but that's a minor point.

The variable name $k$ which appears there in place of the "boolean" $b$ likely stands for "continuation", which is a key notion in PL theory.