Bool and Pair are dual!

Feb 8, 2016

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:

$true = \lambda x. \lambda y. x \\ false = \lambda x. \lambda y. y \\ if = \lambda b. \lambda t. \lambda f. b \: t \: f \\$

For example, $if \: true \: 42 \: 101$ reduces to $42$ , like you’d expect.

And here’s your Church encoding of pairs:

$pair = \lambda l. \lambda r. \lambda f. f \: l \: r \\ fst = \lambda p. p \: (\lambda l. \lambda r. l) \\ snd = \lambda p. p \: (\lambda l. \lambda r. r) \\$

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.