# 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 `fst`

, _{3}`snd`

, and _{3}`trd`

that extract the first, second, and third members of a triple._{3}

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
c
```_{0} ≡ zro
c_{1} = scc zro
c_{2} = scc (scc zro)
⋮

Something bad happens when we try this out:

`scc c`_{0} ≡ (λ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 `c`

. However, they are observationally equivalent (_{1}`scc c`

), which we can show as follows:_{0} = c_{1}

` ⟶`_{v} λs. λz. s ((λz. z) z)
⟶_{v} λs. λz. s z
≡ c_{1}

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.