skip to content

With only abstraction and application available, how can a term encode a pair and recover each component?

level: middleimportance: should knowfreq 26%

answer

  1. data is what you can do with it
  2. the value is itself a function
  3. the caller supplies a selector
  4. two selectors, two components
  5. the same two terms encode booleans

basics

~20 s

A pair becomes a function that carries both components and hands them to a selector the caller supplies. Apply it to a selector returning its first argument to get one component, and to a selector returning its second for the other.

solid answer

~50 s

The trick is that a value is defined by how it is *used*, not by what it stores. A pair is `λa. λb. λs. s a b`: given two components it returns a function still waiting for a **selector**. Hand that function `λu. λv. u` and you get the first component back; hand it `λu. λv. v` and you get the second. Those two selectors are exactly the standard **Church encoding** of true and false, which is why a conditional needs no special form — applying an encoded boolean to two branch terms *is* the conditional. Numbers follow the same pattern: a numeral is the term that applies a supplied function a given number of times to a supplied start value, so zero is `λf. λx. x` and successor wraps one more application around the body.

code

pseudocode · 11 lines
pseudocode
pair   = λa. λb. λs. s a b
first  = λp. p (λu. λv. u)
second = λp. p (λu. λv. v)

pair M N          ==> λs. s M N           -- two steps, one per binder

first (λs. s M N)
  ==> (λs. s M N) (λu. λv. u)   -- substitute the selector for p
  ==> (λu. λv. u) M N           -- the pair hands over both parts
  ==> (λv. M) N                 -- the selector keeps the first
  ==> M                         -- and discards the second

go deeper

for a junior

Recall the central idea rather than the terms: a value can be represented by a function that performs the one thing you would do with that value. A pair is reached by handing it a selector.

for a middle

Write the pair and its two accessors, and trace one recovery to the component. Explain that the two selectors are also the encoded booleans, which is why a conditional is an ordinary application.

for a senior

Draw the practical lesson: modelling a value by the operations it supports rather than by its fields is the same move that produces a good interface, and the encoding is where that idea is at its purest.

for a principal

The angle worth owning is the tradeoff between minimal cores and useful ones. A tiny set of primitives makes a language easy to reason about and shifts every cost onto whatever has to make the derived forms fast.

## A value defined by how it is used The calculus has variables, abstraction and application, and nothing else — no records, no tags, no constructors. Yet it is expressive enough to encode booleans, pairs, numbers and lists, and the single idea behind all of it is this: **represent a value by the one thing anyone can do with it.** What can you do with a boolean? Choose between two alternatives. What can you do with a pair? Take out one component or the other. What can you do with a number, in the crudest possible terms? Repeat something that many times. In each case the encoding is a function that performs exactly that act, given the pieces the caller supplies. This family of encodings is named after the calculus's originator and is usually called **Church encoding**. ## Two selectors, and the booleans they are There are two obvious two-argument functions: | Term | Behaviour | Encoding of | |---|---|---| | `λu. λv. u` | returns its first argument, discards the second | true | | `λu. λv. v` | returns its second argument, discards the first | false | Nothing marks these as booleans; their *behaviour* is the choosing. A conditional is then just application: `c t e`, the encoded boolean applied to the two branch terms, reduces to `t` when `c` is the first term and to `e` when it is the second. A language whose booleans behave this way does not need a conditional in its grammar, because a conditional is an ordinary function. That observation is what people mean when they say control flow can live in a library. ## A pair is a function waiting for a selector Define `pair = λa. λb. λs. s a b`. Applying it to two components takes two beta steps, one per binder, and leaves `λs. s M N` — a term that holds `M` and `N` and is waiting to be told what to do with them. The accessors then supply the selectors: - `first = λp. p (λu. λv. u)` - `second = λp. p (λu. λv. v)` Reducing `first (λs. s M N)` takes four steps: substitute for `p`; the pair hands both components to the selector; the selector keeps the first; the second is discarded. The result is `M`. The components were never *stored* anywhere — they are free-standing terms sitting inside a body, and the only way to reach them is to give the pair the rule it is waiting for. ## Numbers as repeated application A numeral takes a function and a start value and applies the function that many times: - `zero = λf. λx. x` — apply `f` not at all. - `two = λf. λx. f (f x)` — apply it twice. - `succ = λn. λf. λx. f (n f x)` — run `n`, then apply `f` once more. Arithmetic falls out of composition rather than counting. Addition is `λm. λn. λf. λx. m f (n f x)`: apply `f` to `x` a total of `n` times, then `m` more times on top. Nothing anywhere holds a quantity; the numeral *is* the repetition. ## What the encoding buys, and what it costs - **Buys: an existence argument.** Data is not a separate ingredient of a language. Given abstraction and application, the rest can be built, which is why the paradigm treats functions as the primitive and everything else as derived. - **Buys: the habit of defining by use.** Modelling a value by the operations it supports, rather than by its fields, is the same instinct that produces a good interface. - **Costs: everything is a function.** An encoded pair, an encoded boolean and an encoded numeral are all just terms, and nothing in the bare calculus stops you applying one to another and getting a term that means nothing. Ruling that out is the job of a type discipline, which other material owns. - **Costs: performance nobody would accept.** Reaching a component means running a reduction; asking whether a numeral is zero means applying it. These encodings are a demonstration, not an implementation strategy. - **Costs: information thrown away.** Applying an encoded boolean picks a branch and keeps nothing about why — the concern usually named **boolean blindness**, and the reason richer values that carry their reason are preferred in real designs. The reason this is worth ten minutes is not that anyone encodes pairs this way. It is that once you have seen a data structure built out of nothing but functions, "functions are values" stops being a slogan about syntax and becomes a statement about what a value can be.

  • How does a conditional work when booleans are encoded as selectors?
    It needs no special form. The encoded true is the two-argument function returning its first argument and false the one returning its second, so the boolean applied to two branch terms *is* the conditional. Both branches are handed over as terms; whether the discarded one is ever worked on is a question about reduction order rather than about the encoding.
  • What does the numeral encoding make easy, and what does it make awkward?
    Easy: anything shaped like repetition. A numeral applies a function that many times, so addition and multiplication are just arranging that repetition, and successor wraps one more application around it. Awkward: going backwards. Predecessor has to rebuild the count from scratch while carrying the previous value alongside — which is exactly why it is the classic exercise rather than a one-liner.

saying these in an interview costs you the question

  • Thinks the calculus must add primitives for booleans and numbers
  • Says the encoded pair stores its components in a hidden field
  • Assumes an encoded value carries a tag naming its kind
  • Believes a numeral holds a count rather than repeating an application
  • Claims these encodings are efficient enough for real code