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

## Day 20

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.

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 a```Length Double`above). 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.

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.