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.
Comments
- Anonymous
August 29, 2008
Units of Measure in F#: Part One, Introducing Units [ reddit ] [ digg ] - Welcome to the F# CTP project - Anonymous
August 29, 2008
This is fantastic. I had come across your page last night and seen this. What a surprise to see this included in F# the next morning! Thank you for F#. - Anonymous
August 29, 2008
Indeed, this is awesome.However, what about things such as:type Vector = struct val X:float val Y:float val Z:floatnew(x,y,z) = X= x Y = y Z = zWould I be able to do something likeAccelerate(Vector(1.0<m/s>, 1.0<m/s>, 1.0<m/s>), 3<m s^-2>, 2.0<s>)? - Anonymous
August 29, 2008
And, if I am, what will the Vector structure appear to be to non-F# code? - Anonymous
August 29, 2008
Don Syme just announced today the F# Community Technical Preview (CTP) Release September 2008 which is - Anonymous
August 29, 2008
Don Syme just announced today the F# Community Technical Preview (CTP) Release September 2008 which is - Anonymous
August 29, 2008
Don Syme just announced today the F# Community Technical Preview (CTP) Release September 2008 which is - Anonymous
August 30, 2008
Pon: yes, you can parameterize other types (such as Vector) on units-of-measure. Here's an example, in which the value v has type Vector<m/s>. More on this in another article, coming soon!Andrew.[<Measure>] type m[<Measure>] type stype Vector< [<Measure>] 'a> = struct val X:float<'a> val Y:float<'a> val Z:float<'a> new(x,y,z) = {X=x;Y=y;Z=z}endlet v = Vector(2.0<m/s>,3.0<m/s>,4.0<m/s>) - Anonymous
August 30, 2008
Thanks for this.It's a real pleasure to see a "real sytem" implemented. Proper engineering and scientific calculations (and graphs...) have for a long time been ignored in computer science, often by ignorance.Now we don't have to roll our own for a lot of what is needed. - Anonymous
August 30, 2008
Wow, what a busy week!  The F# CTP is out the door, and it's already making reverberations around - Anonymous
August 30, 2008
Que dire de cette CTP , si ce n' est qu' elle est mieux intégrée dans Visual Studio. intellisense de - Anonymous
August 30, 2008
Cool!As my major at university was Physics, unit checking and inferring are more natural than type checking and inferring.Let me ask a question.1) "dimensionless" floatIn physics, some quantities doesn't have dimensions and the fact that it is dimensionless is important.For example, "Reynolds number" in flued mechanics.(http://en.wikipedia.org/wiki/Dimensionless_quantity)My question is, are there any way to require a float to be dimensionless in F#?2) Assert by unitsI don't know whether possible or not, but I think it would be very interesting if I could embed assertion by units and can be checked statically.Something like following: : let m = accel / time / time assert(m:float<kg>) let x = m / mass assert(x:float<"dimensionless">) :Anyway, this is a great job and I hope you to keep moving forward to improve F#! - Anonymous
August 31, 2008
Ευχάριστα νέα για τους φίλους της F#, καθώς έχουμε στα χερια μας το πρώτο release της productized πλέον - Anonymous
August 31, 2008
@Microsoft: PLEASE convince Anders, Brad, etc to figure out a way to bake this into the CLR type system. There are other languages than F# (eg, Python, C#) that science geeks use. :)@Hiroshi:and what should assert(m:float<kg>) mean?.. assert that m has the same axes as kilograms? (eg, float<lb>, float<g>, float<solarMass> .. all would succeed).. assert that m is a float of kilograms? (eg, float<lb>, etc would fail)These are very different questions, but the way the assert is written it's impossible to tell what is meant.Re "dimensionless" quantities:These differ from scalars how? Should counts (eg, Avogradro's number) be handled differently?This is actually a peeve of mine in the way the mathematical powers-the-be have treated angular measure. - Anonymous
August 31, 2008
This is seriously great; however, it begs the question: can those unit types be used for numeric types other than float? Can I use, say, decimal? Or even int? What if I want to roll out my own BigInteger/BigDecimal - will I be able to hook it into the type system seamlessly to the end user? - Anonymous
August 31, 2008
Also, it strikes me odd that I can't write something like: [<Measure>] type g [<Measure>] type kg = 1000 * glet x = 1.0<kg>Of course I could treat kg as a val rather than type: let kg = 1000<g>but then I can't use it in literal type suffixes. - Anonymous
August 31, 2008
The comment has been removed - Anonymous
September 01, 2008
You've been kicked (a good thing) - Trackback from DotNetKicks.com - Anonymous
September 07, 2008
"An acceleration" or "a distance" is ambiguous, proper names would be linear acceleration and linear distance as a distance could also be a rotational distance. - Anonymous
September 24, 2008
First, let me remind you that in my new ongoing quest to read source code to be a better developer , - Anonymous
October 11, 2008
F# es un lenguaje funcional, creado por Microsoft. Implementado bajo el soporte de .NET CLR, es un lenguaje - Anonymous
November 28, 2008
NASA气象卫星意外坠落说明，计量单位绝非小事。为编程语言添加对计量单位的支持可以很大程度上避免这样的错误，编程任务也变得更有趣。F#提供了对计量单位的静态检查，并且封装了国际单位制的各个单位和物理常量，另外我们也可以定义自己的单位；在单位之间进行换算也很简单；此外F#还支持计量单位的泛型。作为对NASA气象卫星的纪念，本文最后给出了一个模拟太阳系的例子 :) - Anonymous
December 03, 2008
I'm puzzled. Why not allow unit checking on integers, or, for that matter, any type whatsoever? I wrote a units-of-measure extension to boo as a 5th-year undergrad project; this compiler step assumed that absolutely everything in a program had an associated unit. This fact had no effect on type checking until the user started annotating variables or constants with types, and then the unit inference engine worked its magic looking for inconsistencies.In my engine, I just assumed certain rules about operators, like'a + 'a -> 'a'a - 'a -> 'a'a * 'b -> 'a*'b'a << _ -> 'a(where _ means 'dimensionless')Therefore any type that had these operators defined automatically got a reasonable default unit checking behavior.There exist certain algorithms in which a variable has to take on different units at different points in time, so I also had a special annotation that (IIRC) disabled unit checking with respect to a specific variable. - Anonymous
March 30, 2009
Units!? YES! This is (the start of) EXACTLY what I need for my job right now! F# just peaked my interest.I can't tell you how much I'll appreciate this feature. - Anonymous
January 05, 2010
YES!! And, it's about time!! 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.Well, I think some folks with physics/engineering/applied math backgrounds, such as myself, would be amazed at your amazement... : )I've stumbled over here into F# land because I started working on a program that needs to process and analyze GPS data contained in GPX files, and it became painfully obvious very quickly that a programming framework that would handle units in a natural way was practically a must, and it ALSO became painfully obvious very quickly that the OO inheritance mechanisms in the common procedural languages (C++, C#, Java, VB etc) all present major roadblocks to implementing a "units of measurement" framework.I cannot even begin to describe how exciting it is to discover that this is a core feature of F#.But going beyond that particular domain, I would propose that the idea that units are not a "near must" almost everywhere else, is actually an illusion born more of ignorance than anything.The idea that units and dimensional analysis don't go beyond "meters/kilograms/seconds", and that they are useful only in the practice of specialized areas of engineering and physics, comes from having a very shallow understanding of what units and dimensional analysis really are.Out in the real world, just about every "number" that one can think of, is not really a pure number at all. Almost every number you'll come across has some kind of units associated with it. A count of oranges is not the same thing as a count of apples, and hence as the old saw goes, one should not try to compare them. Also, a count of web hits, is not the same thing as a count of e-mails sent, is not the same thing as the size of a file in bytes, is not the same thing as the size of a file in characters...With a proper understanding of what units and dimensional analysis really are, and what they are useful for, I think it would be quickly apparent to most that the set of programming applications where units could be very useful, is many orders of magnitude GREATER than the set of applications where they wouldn't be.Even beyond that, I would argue that much of what people wanted to accomplish by means of OO inheritance and encapsulation, would have been / can in many instances be, better accomplished by thinking in terms of units of measure and collections of attributes.This is getting somehwat abstract and far afield but as an illustration start with the inheritance metaphors typically used to introduce the OO concept in the first place.As in, "First, we will construct an Animal class, and then as descendants of that, we will create the classes Fish and Mammals, etc.What you have done with this approach is mapped a taxonomy, which is an APHYSICAL epistemological construct, onto PHYSICALprogram structure. This aphysical -> physical mapping has real consequences, almost none of which are good.One big problem is that as epistemological constructs, taxonomies are continually subject to change and revision. Also, as a matter of practice one should be able to overlay multiple such taxonomies, over top of any generic collection of things each having their own collections of attributes (which might be added to or subtracted from as one's knowledge of the world changes).Inheritance trees, because they become real, physical program structure, are a "one and only one" proposition, and they quickly become set in stone and nearly impossible to change once client code is written around them.Some of the OO projects I've seen resemble nothing so much as a system of crystal spheres, that threatens to shatters whenever one tries to ask it to deal with information, or implement behaviors, not envisioned by their creators at design time. Like "Oooops, we just now discovered Jupiter has moons, and we never imagined that anything could orbit around anything but earth when we designed this system!"This will probably sound rather extreme, and perhaps is, but traditional OO is to my mind a programming practice with no rigorous theoretical underpinnings.Functional programming with units, OTOH, has rigorous logical underpinnings in the form of function theory and dimensional analysis.I think that we may have been here before, in a slightly different context.Here's an interesting thing to ponder:Hierarchical databases -> Relational databasesTraditional OO -> Functional programming w/unitsAt any rate, enormous kudos to you guys for F#. This is a huge, huge leap forward. - Anonymous
January 26, 2011
This is really awesome... I'd love to be able to do the same in C# - Anonymous
February 25, 2011
it appears F# do not support non-integer exponents on units, for instance :[<Measure>] type V[<Measure>] type A[<Measure>] type s[<Measure>] type Hz = 1/s[<Measure>] type W = VA[<Measure>] type Ohm = V/A// *** Any values// Power spectal densitylet PSD = 10.<W/Hz>// Resistorlet R = 100.<Ohm>// Error : (PSDR) is not 'u^2let VSD = sqrt(PSD*R)