I’ve recently been musing on the nature of units of measure within the context of type theory. Units of measure (or simply units), as used in dimensional analysis, are utilised for something very similar to types in programming languages: among other things ensuring that expressions are “well-typed” — you cannot add a distance to a duration, for instance. However, though their use complements traditional type systems, it is uncommon (though not unheard of) to encounter units of measure in programming languages. I want to take a brief look at exactly what a “unit of measure” is from a type theoretic perspective, as it’s not a topic I’ve found much discussion on: the various papers by Andrew Kennedy [K97] [K09] (the author of the technique in F#) are the most detailed I’ve found, though the actual implementation seems to take the curious approach of treating types and units as distinct sorts (without particular justification)1. The other issue with their approach stems from the decision to treat the units themselves as the types, rather than the dimension the unit measures. In the F# approach, for instance, it is not possible to add 3 millimetres to 5 feet or even to 1 centimetre.

3.0<millimeter> + 5.0<foot>  // error

I have an alternative type theoretic interpretation of units of measure, which I believe is more cohesive and representative of the use of units of measure (specifically in dimensional analysis).

Dimensions versus units

In dimensional analysis, one is concerned with performing some analysis (often through computation) of physical quantities (like time, or length, or mass, or acceleration, etc.). The important thing is that one doesn’t lose track of which physical quantity one is concerned with. You don’t want to accidentally end up with an area instead of a speed, or attempt to add a mass to a force.

The physical quantities with which the measurements are concerned are called the dimensions. The values these quantities can take are called denominate numbers, which are simply numbers with units of measure attached to them. The thing to note here is that the choice of unit for each dimension is not unique. For example, the values 5 metres, 3 centimetres and 8 yards all measure length. These units — metre, centimetre and yard — are all related: you can freely convert between them (usually in terms of ratios), and you can think of these units as ways of representing some “canonical length”.

This establishes a core facet of the type theory of units of measure. Different units may be compatible (that is, have the same type): the important property for enforcing safety is the dimension.

The algebra of dimensions

Taking the collection of all dimensions as a set, the dimensions form an abelian group under multiplication. Given two dimensions, such as length and time, we can form a new dimension, length × time (measured in a unit such as metre-seconds). Given any dimension, we can also form its inverse. A unit for the speed, metres per second, measures the product of the dimension length and the inverse of the dimension time. The order of multiplication is unimportant: length × time is the same dimension as time × length and the dimension (length × length) × length is the same as (length × length) × length. We also have an internal operations on dimensions: two values of the same dimension can be added or subtracted, for instance.

What does this look like from a type theoretic perspective? Informally speaking, if we consider a universe of types, \(\mathcal{U}\), as a category (the objects of which are types and whose morphisms are functions between those types), then we can embed the dimensions as types within the universe: Length, Time, Charge, Area, and so on. (Note that there might be multiple ways to refer to a dimension, such as Area or Length × Length, but these are all just names for the same dimension. We usually pick a set of base dimensions from which all other compound dimensions can be generated by multiplication, taking inverses, and exponentiation by rationals: and then the names we give compound dimensions are simply aliases.)

These “dimension types” are related. Together, they form a subcategory of our universe, known as a strict symmetric 2-group. The multiplication operation2 on dimensions appears as the tensor product in the category, with a special “unitless dimension”, referred to simply as 1 (some numeric type, whose exact form will depend on your type system).

So where do our units of measure appear? They form the type constructors for our dimension types. To do this, we have to pick a canonical unit for each dimension, which is the “internal representation” of the values of the type. (The choice is entirely arbitrary.) Then, each unit of measure constructor takes a number and constructs a value of the canonical unit using the respective conversion method. Since units of measure only appear as constructors, we don’t have any restrictions regarding different units measuring the same dimension interacting.

Implementation of units of measure

Units of measure, and dimensional analysis, in general is useful. It’s useful in programming languages too, but we don’t see them all too often (F# is a notable example of a general programming language that treats units of measure as a first-class component of the type system). How feasible is it to provide a type system for a programming language that is expressive enough to allow units of measure as a library feature, rather than something built into the compiler itself (like F#)?

I want to take a quick look at this from the perspective of Rust, which is a reasonably-typed language with a fairly expressive type system (including polymorphism, but without type operators).

We can represent the base dimensions straightforwardly:

// We're using unsigned 128-bit integers for our numeric values
// here, but we could feasibly use any "numeric" type, or even
// make it generic. See "Practical considerations" below.
type Canonical = u128;

// This is a trait that is simply used for identifying
// which types are dimension types.
trait Dimension {
    fn new(Canonical) -> Self;
    fn value(&self) -> Canonical;
}

struct Unitless(Canonical);

struct Length(Canonical);
impl Dimension for Length {
    fn new(c: Canonical) -> Self { Length(c) }
    fn value(&self) -> Canonical { self.0 }
}

struct Time(Canonical);
impl Dimension for Time {
    fn new(c: Canonical) -> Self { Time(c) }
    fn value(&self) -> Canonical { self.0 }
}

We can now also construct units of measure for our dimensions, in the form of constructor functions.

// We're choosing "metre" and "second" as our canonical base
// units here. SI units are not compulsory, but are good
// standard choices.

fn metres(m: Canonical) -> Length {
    Length(m)
}

fn decametres(dm: Canonical) -> Length {
    Length(dm * 10)
}

fn seconds(s: Canonical) -> Time {
    Time(s)
}

Now, we’re going to want to construct new dimensions using multiplication and inverses. We can do that using a polymorphic type.

use std::marker::PhantomData;

struct DimensionMultiply<S: Dimension, T: Dimension>(
    // We only want to store a single value, but we need
    // to keep some reference to the types it came from,
    // which is why we need the `PhantomData`s. This is
    // a Rust-specific nuance.
    Canonical,
    PhantomData<S>,
    PhantomData<T>,
);

impl<S: Dimension, T: Dimension> Dimension for DimensionMultiply<S, T> {
    fn new(c: Canonical) -> Self {
        DimensionMultiply(c, PhantomData, PhantomData)
    }
    fn value(&self) -> Canonical { self.0 }
}

struct DimensionInverse<T: Dimension>(
    Canonical,
    PhantomData<T>,
);

impl<T: Dimension> Dimension for DimensionInverse<T> {
    fn new(c: Canonical) -> Self {
        DimensionInverse(c, PhantomData)
    }
    fn value(&self) -> Canonical { self.0 }
}

This all works so far, but we can already see a problem: we don’t have uniqueness of dimensions. To pick one example, the dimension for speed, Length / Time, can be represented in multiple different ways.

// We can define derived units using type aliases.
type Speed1 = DimensionMultiply<Length, DimensionInverse<Time>>; // Speed
type Speed2 = DimensionMultiply<DimensionInverse<Time>, Length>>; // ...also Speed...
type Speed3 = DimensionInverse<DimensionMultiply<Time, DimensionInverse<Length>>>; // ...and again...

Note that having explicit conversions between these representations isn’t enough: these dimension types are not just isomorphic, they’re actually identical. From an implementation point-of-view, we need to somehow normalise dimensions. Techniques for this exist, but to apply these at a library level at the very least you need type-level functions (or some way to assert equality of [ostensibly different] types, providing conversion methods that are unlikely to be automatically checked for correctness).

Let’s pretend we can get around this issue somehow. We then can provide operations on values of dimension types.

use std::ops::{Add, Sub, Mul, Div};

// These examples don't actually work in Rust, where you
// cannot implement a trait for every (bounded) type like
// this, but this is what it might look like if you could.
impl<T: Dimension> Add for T {
    type Output = T;

    fn div(self, rhs: T) -> Self::Output {
        Self::new(self.value() + rhs.value())
    }
}

impl<T: Dimension> Sub for T {
    type Output = T;

    fn div(self, rhs: T) -> Self::Output {
        Self::new(self.value() - rhs.value())
    }
}

impl<S: Dimension, T: Dimension> Mul<T> for S {
    type Output = DimensionMultiply<S, T>;

    fn div(self, rhs: T) -> Self::Output {
        // The `new` method on `Dimension` is
        // defined to take a canonical value.
        // This locks us into ensuring consistency
        // of canonical representation: we can't
        // measure `Distance` in metres, `Time`
        // in seconds, but then measure `Speed` in
        // feet per nanosecond, but it means that we
        // can derive the various operations
        // automatically.
        DimensionMultiply::new(self.value() * rhs.value())
    }
}

impl<S: Dimension, T: Dimension> Div<T> for S {
    type Output = DimensionMultiply<S, DimensionInverse<T>>;

    fn div(self, rhs: T) -> Self::Output {
        DimensionMultiply::new(self.value() / rhs.value())
    }
}

Here, I’m making use of associated types, a form of which you’re going to need to define such operations. We’re a way beyond Rust’s capabilities now, but in a type system based on something about as expressive as System-Fω, it’s plausible we could get this far. Once we’re here, we’re effectively done (save perhaps some nice synactic sugar for the units). The representation here does support only dimensions with integer powers, but with type-level rationals, you could extend this representation to rational powers fairly naturally.

Practical considerations

My goal here was to describe a type theoretic model for units of measure. In an abstract setting, this model seems to fulfil our expectations. When working with units of measure practically, in a programming language, we need to take a little care regarding the data type we use to represent the dimensional types. From a theoretic standpoint, picking an arbitrary canonical unit (such as metre for Length) is entirely reasonable, as we assume that we’re working with unlimited precision. This is not a luxury we can afford in an implementation, of course, so the representation of the value of dimension types requires a little more care. Ultimately, this comes down to the same questions as working with numeric types generally: how important do we expect precision to be (for example, should users have to accept that adding 5 feet to 3 metres will be prone to rounding, or do we want a more precise representation).

This consideration is separate from the type theoretic interpretation, so I’m not going to dwell on it, but it’s certainly a point of which to be aware. In an extreme case, to avoid these implicit conversions, one could separate the incompatible units of measure (that is, those units of measure that cannot be precisely converted into one another) into separate types: for example, treating foot as a unit of a synthetic dimension Feet, effectively reducing the unit of measure system to one mirroring F#’s.

Conclusion

To sum it all up, I’ve proposed that:

  • The dimensions in dimensional analysis correspond to types.
  • Units of measure are constructors for dimension types.
  • Dimension types form a strict symmetric 2-group as a subcategory of a (typical) category of types.
  • With the ability to define type-level functions, it should be possible to implement units of measure as a library, rather than a language feature.

I think this demonstrates a satisfying justification for why dimensional analysis looks so intuitively like type-checking. What’s more, the complexity is not as great as might be imagined. I’d very much like to see an increase in the prevalence of type-checked systems for units of measure in programming languages, which I feel is an area of computation that (regrettably) often gets ignored by type systems.

I don’t think this is the end of interesting questions in the type theory of units of measure. I’m curious to see whether there are useful extensions of dimension types to non-numeric values, for one (straying decidedly away from physical meaning into the abstract3). Perhaps with an intuitive model for such types, others will be encouraged to investigate further…

  1. This causes issues from a language point-of-view, because constructions on types don’t automatically carry over to units, as you’d expect. You’re forced either to implement the same features twice, for both types and units, or forbid your users from using them in the same ways as each other. ↩

  2. Although I’m using the symbol “×” here, the operation is not the same as the product of types (which is also often denoted with the same symbol). If you consider the dimensional multiplication of any two types, versus their type theoretic product, this is easy to see: 5 metre-seconds is a value of the dimensional multiplication of length and time; whereas the pair (3 metres, 1 second) is a value of the type theoretic product of length and time. The dimensional multiplication combines the numeric components of the values (by the usual notion of multiplication), whereas the type theoretic product preserves the denominate numbers as components of a pair. ↩

  3. Naturally, the way things ought to be. ↩