Type safe dimensional analysis in Haskell

July 16, 2017

Years ago my colleague Gustavo asked how I would represent physical units like m/s or kg*m/s^2 as types so the compiler can check that they match up and cancel correctly. F# supports this natively, but it felt weird to have it baked into the type system. It seemed too ad hoc, though I didn’t know of anything better.

Today I was thinking about this again, and I found a way to do it in Haskell. The main idea is to represent units of measure as function spaces. For example, the unit m/s can be encoded as the type Seconds -> Meters. The numerator becomes the return type, and the denominator the argument type. Function types can be composed to form more interesting units, such as Seconds -> Seconds -> Meters for acceleration. Products can be represented by higher-order functions. A special type class will enable us to easily convert a Double into a quantity with any units of measure and vice versa.

There are a handful of packages on Hackage for doing dimensional analysis. This article will demonstrate a simple, portable way to do it without relying on any language extensions. As we will see in Example 3, this implementation sometimes requires the programmer to provide proofs of unit equivalence (which can be tedious at times). This is less convenient than other libraries, but it’s an interesting exhibition of the power of vanilla Haskell.

Units as function spaces

First, we define some types for base units. We will never instantiate these types, so we don’t specify any constructors. They are only used for type checking.

data Meter
data Kilogram
data Second

Next, we need types which actually represent quantities with units. For the base units above, we define BaseQuantity as follows:

newtype BaseQuantity a = BaseQuantity Double

It’s just a wrapper for Double, but written as a phantom type. The type parameter a keeps track of the base unit. For example, BaseQuantity Meter is a type which represents a length.

A quotient a / b of two units a and b will be represented by the function space b -> a. For example, m / s becomes BaseQuantity Second -> BaseQuantity Meter. To make intentions clear, we formalize this idea as a type synonym:

type Quotient a b = b -> a

We also need a BaseQuantity for dimensionless quantities like π. We could define a new base type for this, but () does the job nicely:

type Dimensionless = BaseQuantity ()

We can also define multiplicative inverse a^-1 as the quotient 1 / a.

type Inverse a = Quotient Dimensionless a

A product a * b can be represented as a / b^-1:

type Product a b = Quotient a (Inverse b)

A helpful synonym to make square units like m^2 easier to read:

type Square a = Product a a

All quantities have some numeric value. We formalize this in Haskell using a type class:

class Quantity a where
  construct :: Double -> a
  destruct  :: a -> Double

The instance for base quantities is trivial, since BaseQuantity just wraps a Double:

instance Quantity (BaseQuantity a) where
  construct = BaseQuantity
  destruct (BaseQuantity x) = x

Quotients of quantities are quantities as well. To construct a Quotient from a Double, we define a function which destructs its argument, multiplies the result by the given Double, and constructs a quantity of the return type (the numerator unit). To destruct a Quotient, we first construct 1 in the denominator unit (the argument type), use the quotient to convert it into the numerator unit, and destruct the result.

instance (Quantity q, Quantity r) => Quantity (q -> r) where
  construct x = \y -> construct (x * (destruct y))
  destruct x = destruct (x (construct 1))

We need to define an axiom that allows us to rearrange quotients:

-- a / (b / c) = c / (b / a)
quotientAxiom :: (Quantity a, Quantity b, Quantity c) =>
  Quotient a (Quotient b c) -> Quotient c (Quotient b a)
quotientAxiom = construct . destruct

Exercise for the reader: Do we need this axiom, or is there a way to derive it without destructing any quantities? Alternatively, are there any other axioms we need?

And finally, we define the familiar arithmetic operations:

-- We can add two quantities of the same unit.
infixl 6 .+.
(.+.) :: Quantity a => a -> a -> a
(.+.) x y = construct $ (destruct x) + (destruct y)

-- We can subtract two quantities of the same unit.
infixl 6 .-.
(.-.) :: Quantity a => a -> a -> a
(.-.) x y = construct $ (destruct x) - (destruct y)

-- We can multiply any two quantities.
infixl 7 .*.
(.*.) :: (Quantity a, Quantity b) => a -> b -> Product a b
(.*.) x y = \z -> construct $ destruct (z y) * destruct x

-- We can divide any two quantities.
infixl 7 ./.
(./.) :: (Quantity a, Quantity b) => a -> b -> Quotient a b
(./.) x y = \z -> construct $ (destruct z) * (destruct x) / (destruct y)

Other primitive operations, such as comparison, can be defined similarly.

Examples

The examples below will use these helpful type synonyms:

type Length   = BaseQuantity Meter
type Mass     = BaseQuantity Kilogram
type Time     = BaseQuantity Second
type Area     = Square Length
type Velocity = Quotient Length Time

Example 1: Tracking units in types

Let’s calculate the area of a table.

tableWidth :: Length
tableWidth = construct 1.5

tableHeight :: Length
tableHeight = construct 2.5

tableArea :: Area
tableArea = tableWidth .*. tableHeight

Calculations with quantities are type safe. Suppose we defined the mass of the table:

tableMass :: Mass
tableMass = construct 150

Then the following is a type error:

tableArea :: Area
tableArea = tableWidth .*. tableMass
-- Error: Couldn't match type ‘Kilogram’ with ‘Meter’
-- Expected type: Area
-- Actual type: Product Length Mass

Example 2: Quantities as functions

Suppose we want to calculate how far a train will travel, given its velocity and the duration of the trip.

trainVelocity :: Velocity
trainVelocity = construct 30

tripDuration :: Time
tripDuration = construct 5000

Here we demonstrate the correspondence between quantities and functions. Velocity is a synonym for Length / Time, but it’s also a function from Time to Length. Given a Time, we can simply “apply” a Velocity to it to get a Length:

tripDistance :: Length
tripDistance = trainVelocity tripDuration

So multiplication of a / b by b is just function application.

Example 3: Manual proofs of unit equality

Let’s define a function that takes a Length and a Velocity and returns a Time. First try:

calculateDuration :: Length -> Velocity -> Time
calculateDuration distance velocity = distance ./. velocity
-- Error: Couldn't match type ‘Velocity -> Length’ with ‘BaseQuantity Second’
-- Expected type: Time
-- Actual type: Quotient Length Velocity

Haskell doesn’t know that Length / Velocity = Time. If this is indeed true, there will be a way to manipulate the program (without destructing the quantity) to make it type check by swapping arguments, defining new functions, using the quotientAxiom, etc. This is similar to what one would do in a proof assistant like Agda or Coq.

So we have:

distance ./. velocity :: Length / Velocity

Velocity is a type synonym for Length / Time, so we actually have:

distance ./. velocity :: Length / (Length / Time)

We can apply the quotientAxiom to get:

quotientAxiom (distance ./. velocity) :: Time / (Length / Length)

Under the interpretation of units as function spaces, we have:

quotientAxiom (distance ./. velocity) :: (Length -> Length) -> Time

We can apply id to cancel the Lengths and get a Time. Putting it all together:

calculateDuration :: Length -> Velocity -> Time
calculateDuration distance velocity = quotientAxiom (distance ./. velocity) id

Now we can calculate how long the trip from Example 2 would take if the train traveled at 40 m/s instead of 30 m/s.

fasterVelocity :: Velocity
fasterVelocity = construct 40

shorterDuration :: Time
shorterDuration = calculateDuration tripDistance fasterVelocity

Example 4: Destructing the results

When we are done calculating, we can convert the results back to Doubles with the destruct function. Let’s print the results of the first three examples:

main = do
  putStrLn $ "tableArea:       " ++ (show $ destruct $ tableArea) ++ " m^2"
  putStrLn $ "tripDistance:    " ++ (show $ destruct $ tripDistance) ++ " m"
  putStrLn $ "shorterDuration: " ++ (show $ destruct $ shorterDuration) ++ " s"

The output is:

tableArea:       3.75 m^2
tripDistance:    150000.0 m
shorterDuration: 3750.0 s

Conclusion

We can do type safe dimensional analysis by encoding units as function spaces. The basic pattern is:

Construct whatever quantities you want using the construct function. A type annotation can be used to specify the units, or you can let type inference figure out the units automatically.
Do type safe operations on these quantities using the operations .+., .*., etc. You may need to manually rearrange units or cancel them to satisfy the type checker, but this will always be possible if your units are actually correct (exercise for the reader: prove it!).
When you are done with calculation and want to use the resulting quantities, the destruct function will convert them into Doubles.

It’s inconvenient that we sometimes have to provide manual proofs of unit equivalence. It would be nice if rearranging and canceling units was completely automatic. But at least we have type safety!

Finding ambiguities in context-free grammars

What are covariance and contravariance?