Dimension types and units of measure

Pure HM plus the two-sorted type former $\mathsf{Num}[d]$. Dimensions form the free abelian group on fixed base generators and inferred dimension variables; ordinary type variables and dimension variables are disjoint sorts. Compound units have product, inverse, and integer power, positive rational scales, and closed dimensions. Source type conversion is structural and uses normalized dimension equality only at numeric annotations. The recursion-free canonical core contains annotated lambdas, rational numeric values, left-to-right arithmetic, and a typed terminal $\mathsf{aritherr}$ outcome for division by zero and negative powers of zero. There is no state, recursion, subtyping, refinement logic, affine-unit translation, or QTT grade judgment. Runtime core contexts and lets are monomorphic; derivation-directed source elaboration expands a generalized let template separately at every source instantiation.

Dimension equality is equality of normalized finite exponent maps. One call of $\mathsf{munify}$ decomposes ordinary type equations and collects all numeric equations in one dimension store. The store is converted to $Mz=c$ and solved by a Smith reduction $UMV=S$ over $\mathbb{Z}$; a pivot equation $(z_i^{\prime }{)}^{s_i}=c_i^{\prime }$ succeeds exactly when $s_i$ divides every generator exponent of $c_i^{\prime }$, and a zero row requires $c_i^{\prime }=1$. Different W nodes compose these principal answers in the inherited substitution order. The mixed-unifier contract states soundness, factorization of every solution, exact failure, support control, and preservation of any finite protected set; the Smith policy fixes pivot, repair, sign, free-column, and fresh-name choices.

Free-abelian substitution laws, Smith reduction, solver termination/soundness/completeness/principality, composition of principal dimension solves, dimension-aware W soundness and principality, derivation-directed elaboration typing, capture-avoiding core substitution, typed annotation substitution, preservation, progress, and deterministic safety are proved in chapter 6. Coherent scale changes relate all closed outcomes: both sides produce $\mathsf{aritherr}$ or related values; at arrows the arguments themselves are related coordinate representations. Termination of all well-typed core terms uses the exact recursion-free signature.

The pinned Kappa companion in artifacts/ch6-dimension-inferencer/ traverses source syntax with disjoint supplies, generates a mixed equation store, solves rows having a coefficient that divides all the others, replays the returned substitution, infers the polymorphic square type in the empty environment, performs coherent arithmetic, and rejects mismatch and odd-pivot cases. For the coupled row $(2,3)$ of ${\delta }^2{ϵ}^3=L$, neither coefficient divides the other, so the run returns Unsupported. Its check-clean odd-pivot mutation is rejected by the oracle. The run proves none of the local metatheorems.