Units of Measure
A breadth-first survey of units of measure — the mathematics of physical quantities and dimensional analysis (quantity calculus, the Buckingham π theorem, free abelian groups of dimensions, tensor lines, torsors, dimensioned algebra, and Kennedy's type-theoretic line), and the twenty checked-units systems real ecosystems ship, from compiler-native (F#, GNAT) through static library encodings (Rust, C++, Haskell, D) and dependent types (Lean) to dispatch-time (Julia), runtime registries (Python), and symbolic engines (Wolfram / MATLAB). The goal is a grounded map of the design space to inform a future Sparkles quantities library: the repo's constraints — templates + CTFE, @safe pure nothrow @nogc cores, Expected-based error handling — select a specific region of that space, and the survey closes with the delta (comparison, Part IV), the D prior art (d-quantities), and thirteen CI-verified runnable D prototypes (examples/).
This survey answers seven questions:
- What is a quantity — and what, exactly, is wrong with
1 m + 1 s? The metrology vocabulary (VIM, SI Brochure, UCUM, QUDT) and the six-account orientation ledger for the survey's central prohibition. See concepts. - What are the classical results? The π-theorem as rank–nullity over the dimension matrix — with the hypotheses folklore elides — and the free-abelian-group skeleton every library implements. See buckingham-pi and free-abelian-group.
- What are the rigorous formalizations of "quantity"? Whitney's rays and birays, Tao's tensor of lines, the torsor/weight-space picture, and Hart's dimensioned linear algebra — with what each takes as primitive. See the theory subtree.
- How does the algebra become a type system? Kennedy's line — types-as-invariance, AG-unification, erasure — and the six mechanism families that encode the group in real checkers. See kennedy-types and type-system-mechanisms.
- How do real ecosystems package this? Twenty systems, from the one compiler with the theory built in to registries and symbolic engines. See the master catalog.
- What does the field agree on, and where does it split? Seven consensus points, nine genuinely open trade-off axes, and a candidate unifying hypothesis (quantities as a graded object) tested against the evidence. See the comparison.
- Where would a Sparkles units library sit? The D evidence — two complete prior designs, thirteen runnable prototypes — and the open decisions a
docs/specs/proposal must make. See comparison, Part IV, d-quantities, and the prototypes.
NOTE
Scope: foundations, vocabulary, and twenty flagship systems (waves 1–2). The theory subtree (eight deep-dives), the concepts glossary, the twenty system pages below, the comparison capstone, and the three CI-verified D prototypes are landed. Wave 2 has now landed six further system pages — the Scala libraries (coulomb + squants), Nim's unchained, Swift's Foundation Measurement, Kotlin's measured, and the UCUM / QUDT interchange implementations — taking the catalog from fourteen to twenty systems. Several systems are covered as in-page asides rather than own rows: astropy.units (inside python-pint), Eisenberg's units package (inside haskell-dimensional), std::chrono (inside cpp-boost-units), nordlow/units-d (inside d-quantities), NeedleInAJayStack/Units (inside swift-units), and the JSR-385 indriya / unit-api layer (inside ucum-qudt). Other-language units libraries remain out of scope for now; the UCUM spec and the QUDT ontology themselves are covered in concepts as the interchange and data poles of the design space.
Last reviewed: July 4, 2026
Foundations (theory)
The formalizations, each developed in its own deep-dive. Start with the concepts glossary for the shared vocabulary, then the theory umbrella for the organizing question (what is wrong with 1 m + 1 s, and what is primitive) and the cross-cutting splits.
| Topic | What it pins down | Canonical sources | Link |
|---|---|---|---|
| Concepts & vocabulary | VIM/SI/UCUM/QUDT definitions; the one-prohibition-six-accounts ledger; the affine/logarithmic/angle edge cases | VIM 3rd ed.; SI Brochure 9th ed.; NIST SP 811; UCUM; QUDT | concepts |
| Buckingham π via linear algebra | the π-theorem as rank–nullity over ℚ + one analytic step; the hidden-hypotheses ledger | Vaschy 1892; Buckingham 1914; Bridgman 1922; Drobot 1953; CLP 1982 | pi |
| Whitney's quantity structures | quantities-first axiomatics; the Q ≅ ℝ × ℚⁿ representation theorem; the unresolved exponent ring | Whitney 1968 (Monthly I & II); Raposo 2018/2019; Jonsson 2021 | whitney |
| Free abelian group | dimensions as exponent vectors (ℤⁿ/ℚⁿ); two GL-actions; what ℤ → ℚ buys and breaks | Kennedy 1996; Jonsson 2020/2021; Zapata-Carratalá 2021; the Lean repo | fag |
| Tensor of lines | base dimensions as 1-D lines; units as basis vectors; inconsistency as unwritability | Tao 2012; Janyška–Modugno–Vitolo 2007 | tensor |
| Torsor / scaling torus | homogeneity = equivariance under (ℝ⁺)ⁿ; units = torsor points; trivialization never canonical | Baez; Tao 2012; Zapata-Carratalá 2021; Jonsson 2021 | torsor |
| Kennedy's types | principal types via unitary AG-unification; parametricity = invariance under rescaling; erasure | Wand & O'Keefe 1991; Kennedy 1994/1996/1997/2010 | kennedy |
| Hart's multidimensional analysis | dimensioned linear algebra: multipliable ⇔ dimensionally rank-1; most of matrix theory breaks | Hart 1994 (SIAM) & 1995 (Springer); Zapata-Carratalá 2021 | hart |
| Type-system mechanisms | the theory→systems bridge: six encodings of the group; the checker evaluates vs solves | Kennedy 2010; Gundry 2015; the pinned system source trees | mech |
Systems master catalog
One row per surveyed system — the identity and classification columns only. Checked is when a mismatch is reported: at compile time, at elaboration (proof assistant), per JIT dispatch specialization, at run time, or only on an explicit opt-in query. Exponents is the dimension group's exponent domain as shipped. Kind is whether same-dimension, different-kind quantities (Hz vs Bq, torque vs energy) are distinguishable. The full per-dimension comparison — affine and logarithmic support, polymorphism, erasure evidence, diagnostics, compile cost — is the comparison's at-a-glance matrix; this catalog is who-is-who.
| System | Ecosystem | Mechanism | Checked | Exponents | Kind | Link |
|---|---|---|---|---|---|---|
| F# units of measure | F# / .NET | native AG unifier in the compiler's constraint solver | compile | ℚ¹ | —² | fsharp-uom |
| uom-plugin | Haskell (GHC) | typechecker-plugin AG unifier over an uninterpreted Unit kind | compile | ℤ³ | — | haskell-uom-plugin |
| dimensional | Haskell | closed type families over a fixed 7-slot Dimension kind | compile | ℤ⁷, closed basis | —⁴ | haskell-dimensional |
| uom | Rust | macro-generated Quantity over typenum trait arithmetic | compile | ℤ⁷ | flat Kind tags⁵ | rust-uom |
| dimensioned | Rust | make_units! systems over typenum tarr! exponent arrays | compile | ℤⁿ per system⁶ | — | rust-dimensioned |
| mp-units | C++20/23 | consteval symbolic expressions (constexpr values of empty types) | compile | ℚ, open basis | quantity_spec hierarchy⁷ | cpp-mp-units |
| Boost.Units | C++03 | MPL typelists of (base dimension, static_rational) pairs | compile | ℚ, open basis | extra base dimensions⁸ | cpp-boost-units |
| Au | C++14 | canonicalized variadic packs + a prime/π magnitude vector space | compile | ℚ, open basis | —⁹ | cpp-au |
| quantities / std.units | D | CTFE dimension values · units-as-types conversion graph | compile¹⁰ | ℚ (all artifacts) | — | d-quantities |
| Pint | Python | runtime UnitRegistry + exponent dictionaries | run | ℚ, open basis | — | python-pint |
| Unitful.jl | Julia | Rational{Int} exponents as type parameters, multiple dispatch | dispatch¹¹ | ℚ, open basis | — | julia-unitful |
| GNAT dimensionality | Ada (GNAT-only) | implementation-defined aspects; ℚ vectors on AST nodes | compile | ℚ, ≤ 7 dimensions | — | ada-gnat-dimensions |
| LeanDimensionalAnalysis | Lean 4 | dependent types; CommGroup (dimension B E) proved, not encoded | elaboration | open ring¹² | — | lean-mathlib-units |
| Wolfram / MATLAB | Wolfram Lang. · MATLAB | symbolic Quantity data · inert symunit factors | run / opt-in¹³ | ℤ observed | temperature only¹⁴ | wolfram-matlab |
| coulomb | Scala | opaque-type Quantity[V,U]=V + reflective-macro canonicalization (cansig) | compile | ℚ | —¹⁵ | scala-coulomb |
| squants | Scala | runtime values; a dimension is a distinct final class; F-bounded nominal typing | compile¹⁶ | n/a (nominal) | nominal (free)¹⁷ | scala-squants |
| unchained | Nim | compile-time-only macros over an integer QuantityPower array | compile | ℤ | — | nim-unchained |
| measured | Kotlin | Measure<T:Units> with nested UnitsProduct/UnitsRatio generics (no normalization) | compile | ℤ (structural)¹⁸ | — | kotlin-measured |
Foundation Measurement | Swift | nominal Measurement<UnitType:Unit>; per-quantity Dimension subclass | compile¹⁹ | n/a (nominal) | nominal | swift-units |
| UCUM / QUDT | JVM · JS | UCUM string-grammar canonicalization / QUDT dimension-vector IRI; JSR-385 type-API | run | ℤ (7–8-slot) | — | ucum-qudt |
¹ Surface syntax defaults to integers, but parenthesized kg^(1/2) parses and the shipped solver is rational throughout — diverging from Kennedy's published ℤ design. ² 5.0<Hz> + 3.0<Bq> type-checks; the stdlib's own SI.fs defines both as second^-1. ³ Solver-side ℤ; the surface ^: family takes only Nat (negative powers via /:, fractional powers inexpressible). Final release 0.4.0.0 (2022); GHC 9.0–9.4 only. ⁴ DTorque = DEnergy and DActivity = DFrequency are type synonyms by construction. ⁵ Kinds separate Hz/Bq, torque/energy, and temperature point/interval, but reset to the default kind under ×/÷ — comparability tags, not algebra. ⁶ Gaussian half-integer dimensions handled by rescaling the basis (SqrtCentimeter); dormant since 2022. ⁷ The field's most developed kind system: lowest-common-ancestor addition, a four-level conversion lattice, kind algebra closed under */÷. ⁸ Nine-base-unit SI (radian, steradian) makes torque ≠ energy, but Bq = Hz survives. ⁹ Explicit policy ("No plans at present to support"); Angle/Information ship as extra base dimensions instead. ¹⁰ Plus a run-time twin: quantities' QVariant throws DimensionException (GC + exceptions); all three D artifacts are dormant. ¹¹ Resolved per JIT specialization: a mismatch compiles to an unconditional throw, a match to bare arithmetic — a third category between compile and run. ¹² Any CommRing E — ℝ exponents type-check; the artifact is theorems (noncomputable), not executables. ¹³ Wolfram checks eagerly at evaluation ($Failed on incompatibles); MATLAB checks only on an explicit checkUnits query returning logicals, never raising. ¹⁴ Wolfram curates DegreesCelsius vs DegreesCelsiusDifference; MATLAB defaults all temperatures to differences. ¹⁵ coulomb has NO Kind mechanism — torque/energy, Hz/Bq, angle/ratio are unguarded (the sharpest contrast with uom's Kind). ¹⁶ squants rejects Power + Energy at compile time as an ordinary nominal type mismatch; value + scale-conversion are runtime. ¹⁷ nominal typing gives kind-vs-dimension for free — Torque ≠ Energy despite identical dimension. ¹⁸ Kotlin has no type-level integers; composite dimensions are nested generic types (A·B ≠ B·A), not a normalized exponent vector; no fractional powers. ¹⁹ Foundation catches m + s as a generic-parameter mismatch, but there is no product type (m·s is unnameable); the typed third-party contrast on the same page (NeedleInAJayStack/Units) is runtime-thrown — neither is a full type-level exponent algebra.
Runnable prototypes
Thirteen single-file D programs co-located with this tree, compiled and run by the repository's ci helper on every pass; each header cross-links the theory or system page it demonstrates. The first three are zero-dependency and pin the core mechanism:
quantity-zn-graded.d— a minimalℤ³-gradedQuantity: the dimension is its unique normal form as a template value parameter;metres + secondsis a checked rejection viastatic assert(!__traits(compiles, …)).quantity-rational-exponents.d— theℚⁿvariant: CTFE-gcd-normalized rational exponents makesqrttotal (sqrt(m²)is the length type) whilem^(1/2) + mstays rejected.quantity-erasure.d— representation-level erasure machine-checked (sizeof/alignof/offsetof/array layout), with the codegen-identity honesty boundary stated.
Ten more are motivated by a physically-based raytracer and, where relevant, composed with sparkles:math's Vector; they prototype the remaining design-space axes:
quantity-affine-torsor.d— affinePoint3vsDisplacementvsDirectionandRay.at(Length t);Point + Pointandscalar · Pointrejected (composition ordering A:Quantity!(dim, Vec3)over the realVector).quantity-kind-tags.d— a flatKindtag orthogonal to the exponent vector (Hz≠Bq, plane-angle ≠ ratio); kind erased under×/÷.quantity-nominal.d— a distinct struct per quantity (kind for free), hand-wired products, undeclared product unnameable; poorVectorreuse shown.quantity-runtime-expected.d— a runtime dimension value; fallible ops return anExpected(m + sis a runtimeerr, not a throw).quantity-unit-in-type.d— the unit (rational scale) lives in the type;nm + mconverts lazily at the boundary, not eagerly at construction.quantity-diagnostics.d— a CTFE pretty-printer emits domain-languagestatic assertprose, contrasted with the raw mangled encoding.quantity-polymorphism.d— dimension-aware genericdot/cross/magnitude/normalize; forward IFTI inference works, the invert-from-result ceiling does not.quantity-open-basis.d— an open(name, exp)dimension basis; mint a custom base dimension without editing a closed vector core.quantity-logarithmic.d— EV/stops and dB: log-domain add = linear-domain multiply; why logarithmic units resist the exponent-vector model.quantity-vector-composition.d— units ⋈ linear algebra, head to head:Vector!(Quantity, N)is blocked today (theisNumeric!Tconstraint) while an element-genericVecworks, yielding a co-design recommendation forsparkles:math(see the comparison capstone).
Taxonomy
By checking time
The survey's most load-bearing axis (comparison reads the matrix along it): when is a dimensional mismatch reported, and by whom.
| Checking time | The contract | Systems |
|---|---|---|
| Compile — compiler-native | the language's own type checker / semantic pass reports the mismatch | F# (AG unifier), GNAT (sem_dim aspects) |
| Compile — compiler plugin | a plugin extends the stock solver with the abelian-group theory | uom-plugin |
| Compile — library encoding | the host's generic-programming machinery evaluates the group; no solver | dimensional, uom, dimensioned, mp-units, Boost.Units, Au, D artifacts, coulomb, squants, unchained, measured, Foundation Measurement |
| Elaboration (proof assistant) | homogeneity is a proposition; the output is theorems, not executables | Lean |
| Dispatch / specialization | the check resolves per JIT specialization — mismatch compiles to a throw | Unitful.jl |
| Run | checked when two quantities actually meet (registry / symbolic evaluation) | Pint, Wolfram, UCUM / QUDT |
| Opt-in query | arithmetic never checks; an explicit call reports a logical verdict | MATLAB symunit |
By exponent domain
Theory published ℤ; practice shipped ℚ (comparison § exponents); the free-abelian-group page tallies what the extension costs.
| Exponent domain | Systems | The documented cost / benefit |
|---|---|---|
ℤ — closed 7-vector | dimensional, UCUM / QUDT (7–8-slot) | sqrt of a non-square dimension is a compile error ("fractional powers make little physical sense") |
ℤ — per-system vectors | uom, dimensioned, uom-plugin, unchained, measured (structural) | Length.sqrt() rejected; √Hz named future work; Gaussian basis rescaled to stay integral |
ℚ — capped basis | GNAT (≤ 7 dimensions) | Sqrt halves vectors; ** requires a static exponent |
ℚ — open basis | F#, mp-units, Boost.Units, Au, D, Pint, Unitful, coulomb | total sqrt and honest √Hz — at the price of freeness, perfect squares, and gcd structure |
| Open ring | Lean | any CommRing E; nothing enforces the physics convention against ℝ |
ℤ observed (uncommitted) | Wolfram / MATLAB | captures show integer powers only, with no stated bound |
| Nominal — no exponent vector | squants, Foundation Measurement | a dimension is a class / generic-parameter identity, not an exponent tuple — there is no domain to have |
By kind treatment
The four-rung ladder from comparison § kinds — no rung is derived from theory, and QUDT (kind above dimension, as data) sits off-ladder.
| Rung | Mechanism | Systems |
|---|---|---|
| 1 — nothing | the dimension vector is the whole identity; Hz + Bq passes | F#, GNAT, dimensional, dimensioned, uom-plugin, Pint, Unitful, Lean, D artifacts, coulomb, unchained, measured, UCUM / QUDT |
| 2 — extra base dimensions | mint an axis; splits torque/energy but never Hz/Bq | Boost.Units (radian/steradian), Au (Angle, Information), Wolfram (angle/solid-angle/information/money/person axes) |
| 3 — flat tags | nominal comparability tags, erased under ×/÷ | uom |
| 4 — propagating hierarchy | a quantity_spec tree: LCA addition + a conversion lattice | mp-units |
| Nominal — kind for free | same-dimension quantities are distinct nominal types, so Torque ≠ Energy with no tag (off-ladder) | squants, Foundation Measurement |
Milestones
A timeline interleaving theory / formalization milestones with system / tooling milestones. Every date below is grounded in a landed page of this tree (per-result provenance in each page's Sources); uncertain entries are marked *.
| Year | Theory / formalization milestone | System / tooling milestone |
|---|---|---|
| 1892 | Vaschy states the π-theorem (buckingham-pi) | — |
| 1914 | Buckingham names it, proving "for special cases" under a sum-of-monomials postulate | — |
| 1922 | Bridgman — Dimensional Analysis: complete equations, the tacit single-relation restriction | — |
| 1953 | Drobot — the first fully rigorous algebraic foundation | — |
| 1968 | Whitney — The Mathematics of Physical Quantities I & II (whitney) | — |
| 1982 | Curtis–Logan–Parker — the π-theorem as frames + group action, no smoothness | — |
| 1991 | Wand & O'Keefe — dimensional inference "fits neatly" into ML type inference | — |
| 1994 | Kennedy — Dimension Types (ESOP); Hart — dimensioned matrices (SIAM) | ML Kit extension — the first implementation of Kennedy's dimension types (kennedy-types) |
| 1995–1997 | Kennedy's thesis (TR-391, 1996) and POPL '97 parametricity; Hart's Springer book (1995) | — |
| 2003 | — | Schabel's MPL dimensional-analysis demo — Boost.Units' origin (cpp-boost-units) |
| 2007 | Janyška–Modugno–Vitolo — positive spaces (arXiv, Oct) | Boost.Units formal review (Feb; after a factor-of-10 compile-time rewrite) |
| 2008 | — | Boost.Units 1.0.0 ships in Boost 1.36 (Aug), ℚ exponents from the start |
| 2010 | Kennedy's CEFP notes — the shipped F# design, didactically (kennedy-types) | Boost.Units feature-frozen (v1.2, Boost 1.43) |
| 2011 | — | Nadlinger's std.units Phobos RFC (Apr) and push (Dec) — never formally reviewed (d-quantities) |
| 2012 | Tao — the tensor-of-lines / weight-space essay (Dec) (tensor-of-lines) | GNAT dimensionality aspects presented (HILT 2012*); Mathematica 9.0 ships Quantity (wolfram-matlab) |
| 2013 | — | quantities — D's CTFE value-level design (Sicard, 2013–2020) (d-quantities) |
| 2014 | Atkey — parametricity → conservation laws, closing Kennedy's POPL '97 conjecture | — |
| 2015 | Gundry — the GHC typechecker-plugin AG unifier (haskell-uom-plugin) | dimensioned 0.5.0 moves to typenum (Dec) (rust-dimensioned) |
| 2016 | — | units-d fork created the day the std.units thread ends (30 Mar) (d-quantities); Foundation Measurement ships with Swift 3* (swift-units) |
| 2017–2018 | — | MATLAB symunit/checkUnits (R2017a); unitConvert (R2018b) |
| 2018–2019 | Raposo — the algebraic structure of quantity calculus, I & II (whitney) | — |
| 2020–2021 | Jonsson (2020 π-foundation; 2021 scalable monoids); Zapata-Carratalá — dimensioned algebra | mp-units P1935R2 before WG21 (2020) (cpp-mp-units); squants v1.8.3 — last tagged release (Aug 2021) (scala-squants) |
| 2022 | — | uom-plugin 0.4.0.0 final (Oct; GHC 9.0–9.4, then dormant); dimensioned 0.8.0 final (Apr) |
| 2023 | — | P2980R1 — the C++29 standardization plan; JSR-385 unit-api v2.2 (May) (ucum-qudt) |
| 2025 | Bobbin et al. — the Lean 4 formalization (arXiv, Sep) (lean-mathlib-units) | mp-units v2.5.0 (Dec); coulomb v0.9.1 (Sep) (scala-coulomb) |
| 2026* | — | P3045R8 — Quantities and units library (WG21); Kotlin measured v0.5.0 (Apr) (kotlin-measured); indriya v2.2.4, the JSR-385 RI (May) (ucum-qudt); current pins as reviewed: uom 0.38.0, Unitful 1.28.0, Pint 0.25.3 |
* The HILT 2012 attribution (Pucci & Schonberg) is stated on the GNAT page but has no local artifact behind it; the Swift 3 / macOS 10.12 date for Foundation Measurement is the platform era, not a pinned release; 2026 entries are current-as-of-review (July 2026).
Quick navigation
Suggested reading paths
- "I'm designing the Sparkles units library." concepts → kennedy-types + type-system-mechanisms → d-quantities → comparison § Part IV (the Sparkles delta and open decisions) → the runnable prototypes and their side-by-side evaluation (what to take from each).
- "I want the mathematics." concepts → whitney → tensor-of-lines → torsor-representation → hart-multidimensional → comparison § Part II (the graded-algebra hypothesis, tested).
- "I'm implementing a units library (any language)." free-abelian-group → type-system-mechanisms → fsharp-uom (the inference ceiling) → cpp-mp-units (kinds, affine, engineered diagnostics) → rust-uom (the evaluator mainstream) → comparison § Part III.
- "Just the π-theorem." buckingham-pi → free-abelian-group (the kernel lattice) → python-pint (a shipped
pi_theoremsolver). - "The metrology / interchange view." concepts (VIM, SI, UCUM, QUDT) → wolfram-matlab (curated corpora) → python-pint (registry-as-data).
Synthesis
- Concepts & vocabulary — the metrology-grounded glossary + the one-prohibition-six-accounts ledger.
- Theory umbrella — the organizing question, the catalog, and the primitive / exponent-ring / semantic-vs-syntactic splits.
- Comparison — the formalizations reconciled, the graded-algebra hypothesis tested, the at-a-glance matrix, the consensus, and the Sparkles delta.
- Prototype evaluation — the thirteen runnable D probes compared across the design axes, with what a Sparkles units library should take from each.
Sources
Each deep-dive carries its own primary-source citations — papers and books (pinned as local artifacts, with editions and page numbers), SHA-pinned source trees for every surveyed implementation, vendor-doc captures where a system is closed-source, and local reproductions (compiler transcripts, codegen diffs) for the load-bearing behavioural claims. The authoritative artifacts behind this index's classifications are:
- Foundational theory — Buckingham 1914; Bridgman 1922; Drobot 1953; Whitney 1968; Curtis–Logan–Parker 1982; Wand & O'Keefe 1991; Kennedy 1994–2010; Hart 1994/1995; Janyška–Modugno–Vitolo 2007; Tao 2012; Gundry 2015; Raposo 2018/2019; Jonsson 2020/2021; Zapata-Carratalá 2021; Bobbin et al. 2025 — as cited in the theory subtree.
- Metrology primaries — the VIM (JCGM 200:2012), the SI Brochure (9th ed.), NIST SP 811, the UCUM specification, and the QUDT ontology — as quoted in concepts.
- Per-system sources — the pinned project source trees, official docs, and papers cited in each linked system page.