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.
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
Today I’ll show a little bit of code using it to give a flavor of what you can do with it.
dimensional is moving so quickly, I didn’t use the old
version coming with the current Stackage LTS. I added to
- dimensional-220.127.116.11 - 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
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
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
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
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
above). The normal operators such as+` operate on
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
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-18.104.22.168:Numeric.Units.Dimensional.Internal.Dimensional ' (' '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
this stage, however cool it is. That said, I’m pretty excited that
dimensional exists and is currently being actively developed!
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