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.


1 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.