Dimension types and units of measure

Dimension expressions are finite-support exponent maps $d:\mathcal{B}\cup D\to \mathbb{Z}$. Multiplication, inverse, and integer power are pointwise addition, negation, and scalar multiplication. Compound units and source types are $$u::=u_0\mid uu\mid u^{-1}\mid u^n,\tau ::=\alpha \mid \mathsf{Num}[d]\mid \tau \to \tau ,\sigma ::=\mathrm{\forall }\overline{\alpha }\overline{\delta }.\tau .$$ The unit environment gives primitive units positive rational scales and closed dimensions and extends homomorphically to all four unit forms.

Ordinary and dimension variables are disjoint sorts. Formation is

$\alpha \in \mathcal{A}$

$\mathcal{A};D⊢\alpha \mathsf{type}$

$d:\mathcal{B}\cup D\to \mathbb{Z}\text{finitely supported}$

$\mathcal{A};D⊢\mathsf{Num}[d]\mathsf{type}$

$\mathcal{A};D⊢{\tau }_1\mathsf{type}$$\mathcal{A};D⊢{\tau }_2\mathsf{type}$

$\mathcal{A};D⊢{\tau }_1\to {\tau }_2\mathsf{type}$

Type equivalence extends dimension equality structurally, and conversion is $$\frac{\begin{array}{c}\mathrm{\Gamma }⊢e:\tau \\ \tau {=}_D{\tau }^{\prime }\end{array}}{\mathrm{\Gamma }⊢e:{\tau }^{\prime }}\mathrm{D}-\mathrm{Conv}.$$ The source terms and arithmetic rules are $$e::=x\mid q@u\mid \lambda x.e\mid ee\mid \mathsf{let}x=e\mathsf{in}e\mid e+e\mid e\ast e\mid e/e\mid e^{⟨n⟩},$$

${\mathcal{U}}^{\ast }(u)=(s_u,d_u)$

$\mathrm{\Gamma }{⊢}_{\mathcal{U}}q@u:\mathsf{Num}[d_u]$

$\mathrm{\Gamma }{⊢}_{\mathcal{U}}{e}_1:\mathsf{Num}[d]$$\mathrm{\Gamma }{⊢}_{\mathcal{U}}{e}_2:\mathsf{Num}[d]$

$\mathrm{\Gamma }{⊢}_{\mathcal{U}}{e}_1+e_2:\mathsf{Num}[d]$

$\mathrm{\Gamma }{⊢}_{\mathcal{U}}{e}_1:\mathsf{Num}[d_1]$$\mathrm{\Gamma }{⊢}_{\mathcal{U}}{e}_2:\mathsf{Num}[d_2]$

$\mathrm{\Gamma }{⊢}_{\mathcal{U}}{e}_1\ast e_2:\mathsf{Num}[d_1{d}_2]$

$\mathrm{\Gamma }{⊢}_{\mathcal{U}}{e}_1:\mathsf{Num}[d_1]$$\mathrm{\Gamma }{⊢}_{\mathcal{U}}{e}_2:\mathsf{Num}[d_2]$

$\mathrm{\Gamma }{⊢}_{\mathcal{U}}{e}_1/e_2:\mathsf{Num}[d_1{d}_2^{-1}]$

$\mathrm{\Gamma }{⊢}_{\mathcal{U}}e:\mathsf{Num}[d]$

$\mathrm{\Gamma }{⊢}_{\mathcal{U}}{e}^{⟨n⟩}:\mathsf{Num}[d^n]$

For $E=(d_i{=}_D{e}_i{)}_{i=1}^m$, list unknowns $\overline{\delta }=({\delta }_1,\dots ,{\delta }_n)$, put $$M_{ij}=d_i({\delta }_j)-e_i({\delta }_j),c_i=\prod _{b\in \mathcal{B}\cup G_r}{b}^{e_i(b)-d_i(b)},$$ and compute a Smith form $UMV=S$. With $z=V{z}^{\prime }$ and $c^{\prime }=Uc$, each pivot equation is $(z_i^{\prime }{)}^{s_i}=c_i^{\prime }$. It succeeds exactly when $s_i$ divides every generator exponent in $c_i^{\prime }$; a zero row requires $c_i^{\prime }=1$. Free columns become fresh dimension parameters, and back-substitution gives the principal substitution ${\rho }_E$. The deterministic policy chooses the first nonzero row-major pivot, uses canonical extended-Euclidean coefficients, repairs the first offending entry, makes pivots positive, and names free columns left to right from a globally fresh dimension supply.

The sorted type unifier $\mathsf{munify}$ decomposes arrows and ordinary variables as in HM and accumulates every $\mathsf{Num}[d]\doteq \mathsf{Num}[e]$ of one call into one dimension store. The dimension-aware inference judgment is ${\mathcal{I}}_{\mathcal{U}}(\mathrm{\Gamma },e)=(S,\tau )$. Besides inherited W, its exact binary clauses first compute $(S_1,{\tau }_1)=\mathcal{I}(\mathrm{\Gamma },e_1)$ and $(S_2,{\tau }_2)=\mathcal{I}(\mathrm{\Gamma }[S_1],e_2)$. Addition chooses fresh $\delta$, computes $$U=\mathsf{munify}({\tau }_1[S_2]\doteq \mathsf{Num}[\delta ],{\tau }_2\doteq \mathsf{Num}[\delta ]),$$ and returns $(S_1;S_2;U,\mathsf{Num}[\delta [U]])$. Multiplication and division choose fresh ${\delta }_1,{\delta }_2$, solve the corresponding two numeric equations, and return $S_1;S_2;U$ together with $$\mathsf{Num}[{\delta }_1[U]{\delta }_2[U]]\text{or}\mathsf{Num}[{\delta }_1[U]{\delta }_2[U{]}^{-1}].$$ Power computes $(S,\tau )=\mathcal{I}(\mathrm{\Gamma },e)$, solves $U=\mathsf{munify}(\tau \doteq \mathsf{Num}[\delta ])$, and returns $(S;U,\mathsf{Num}[\delta [U{]}^n])$.

The complete canonical core is where $\odot \in \{+,\ast ,/\}$. Core contexts contain monotypes only; C-Var and C-Let are monomorphic:

$\mathrm{\Delta }(x)=\tau$

$\mathrm{\Delta }⊢x:\tau$

$\mathrm{\Delta },x:\tau ⊢a:\upsilon$

$\mathrm{\Delta }⊢\lambda (x:\tau ).a:\tau \to \upsilon$

$\mathrm{\Delta }⊢a_1:\tau \to \upsilon$$\mathrm{\Delta }⊢a_2:\tau$

$\mathrm{\Delta }⊢a_1{a}_2:\upsilon$

$\mathrm{\Delta }⊢a_1:\tau$$\mathrm{\Delta },x:\tau ⊢a_2:\upsilon$

$\mathrm{\Delta }⊢\mathsf{let}x=a_1\mathsf{in}{a}_2:\upsilon$

The core numeric rules are

$\mathrm{\Delta }⊢{\bar{q}}_d:\mathsf{Num}[d]$

$\mathrm{\Delta }⊢a_1:\mathsf{Num}[d]$$\mathrm{\Delta }⊢a_2:\mathsf{Num}[d]$

$\mathrm{\Delta }⊢a_1+a_2:\mathsf{Num}[d]$

$\mathrm{\Delta }⊢a_1:\mathsf{Num}[d_1]$$\mathrm{\Delta }⊢a_2:\mathsf{Num}[d_2]$

$\mathrm{\Delta }⊢a_1\ast a_2:\mathsf{Num}[d_1{d}_2]$

$\mathrm{\Delta }⊢a_1:\mathsf{Num}[d_1]$$\mathrm{\Delta }⊢a_2:\mathsf{Num}[d_2]$

$\mathrm{\Delta }⊢a_1/a_2:\mathsf{Num}[d_1{d}_2^{-1}]$

$\mathrm{\Delta }⊢a:\mathsf{Num}[d]$

$\mathrm{\Delta }⊢a^{⟨n⟩}:\mathsf{Num}[d^n]$

$\mathrm{\Delta }⊢\mathsf{aritherr}:\tau$

The functional roots are $$(\lambda (x:\tau ).b)v⟶b[v/x],\mathsf{let}x=v\mathsf{in}b⟶b[v/x],$$ with capture-avoiding substitution. Compatibility decomposes $E$ into one-hole frames $F$: $F⟨r⟩⟶F⟨r^{\prime }⟩$ for a root step, and only $F⟨\mathsf{aritherr}⟩$ propagates in one step. Source elaboration is derivation directed. It inserts inferred lambda annotations and maps a generalized source-let declaration to a template $\theta \mapsto a[\theta ]$; each variable instance emits the specialized template, so no polymorphic value reaches the runtime core. Literal elaboration is $q@u\mapsto {\overline{q{s}_u}}_{d_u}$; the arithmetic and zero-domain roots are exactly those displayed in the owning chapter.