Repository navigation
Speculative Units and Dimensions
Speculative design. Open, not settled — thinking and proposals, not shipped behavior. See Roadmap for what's in flight.
Status: speculative (2026-10-01). Units should be something packages install, not something the engine holds globally: which units exist, which notation reads as one, and what they convert to all depend on context. Under every kind of unit, physical or algebraic, is a dimension, and one notion of dimension ties the two together. How packages enable things per scope is Package Scopes; this page is what they enable.
compute-engine ships a physical unit table today, global:
-
5\,\mathrm{m}parses toQuantity(5, m); -
3\,\mathrm{km} + 2\,\mathrm{m}evaluates to3.002 km; -
2\,\mathrm{N}is newtons, everywhere.
A bare m or N stays a free symbol, so it's the notation and the table inside Quantity that
are global. The hypercomplex units (i_k, j_k, ε_k, e_k) are subscripted symbols the
hypercomplex package declares globally (Package Scopes §4).
A dimension is what a quantity is graded by.
- Physical dimensions form a free abelian group: exponent vectors over the base dimensions (length, mass, time, …), with rational exponents where a field needs them (noise in V/√Hz). Dimensional analysis is arithmetic in that group.
-
Algebraic dimensions are the grading of an algebra's basis. For the hypercomplex
families it's the group (ℤ/2)ⁿ of Algebras, Units and Places §4,
where a basis element
u_Shas degree S.
Both are an algebra graded by an abelian group. The physical case is untwisted (units commute and multiply freely), and the hypercomplex case is twisted by a cocycle (squares, anticommuting pairs). So the unit infrastructure is one layer for both, with the algebraic one sitting slightly above the physical.
Linear units are a choice of scale. Each graded piece of a physical quantity is one-dimensional, and a unit picks a basis vector for it: the metre is a choice of basis for length. Derived units follow by multiplication (N = kg·m·s⁻²), and conversion is rescaling between two bases. (Tao: a unit is a one-dimensional coordinate system; §8.) For the hypercomplex families the basis is canonical up to sign, so there's no scale to choose: a unit there is just the basis element.
Affine and logarithmic units are charts with more to them.
-
Affine (Celsius, Fahrenheit): absolute temperature is a point in a one-dimensional
affine space, and a unit is a chart, a scale plus an origin. Differences are linear and
carry the kelvin's dimension;
20 °C + 30 °Cis ill-typed, while20 °C + 30 Kis a point. - Logarithmic (decibel, neper, pH): a chart through a log. A level (dBm, dB SPL) is a point relative to a reference; a gain is a difference, with no reference.
So "unit" in general is a chart on a graded piece, and a linear unit is the common special case whose chart is only a scale.
A package can:
- introduce dimensions (base or derived);
- introduce units, each defined from others (an exact factor, or an affine or log chart);
- depend on units another package introduced;
- introduce notation for them (
m,\mathrm{N},°C), and say whether it's enabled by default.
All of these join the kernel's overall set of units as installed. Notation is enabled per scope, like any other package notation (Package Scopes §1, §3).
Contradictory notation is ordinary and only matters when enabled together:
-
Nis the newton, Wolfram'sNand the natural numbers; -
Gis the gauss and the gravitational constant; -
ais the year (annum) and the are; -
Cis the coulomb, while°Cis a different unit again.
The ambiguity checks (Kernels and Front Ends §6) run over the enabled set, as for every notation.
A unit label isn't a symbol, and shouldn't print or read as one. A quantity prints as a box whose
unit part is a unit box carrying the unit's expression, the way a dressed shorthand carries its
head (Kernels §6: an InterpretationBox whose display is N and whose expression is the
newton). Printing never confuses a unit with a symbol, and copying a quantity gives back the
unit, not a letter. See Boxes.
Input still has to choose. A typed 2 N is a newton or a variable N times 2. Options:
-
A trigger: compute-engine already reads
2\,\mathrm{N}(thin space, upright) as a quantity, and an editor shortcut can insert the boxed unit directly. -
Scope: accept a bare
Nas the unit only where a units package is enabled and nothing else enabled claimsN.
Wolfram's $UnitSystem (Metric or Imperial) is close to this, but it's one global default. Ours
could be a set of enabled systems, allowed together when they govern disjoint base dimensions.
For example: SI for physical dimensions, bits and bytes for information, a currency for money,
pixels for a rendering environment.
A system for the physical dimensions should be any system, not just Metric or Imperial:
- SI;
- CGS-Gaussian, which has a different dimension group (charge is derived, so Maxwell's equations are written differently);
- natural or Planck units, which set c = ħ = 1, a quotient of the dimension group that collapses length, time and mass to one dimension.
So a system is a choice of basis per base dimension, possibly composed with a quotient of the
dimensions. That's why it's context in the strong sense: it changes what an expression means,
not only its numbers. (Tao calls the quotient "spending symmetry": in c = 1 units, E = m no
longer carries back to the full setting.) A simple default (SI for the physical family) keeps
the common case simple.
Each of these is a grading that isn't a physical base dimension, so it fits the same layer. All are later extensions, and some may turn out to belong to the algebra layer instead.
-
Angle as a dimension. With angle as its own dimension,
sintakes an angle, and a ratio that was never an angle is a type error, not silently accepted. It also tracks something algebraically useful: whether a ratio is trigonometric at all. Precedents: mp-units' strong angular system; Quincey's proposal to drop the radian's dimensionless status (§8). - Trigonometric depth. How many times a quantity has passed through a trigonometric transform, as a further graded tag on top of angle.
- Residual dimensions for ratios. m/m cancels to the trivial dimension, but a system could choose not to quotient: keep the formal pair (length, length⁻¹) as a grading that remembers where it came from, and collapse it only when asked. That's the same lever as c = ħ = 1, a choice of quotient, so it adds nothing new conceptually.
-
Infinitesimals. Dual numbers are already a hypercomplex family (
ε² = 0), so an infinitesimal is an algebraic unit with a nilpotent square, and its order is a grading. - Currency. Exchange rates behave like a gauge field: the rate between two currencies is a connection, a round trip through several markets is a holonomy (arbitrage when it isn't 1), and interest rates are the connection along time. An exploration for once the primitives are in place (§8).
Lean.
-
Mathlib has no units library that we found.
-
Physlib (formerly PhysLean) does:
-
Physlib/Units/Dimension.leanis a dimension as exponents over a chosen basis (LTMCT, ISQ, Gaussian-CGS), with a commutative group structure; -
Physlib/Units/WithDimmakes the dimension a type index on a quantity.
That's our physical half (§2): a free abelian group with the base set varying by system. No algebraic dimensions, no charts.
-
-
A separate Lean 4 formalisation of dimensional analysis, with Buckingham Pi: arXiv:2509.13142.
Charts: affine and logarithmic units.
| system | affine | logarithmic |
|---|---|---|
| mp-units (C++) | quantity points with explicit origins; point − point is a quantity | proposed: levels as points on a reference, gains as differences |
| Unitful.jl |
@affineunit; point + point raises AffineError
|
Level and Gain |
| Pint (Python) | offset units, delta_degC
|
beta |
| Wolfram |
DegreesCelsius vs DegreesCelsiusDifference
|
not checked |
| Boost.Units |
absolute<>, offset conversions |
none found |
| F# units of measure (Kennedy) | none found | none found |
Dimensions and algebra.
- Terence Tao, A mathematical formalisation of dimensional analysis (2012): dimensions as one-dimensional vector spaces, quantities transforming under a group of scalings, a unit as a one-dimensional coordinate system, natural units as "spending symmetry". The closest match to §2, §3 and §6.
- George Hart, Multidimensional Analysis (Springer, 1995): linear algebra with dimensioned matrices.
- Kitano, Mathematical structure of unit systems: unit systems as equivalence classes, dimension defined per class.
- Nothing found ties physical dimensions to an algebra's grading in the hypercomplex sense; as far as we've looked, that link is ours.
Angle.
- mp-units' strong angular system: angle is its own dimension and trigonometric functions take angles.
- Quincey, Angles in the SI: a detailed proposal (Metrologia, 2021).
- The other side of the debate: Brownstein, arXiv:1909.08389; Mohr and Shirley, arXiv:2203.12392.
Currency and gauge theory.
- Maldacena, The symmetry and simplicity of the laws of physics and the Higgs boson (2014): exchange rates as gauge potentials on links, interest rates along time, explicitly as an analogy.
- Ilinski, Physics of Finance (1997; book 2001): currency exchange as parallel transport, markets modelled as a gauge field, as a literal model.
- Malaney's thesis (1996): index numbers as connections on a fibre bundle; disputed (arXiv:2112.03460).
- Where §7 belongs. Angle and residual dimensions are unit-system questions; infinitesimals and trigonometric depth may be the algebra layer's.
- Dated conversions. An exchange rate isn't a constant; a conversion can depend on a date or a source, so a unit definition may need a parameter.
- The default physical system's dimension for angle. SI keeps the radian dimensionless; a strong-angle system doesn't. Which is our default, and how a scope switches.
- Input. Whether a bare unit letter is ever accepted, or only the trigger form (§5).
-
First slice.
- Wrap compute-engine's unit table as an installed package, enabled by default where physical
quantities are wanted. A scope that hasn't enabled it lowers a
Quantityparse back to a product (2\,\mathrm{N}to2 · N), as Package Scopes §3's filter does. - Put dimensions under it as data, so the hypercomplex
Unitfamilies can declare their grading in the same terms.
- Wrap compute-engine's unit table as an installed package, enabled by default where physical
quantities are wanted. A scope that hasn't enabled it lowers a