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
snd look so familiar?
And wait, isn’t
if with its arguments rearranged?
…Oh my god.