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:

For example, reduces to , like you’d expect.

And here’s your Church encoding of pairs:

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.