🪞 Neat, Not Useful

The front page maps where programming-language theory and category theory converge: same structure, different notation. This page maps the opposite. Where the bridge holds and still drops its cargo.

Each entry below is a useful PL theorem whose clean categorical mirror already exists and is useless, because the mirror was made clean by discarding the part that made the theorem worth proving. The bridge carries the structure across. It leaves the payload on the dock.

reverse-mode gradient costs
≤ c · forward,
for every input dimension n
        (Baur–Strassen)

R[f] : A × B → A
the reverse derivative,
functorially correct
        (reverse derivative cats)

The mirror on the right is exact. It says nothing about cost. The neatness bought correctness by forgetting the only quantity anyone wanted.

Neat and useful come apart

A result is neat when it composes: it falls out of a universal property, the diagram commutes, the proof is two lines of abstract nonsense. It is useful when it tells you something you can act on: this loop costs that much, those three processes deadlock, this query settles in n rounds. The two often coincide. At this boundary they come apart on a schedule, and the breakage has a shape.

None of that is news in the abstract. That denotational, compositional semantics quotients away cost, scheduling, and reduction order is the oldest lesson in the field, from the full-abstraction problem through Abramsky's intensional-semantics program to modern cost-aware semantics (Danner, Licata, Ramyaa). The narrow, concrete claim is this: walk the specific bridges the front page celebrates, push each one until it breaks, and every break sorts into one of three kinds.

⊘ payload dropped — the mirror is exact and blind to the quantity that mattered (the neat, not useful case proper) · ⤳ wrong building — a real home exists, but in a different structure than the advertised bridge · ▣ already named — the mirror exists under a name from another field

The rule, stated so it can be broken

A PL theorem ports across one of these bridges when its content is extensional, and resists when its content is intensional: cost, sharing, rate, scheduling, realizability. The clean mirror keeps what survives the quotient and loses the rest, and the rest is usually the reason the theorem exists.

To break the rule, exhibit one port that carries the intensional theorem itself, not its correctness corollary: a categorical statement that recovers the cost bound, the deadlock classification, the convergence rate, with the constant or the count intact. Seventeen tries across this interface did not produce one. That is a weak induction, not a proof, and this page exists to be falsified by a counterexample.

The caution that follows is small and practical. When category theory does not yet have your favorite PL result, three things are far more likely than an open gold seam: it has the result under a name you have not searched, or the clean version drops the part you cared about, or the right structure is in a different building than the obvious bridge. Check those three before claiming the seam.

Why this is a companion to the front page and not a contradiction of it: the entries there are real. Same structure, different notation, often a proven equivalence. This page is what is left when you ask each of those bridges to carry something heavier than structure.

Related: the convergences · 🐱 Category Theory