July 16, 2017
Years ago my colleague Gustavo asked how I would represent physical units like
kg*m/s^2as 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/scan 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 -> Metersfor acceleration. Products can be represented by higher-order functions. A special type class will enable us to easily convert a
Doubleinto 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
newtype BaseQuantity a = BaseQuantity Double
It’s just a wrapper for
Double, but written as a phantom type. The type parameter
akeeps track of the base unit. For example,
BaseQuantity Meteris a type which represents a length.
a / bof two units
bwill be represented by the function space
b -> a. For example,
m / sbecomes
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
BaseQuantityfor 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^-1as the quotient
1 / a.
type Inverse a = Quotient Dimensionless a
a * bcan be represented as
a / b^-1:
type Product a b = Quotient a (Inverse b)
A helpful synonym to make square units like
m^2easier 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
BaseQuantityjust wraps a
instance Quantity (BaseQuantity a) where construct = BaseQuantity destruct (BaseQuantity x) = x
Quotients of quantities are quantities as well. To construct 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
1in 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.
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 weight 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.
Velocityis a synonym for
Length / Time, but it’s also a function from
Length. Given a
Time, we can simply “apply” a
Velocityto it to get a
tripDistance :: Length tripDistance = trainVelocity tripDuration
So multiplication of
a / bby
bis just function application.
Example 3: Manual proofs of unit equality
Let’s define a function that takes a
Velocityand 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
Velocityis a type synonym for
Length / Time, so we actually have:
distance ./. velocity :: Length / (Length / Time)
We can apply the
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
idto 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
destructfunction. 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
We can do type safe dimensional analysis by encoding units as function spaces. The basic pattern is:
- Construct whatever quantities you want using the
constructfunction. 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
destructfunction will convert them into
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!