# Data structures in the lambda calculus

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.