Units of Measure in F#: Part One, Introducing Units
Do you remember NASA's Mars Climate Orbiter? It was lost in September 1999 because of a confusion between metric and so-called "English" units of measurement. The report into the disaster made many recommendations. In all likelihood, the accident could have been prevented if the NASA engineers had been able to annotate their program code with units, and then employed static analysis tools or language-level type-checking to detect and fix any unit errors.
Of course, the languages that NASA used had no language or tool support for units. Many people have suggested ways of extending programming languages with support for static checking of units-of-measure. It's even possible to abuse the rich type systems of existing languages such as C++ and Haskell to achieve it, but at some cost in usability. More recently, Sun's Fortress programming language has included type system support for dimensions and units. It also happens to have been the subject of my PhD thesis from a few years ago. So it's particularly exciting for me that a feature which I studied in theory in 1995 will now get used in practice in F#.
As recently announced in the September 2008 F# CTP (Community Technical Preview), the F# programming language now has full support for static checking and inference of units-of-measure. In this series of articles I'll gently introduce the feature. (If you're not familiar with F#, look here.) We've already been testing out the units-of-measure feature inside Microsoft and I'm amazed at the diversity of applications that are turning up. Of course, there are the obvious applications to scientific computing, and games (which are all about physics, after all), but we're seeing applications in machine learning, finance, search (think click rates, etc) and others.
We'll start more traditionally, with units for mass, length and time. As it's the 21st century I'll use the modern incarnation of the metric system, the International System of Units, abbreviated SI from the French "Le Système International d'Unités".
Here, the Measure attribute tells F# that kg, s and m aren't really types in the usual sense of the word, but are used to build units-of-measure. (You'll see in Part Two of this series of articles that they can have static members just like ordinary types in F#, but other than that they are quite different).
Now let's introduce some constants with their units, which we can do simply by tacking the units onto a floating-point number, in between angle brackets:
Notice how conventional notation for units is used, with / for dividing, and ^ for powers. Juxtaposition just means "multiply", and negative powers can be used in place of division, so you might prefer to express the units of acceleration slightly differently:
Or I might invite the wrath of my old physics teacher by writing it this way:
Now we can do some physics! If I jump out of my window, at what speed will I hit the ground?
You could try this in F# Interactive and see the result, or print it out. (It's about 8.3 metres per second. Ouch!) But more interestingly, hover the cursor over the variable and look at its type:
Magic! Units-of-measure are not just handy comments-on-constants: they are there in the types of values, and, what's more, the F# compiler knows the rules of units. To be more precise: the built-in type float takes an optional unit-of-measure parameter, written in angle brackets, in a similar way that types such as IEnumerable take a type parameter, as in IEnumerable<int>. When values of floating-point type are multiplied, the units are multiplied too; when they are divided, the units are divided too, and when taking square roots, the same is done to the units. So by the rule for multiplication, the expression inside sqrt above must have units m^2/s^2, and therefore the units of speedOfImpact must be m/s.
What if I make a mistake?
I've tried to add a height to an acceleration, so F# tells me exactly what I've done wrong. The units don't match up, and it tells me so!
Now let's do a little more physics. What force does the ground exert on me to maintain my stationary position?
We've just applied Newton's Second Law of motion. Being such a Great Man, Sir Isaac had a unit named after him: the newton, the SI unit of force. So instead of the cumbersome kg m/s^2 we can introduce a derived unit and just write N, the standard symbol for newtons.
Derived units are just like type aliases: as far as F# is concerned, N and kg m/s^2 mean exactly the same thing.
Summing up. We've seen how to introduce base units, how to introduce derived units, and how to introduce constants with units. Everything else has followed automatically: F# checks that units are used consistently, it rejects code with unit errors, and it infers units for code that's unit-correct.
Next time we'll have a look at multiple unit systems, converting between units, and interfacing with non-unit-aware code.
