# 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

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
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.

## 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.

comments powered by Disqus