24 days of Hackage, 2015: day 20: dimensional: type-checked computation on physical quantities with units

Table of contents for the whole series

A table of contents is at the top of the article for day 1.

Day 20

(Reddit discussion)

One thing that my science teachers in high school always emphasized, when we did calculations, was to be explicit about the units of measurement. They were very stern that we show our units, carry them and cancel them as appropriate, in order to get a final answer that was meaningful. And for good reason! If you add a distance (such as in meters) and a velocity (such as kilometers per second), that is a type error. It is also a type error to add the numerical value of a distance in meters and a value of a distance in feet: to perform such an addition, you have to convert to a common unit first and then add the numbers.

The programming language F# comes with units of measure built into its type system. This is a really cool feature. How can we do this in Haskell?

It turns out that with a lot of fancy type machinery, people have done this sort of thing in Haskell. A library I looked at for making unit-checking into type-checking for physical quantities is the actively evolving dimensional library.

Today I’ll show a little bit of code using it to give a flavor of what you can do with it.

Installation

Because dimensional is moving so quickly, I didn’t use the old version coming with the current Stackage LTS. I added to stack.yaml

- dimensional-1.0.1.1
- exact-pi-0.4.1.0
- numtype-dk-0.5

dimensional is moving so quickly that the master branch on GitHub is already beyond even this version.

(Update of 2016-01-06)

Stackage LTS 4 has caught up, no no more need for these modifications.

Example task

As a runner, I sometimes want to perform all kinds of predictions or projections from goals, to calculate various quantities such as required pace to finish a race in a certain time, so I decided to play with using dimensional to express a simple calculation.

Given a goal 5K time and a target racing stride rate (180 steps per minute), I calculate the stride length required.

An HSpec test

Imports:

module DimensionalExampleSpec where

import DimensionalExample (requiredStrideLength)

import Prelude hiding ((+))
import Numeric.Units.Dimensional.Prelude
       ( (*~), (/~)
       , (+)
       , Length, Time, kilo, meter, minute, second
       )
import Numeric.Units.Dimensional.NonSI (foot)

import Test.Hspec (Spec, hspec, describe, it, shouldSatisfy)

Note that I took the pain to provide explicit imports for Numeric.Units.Dimensional.Prelude. In reality, if I were using the dimensional library for a serious amount of code, I would bite the bullet and acknowledge that we are working in an entire domain-specific language of arithmetic that warrants hiding the Prelude and just using everything the dimensional Prelude provides, as far as commonly used units, quantity types, and overloaded arithmetic operators.

The sample test, which just verifies I do not have to have a stride greater than 4 feet but must be greater than 3 feet:

spec :: Spec
spec =
  describe "dimensional" $ do
    it "check required running stride length" $
      let fiveK :: Length Double
          fiveK = 5 *~ kilo meter

          goalTime :: Time Double
          goalTime = 24 *~ minute + 45 *~ second

          feetPerStep :: Double
          feetPerStep = requiredStrideLength fiveK goalTime /~ foot
      in feetPerStep `shouldSatisfy` (\x -> x > 3 && x < 4)

Note that every quantity is parameterized over the numeric type involved, e.g., Length a. The operators with ~ combine a numeric value with a unit to give a complete quantity. You can multiply by units, divide by them (as in dividing by foot to get a Double from aLength Doubleabove). The normal operators such as+` operate on quantities.

Implementation

module DimensionalExample where

import Prelude hiding ((/))
import Numeric.Units.Dimensional.Prelude
       ( (*~)
       , (/)
       , Quantity, Recip, DTime, Length, Time
       , one, minute
       )

-- | "Ideal" turnover for steps while running is 180 steps per minute.
turnover :: Quantity (Recip DTime) Double
turnover = (180 *~ one) / (1 *~ minute)

requiredStrideLength
  :: Length Double
  -> Time Double
  -> Length Double
requiredStrideLength distance goalTime =
  distance / goalTime / turnover

Here one is used to go to a dimensionless quantity. Underneath, the dimensional library uses type families to represent division by units and so forth.

A concern about usability

Unfortunately, as you might expect from a library that uses a lot of type level infrastructure and computation, there’s definitely a learning curve in understanding the conceptual foundation of this library, although the documentation is pretty good. The worst thing is that because of type synonyms in combination with all the type level stuff, the error messages can get really weird if you do something nonsensical. Even if you do something meaningful, you can get confused. For example, supposed we didn’t know enough to write the type signature for turnover above. The inferred type is:

    Top-level binding with no type signature:
      turnover :: dimensional-1.0.1.0:Numeric.Units.Dimensional.Internal.Dimensional
                    'Numeric.Units.Dimensional.Variants.DQuantity
                    ('Numeric.Units.Dimensional.Dimensions.TypeLevel.Dim
                       'numtype-dk-0.5:Numeric.NumType.DK.Integers.Zero
                       'numtype-dk-0.5:Numeric.NumType.DK.Integers.Zero
                       'numtype-dk-0.5:Numeric.NumType.DK.Integers.Neg1
                       'numtype-dk-0.5:Numeric.NumType.DK.Integers.Zero
                       'numtype-dk-0.5:Numeric.NumType.DK.Integers.Zero
                       'numtype-dk-0.5:Numeric.NumType.DK.Integers.Zero
                       'numtype-dk-0.5:Numeric.NumType.DK.Integers.Zero)
                    Double

Ouch! This is in fact what I first got when writing the code without explicit type annotations. I had to hunt down what was really going on in order to find the type synonyms that expressed my intent.

I don’t know how to fix the general problem of type-heavy libraries resulting in a lot of usability learning curves and gotchas, but I think that as more and more fancy types are used in Haskell libraries, something needs to be done. I have a hard time believing that a typical scientist who barely knows any Haskell and whose job is to write safe and correct code would use a library like dimensional at this stage, however cool it is. That said, I’m pretty excited that dimensional exists and is currently being actively developed!

Real examples

Doug Burke uses dimensional in his astronomy IHaskell notebooks, for example this one.

Conclusion

dimensional is an interesting library for making units explicit and type-checked in calculations involving physical quantities, and a showcase for how types can be used to better express and check intent.

All the code

All my code for my article series are at this GitHub repo.