Bool and Pair are dual!

Right, so. I’ve “known” for a while that sum types (enums) and product types (structs) are dual in a precise sense. I even kind of intuitively understood what that “precise sense” is. But this example was particularly visceral.

Here’s your bog-standard Church encoding of booleans:

\[\begin{align} \mathrm{true} &= \lambda x. \lambda y. x \\\
\mathrm{false} &= \lambda x. \lambda y. y \\\
\mathrm{if} &= \lambda b. \lambda t. \lambda f. b \: t \: f \end{align}\]

For example, \(\mathrm{if} \: \mathrm{true} \: 42 \: 101\) reduces to \(42\), like you’d expect.

And here’s your Church encoding of pairs:

\[\begin{align} \mathrm{pair} &= \lambda l. \lambda r. \lambda f. f \: l \: r \\\
\mathrm{fst} &= \lambda p. p \: (\lambda l. \lambda r. l) \\\
\mathrm{snd} &= \lambda p. p \: (\lambda l. \lambda r. r) \end{align}\]

Wait, why do those inner lambdas in fst and snd look so familiar? And wait, isn’t pair just if with its arguments rearranged?

…Oh my god.