Thinking about this, adapted from a tweet that was meant to infuriate

if e then true else false

Because it's equivalent to e ofc, but really it's a case of:

if e then C[true] else C[false] === C[e]

But also:

if e then (if e then e1 else e2) else (if e then e3 else e4) === if e then e1 else e4

Or generally:

if e then C1[e] else C2[e] === if e then C1[true] else C2[false]

And finally:

C[if e then e1 else e2] === if e then C[e1] else C[e2]

✨ eta laws ✨

At least, the first one is definitely an eta law, since it's the eliminator wrapped around constructors
The third one is a bit dangerous, since e gets evaluated first instead of whatever's in your context C
I feel like the second one should arise from some congruence rules but I can't see how

Anyway I distinctly remember making the same "mistake" in my first CS lab in Racket, but it's amusing to think that something as simple as that could be made as complicated as "eta expansion of booleans in the empty context"
Anything can be made complicated if you specialize deep enough

But why are there three of them? Are there more that I'm missing? Where do they come from? These and more than these

Sign in to participate in the conversation

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.