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]
if e then (if e then e1 else e2) else (if e then e3 else e4) === if e then e1 else e4
if e then C1[e] else C2[e] === if e then C1[true] else C2[false]
C[if e then e1 else e2] === if e then C[e1] else C[e2]
✨ eta laws ✨
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
A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.