In my view, the definitive trick is reading the definitions from the end to the beginning, because in all three of them the free variables are always those that can be found in the lambda within the body (m
, p
and q
). Here is an attempt to translate the code to English, from the end (bottom-right) to the beginning (top-left):
(define (cons x y)
(lambda (m) (m x y))
Whatever m
is, and we suspect it is a function because it appears right next to a (
, it must be applied over both x
and y
: this is the definition of cons
ing x
and y
.
(define (car z)
(z (lambda (p q) q)))
Whatever p
and q
are, when something called z
is applied, and z
is something that accepts functions as its input, then the first one of p
and q
is selected: this is the definition of car
.
For an example of "something that accepts functions as its input", we just need to look back to the definition of cons
. So, this means car
accepts cons
as its input.
(car (cons 1 2)) ; looks indeed familiar and reassuring
(car (cons 1 (cons 2 '()))) ; is equivalent
(car '(1 2)) ; is also equivalent
(car z)
; if the previous two are equivalent, then z := '(1 2)
The last line means: a list is "something that accepts a function as its input".
Don't let your head spin at that moment! The list will only accept functions that can work on list elements, anyway. And this is the case precisely because we have re-defined cons
the way that we have.
I think the main point from this exercise is "computation is bringing operations and data together, and it doesn't matter in which order you bring them together".
pair ≡ λx.λy.λz.z x y
. – Joshua Taylor