Lesson 12 · Canonicalisation

Canonicalisation, and why pass order stops mattering

In lesson 4 you said “idempotency is not enough”, which is right, and you were one term short of the answer. Here are the missing terms — and the surprise, which is that the way to make pass order irrelevant is not to make your passes commute.

Five words, precisely

Terminating and confluent are the two halves, and neither implies the other. A system can terminate at two different answers (not confluent), or agree on the answer it never reaches (not terminating). The textbook is Baader and Nipkow's Term Rewriting and All That; the practitioner statement of the same idea is MLIR's canonicalization doc, which is two screens and worth reading because it is a real system stating its rules as engineering constraints.

The move: shrink the input space, don't reorder the passes

The instinct after lesson 4 is to prove your passes commute pairwise. Don't — that is O(n²) obligations that grow every time you add a pass, and most pairs will not commute for reasons that have nothing to do with types.

The real technique is upstream. Run one normalising pass at the boundary that maps every input to its canonical form, and then the distinctions the later passes could have disagreed about no longer exist in their input. A pass that never sees Optional[X] cannot handle it differently from the pass next to it. You have not made the passes commute; you have removed the terms on which they differed.

Order stops mattering because the input got smaller, not because the passes got better.

This is the discipline the nanopass paper depends on and never has to argue for: each pass declares an IR that is missing the forms an earlier pass eliminated, so “handles only the canonical form” is checked by the language definition rather than remembered. Your equivalent, without a language definition, is the type: after canonicalisation TypeOpaque should be able to lose cases, and every case it loses is a branch that can never disagree again.

Newman's lemma, which saves you the O(n²)

You still need confluence of the canonicaliser's own rules, and here the theory gives you something usable. For a terminating system, local confluence implies global confluence — if every pair of rules that could both fire on the same term can be rejoined in one or more steps, the whole system is confluent. So you check critical pairs: overlapping rules, two at a time, on the smallest term where both apply. Not sequences. Not orders. Pairs of rules, of which you will have about eight.

The equivalences you actually have

Here is the concrete list for pydantic-codegen. Three of these are safe, and three of them look identical and are traps — which is the exercise below, so read the table for the shape and not for the answers.

Exercise A — Classify

Three verdicts per row. Canonicalise — safe, do it at the boundary. Not equivalent — the terms mean different things and collapsing them is a correctness bug. Equivalent, don't collapse — same meaning, but something downstream depends on the difference. Commit before clicking.

Four obligations on a canonicaliser

1. Meaning-preserving, on a stated property

“Same meaning” is not a feeling; it is a claim about a specific observation. Yours is: the generated output type-checks and validates identically. Under that property, dropping Annotated metadata is not meaning-preserving, and PEP 585 aliasing is. Say which property you mean and the arguments stop being about taste. This is the same discipline the EMI work in lesson 9 rests on — perturbations chosen so they cannot change the observation.

2. Idempotent, and tested for it

@given(annotations())
def test_canonical_is_idempotent(a: Annotation) -> None:
    once = canonicalise(a)
    assert canonicalise(once) == once

Three lines, and it catches the most common bug in the file: a rule that handles one level and not the nesting. Cheap, and it is a real property rather than an example.

3. Terminating, by a decreasing measure

Every rule must strictly decrease something — node count, or nesting depth, or a term ordering you write down. The failure mode is specific and social: someone adds X | None → Optional[X] because it reads better in output, while the existing rule goes the other way, and while changed: spins forever. A direction agreed globally, in one place, is the only defence, and a measure is how you state it.

4. Confluent, tested as a metamorphic relation

@given(annotations(), permutations(RULES))
def test_rule_order_is_irrelevant(a: Annotation, order: list[Rule]) -> None:
    assert apply_until_fixed(a, order) == canonicalise(a)

Read the shape: T is “permute the rule order”, R is “equal”. That is a metamorphic relation in lesson 9's exact sense, and it is the strongest one in your suite because it is where a non-confluent rule set shows up as a flake rather than as a failure.

Exercise B — Bug hunt

Five snippets. Click the offending line, or say no bug. One is clean.

Where canonicalisation hurts: the diagnostic

A canonicaliser destroys information on purpose. The information it destroys is what the user wrote, and that is the information a good error message needs:

error[E021]: recursive model has no base case
  --> app/models.py:14:4
   |
14 |     parent: Optional[Node]
   |             ^^^^^^^^^^^^^^ expected `Node | None`

The caret is right, the message mentions a form that appears nowhere in the file. There are exactly three fixes and only one of them is any good:

Take the middle one. The general statement is worth holding onto because it recurs: the canonical form is for your passes, the surface form is for the user, and the bridge between them is provenance. Give a compiler two audiences and it needs two representations; give it one place to recover the second and you can canonicalise as hard as you like.

Exercise C — Free recall

Interleaved with lesson 4, where the gap was.

What changes in the repo

And the diff that makes it worth having done: the assertion. One line, in the pass driver, and it converts “we normalise on the way in” from a convention into a checked invariant:

assert is_canonical(model), f'non-canonical annotation reached {pass_.__name__}'

Without it, the first pass that constructs an annotation by hand reintroduces a non-canonical form, nothing complains, and six months later a rule fires in one place and not another. With it, the pass that did it is named on the spot. Cheap invariants at pass boundaries are what a verifier is, from lesson 1.

What this unlocks

Two things, both of which were locked on this lesson. First, the nanopass discipline: per-pass IRs only pay for themselves when the forms actually shrink, and a canonicaliser is what makes them shrink. Second, and nearer, the feature that has been sitting on the fringe since lesson 5 — user-supplied methods. It needs canonical annotations for the same reason fake() did: a body that mentions a type must import it, and “which type is this?” has to have one answer.

status · resources · mission