ch:dimension-types: ch:dimension-types

Problem and result. Build one syntax-directed inferencer that normalizes dimensions, traverses source terms, solves its mixed equation store, and replays every returned substitution. The completed run infers polymorphic square, performs coherent unit addition, solves a coupled Smith row, and rejects both mismatched dimensions and an odd Smith pivot. The bundled corpus.kp runs the empty-environment cases. On the row $(2,3)$ for ${\delta }^2{ϵ}^3=L$, neither coefficient divides the other, so the starting fixture returns Unsupported; the completed project reduces $(2,3)$ to $(1,0)$ by Euclidean column operations.

Representation. Let $m$ be the number of base dimensions and dimension variables currently in scope, and let $k$ be the number having nonzero exponent in one expression. A normalized ordered sparse map stores $k$ key–exponent pairs; equality and substitution merge the ordered keys. A dense vector stores all $m$ exponents and gives constant-time access once a key’s index is known. Use sparse maps while traversing source syntax. Before Smith reduction, freeze one ordered list of the $m$ keys and convert every equation row to a dense vector in that same order. Give types constructors for ordinary variables, numeric annotations, and arrows. Give source terms constructors for variables, literals, lambdas, application, let, the three binary arithmetic forms, and integer power. Store schemes as a quantified prefix plus a monotype. Keep ordinary-type and dimension-variable supplies as separate counters, each initially above every name in the input. An inference result contains a substitution, inferred type, generated ordered equations, and the unused suffixes of both supplies. The entry point solveDimSystem returns a solved substitution and unused supply or a divisibility certificate; inferW returns the inferred type, composed substitution, equation store, and unused supplies; evalCore returns a numeral or aritherr.

First complete version. Implement exponent-map normalization, multiplication, inverse, power, and substitution first. Then replace the bundled divisibility selector by Smith reduction while recording every row and column operation for replay. For a fresh dimension parameter $\eta$, the fixture ${\delta }^2{ϵ}^3=L$ must return and replay $\delta =L^{-1}{\eta }^3,ϵ=L{\eta }^{-2}$, rather than Unsupported. Next implement variables, annotated literals, lambdas, and multiplication in Algorithm W’s left-to-right order. On $\lambda x.x\ast x$, choose one ordinary type for $x$, two fresh dimension variables for the numeric premises, solve the generated mixed equations, and generalize the residual dimension parameter. Print the inferred scheme and replay every generated equation under the returned substitution before declaring the case successful.

Remaining cases. Add application and let with the exact substitution order from definition 6.16. Add addition, multiplication, division, and power; addition must apply the right-operand substitution to the left inferred type before creating its two numeric equations. The mixed solver first eliminates ordinary variables with an occurs check, then sends its complete residual numeric store to the deterministic Smith routine. Name free Smith columns left to right from the remaining dimension supply. Generalize both ordinary and dimension variables after subtracting the free variables of the substituted environment. The fixture $y:\mathsf{Num}[\delta ]⊢\lambda z.y$ must quantify the argument type variable but not $\delta$. Finish with canonical unit scales and a small evaluator for the accepted arithmetic case.

A failing version. Change only the pivot test so that exponent one is accepted at pivot two. This check-clean mutation admits ${\delta }^2=L$. The oracle must reject the mutant even though the compiler still accepts it.

Acceptance test. Require a silent check, an empty audit, and computed trace lines for the generalized square scheme, successful equation replay, the canonical result $2$ at $L$, rejection of $3@\mathsf{m}+2@\mathsf{s}$, and rejection of ${\delta }^2=L$. Also require the coupled-row solution and the environment-sensitive generalization fixture. From artifacts/ch6-dimension-inferencer/, run kappa check corpus.kp, kappa test corpus.kp, kappa run corpus.kp, and kappa audit corpus.kp. Require the completed corpus to pass and the odd-pivot mutant to fail its test oracle.

Mathematical boundary. The run checks a finite set of generated certificates. It does not prove the Smith theorem, mixed-unifier principality, type safety, or unit-change invariance.