Data structures in λ

Reading: TAPL Section 5.2, pages 58-63.

Booleans

We represent true and false as functions of two arguments that return their first and second argument, respectively.

  tru ≡ λt. λf. t
  fls ≡ λt. λf. f
 test ≡ λl. λm. λn. l m n

Note that under call-by-value evaluation, test is not the same as if in most programming languages. This is the subject of Exercise 5.2.9. (Similarly, and as defined here is not the same as in most programming languages.)

Exercise. In C (and Java and other languages) you can define Booleans as an enum:

enum bool {false, true};

Another common example of an enum is colors:

enum color {red, green, blue};

How would you encode the colors {red, green, blue} in the lambda calculus? Write definitions for red, green, blue, and a function casecolor that satisfy the following:

casecolor red   r g b = r
casecolor green r g b = g
casecolor blue  r g b = b

(Here and below, = means βᵥ-equivalence.)

Pairs

We represent a pair as a function that takes another function b and calls it on the two members of the pair.

    pair ≡ λf. λs. λb. b f s
     fst ≡ λp. p tru
     snd ≡ λp. p fls

If you’ve done any event-driven programming (like in JavaScript), you may recognize b as a callback.

Exercise. How would you generalize pairs to triples? Define a function triple that creates a triple, and functions fst3, snd3, and trd3 that extract the first, second, and third members of a triple.

The techniques illustrated above can be combined and generalized to any sort of data structure that has one or more alternatives, each of which contains zero or more values.

Exercise. An option is a simple data structure that either holds a value (some v) or nothing (none). Define functions some, none, and caseoption such that:

caseoption (some x) s n = s x
caseoption  none    s n = n

Natural numbers

We represent the number n as a function taking two arguments, s and z, and applying s to z n times. These are known as Church numerals.

scc ≡ λn. λs. λz. s (n s z)
zro ≡     λs. λz. z
 c0 ≡ zro
 c1 = scc zro
 c2 = scc (scc zro)
    ⋮

Something bad happens when we try this out:

scc c0 ≡ (λn. λs. λz. s (n s z)) (λs. λz. z)
     ⟶ λs. λz. s ((λs. λz. z) s z)

Under call-by-value, we cannot reduce anymore, but this is not the same as c1. However, they are observationally equivalent (scc c0 = c1), which we can show as follows:

    ⟶v λs. λz. s ((λz. z) z)
    ⟶v λs. λz. s z
       ≡ c1

You could also think of Church numerals as a kind of data structure: a Church numeral is either zro, which contains no values, or scc n, which contains the value n. In fact, they’re very similar to the options from the exercise above. The difference is that applying an option deconstructs just the option, not its contents, whereas applying a Church numeral deconstructs the whole thing.

This makes it possible to define addition, multiplication, etc. easily. But it also makes defining the predecessor function (prd) surprisingly difficult. For a while, Church thought it might not be possible, until Kleene thought of a solution (essentially the one in TAPL) while he was having his wisdom teeth out.