## Dimensional analysis typing

This link describes an implementation of dimensional analysis in C++ using the Boost MPL. What this means is that physical quantities have a type parametrised by a tuple of integers representing the order of physical dimension (i.e. mass, length, time, etc...) with rules determining what operations can be carried out. This is a standard sanity check for equations in physics and easily catches typos.

For example the equation for the force acting on two massive bodies is G(m1m2)/d2. If this were accidentally entered as force f = G*(m1+m2)/(d*d) (perhaps due to misremembering the formula) the compiler would throw a type error.

This is clearly a useful techniques for say, rocket guidance systems. What other languages are capable of doing this without having to declare a morass of types and functions relating those types to each other?

## Comment viewing options

### It looks to be doing pretty

It looks to be doing pretty much the same thing, but using an external system to validate the correctness. The beauty of the C++ system is it's internal, i.e. it uses only the C++ compiler for verification.

### external v. internal checking

It's true, the two systems have different aims. Osprey was designed to work on existing C code, and the utility of that decision might compensate for any perceived ugliness.

### XeLda

Osprey uses the Gaussian-elimination technique Tudor Antoniu and I
developed for spreadsheet unit inference in XeLda some time back.
There's more to that story that I've never written down ... someday.

I, for one, would be very interested in any additional references or writings you might have on this subject!

### Pseudonym did exactly this

Pseudonym did exactly this in Haskell three years ago. I'm not sure where the code has migrated to, but old code is here. There are also other libraries like this floating around.

### Yes, but...

such systems are inherently incomplete: they don't allow for the fact that it's sensible to multiply length and width, but not (in general) to add them, or for the fact that free energy, energy, enthalpy, and even torque (to cite only the most well-known example) have the same units but are not truly commensurable.

### Huh? The first thing is

Huh? The first thing is exactly what they do. The second is easily accomplishable in both C++ and Haskell, and just about any language with abstraction capabilities.

No, I'm wrong about the former; I just realized what you said. Luckily, the solution to the latter also works for the former.

However, is does not need to be complete to be helpful (though, that'd be nice). I can just as easily add a length and width on paper, and doing dimensional analysis accurately still won't help me but it is still helpful.

### Well, actually there's

Well, actually there's nothing stopping you using this system to give length and width different dimensions. There's a whole world of multidimensional dimensional analysis (now there's a confusing term) that this technique can be applied to. Of course you'd only do this if your problem domain required it.

### No it doesn't catch all

No it doesn't catch all errors. However it is very likely to catch the errors you are likely to make. It doesn't provide any kind of proof that your equations are correct (you're expected to do that yourself), but it will very probably show that you've typed them in correctly.

### Fortress

Speaking of Ultimate Lambdas, Guy Steele's current project, Fortress, intends to have this built in to the language. Go down the page and look at the Object-Oriented Units of Measurement paper (OOPSLA 04).

Josh

### Fortress discussion

I might point to a previous Fortress discussion here where we discussed some of the things that dimensional analysis can and can't check easily, about ambiguities when mapping common usage of units of measure into unambiguous, computer-parseable syntax, about weirdnesses in expected order of operation when manipulating units, about following the rules of the International System of Units (SI) for writing and parsing units, etc.

There's another discussion where we discuss some of the design issues and unexpected behaviors introduced by Fortress and the Google calculator that try to perform "do what I mean" fixups that don't follow standard mathematical notation or precedence.

### frink

Frink a programming language designed to help us all to better understand the world around us, to help us get calculations right without getting bogged down in the mechanics, and to make a tool that's really useful in the real world.

### More Frink

That looks like quote from my documentation! :)

Yes, Frink does track units of measure through all calculations. Every single function and mathematical operator in Frink is units-aware, and can handle units of measure any place you can have a number. Frink programs are expected to contain their units of measure explicitly, and the language makes sure that dimensions are tracked properly and units are mixed transparently. Of course, not every case makes sense, like taking sin[3 days], in which Frink will generate an error.

Frink is also intended to follow standard mathematical notation when possible, and to make using units of measure as transparent as possible, that is, to follow standard orthography (as compared to, say, Mathematica, which makes you write Kilo Meter when you mean kilometer or km.)

Frink also validates that units of measure are conformal as soon as possible at runtime. For example, adding 1 foot + 1 meter works fine, but 1 foot + 1 day fails immediately. (Compare this again to Mathematica, which will let you add them and not flag an error until you try to convert them to other units.)

It also contains a large standard data file of common (and uncommon) units of measure and information about things like planets, subatomic particles, fundamental constants of the universe, elements, etc., to allow you to do most calculations without digging up reference books, or remembering how many joules are in a calorie, or look up the current value of Planck's constant.

All of this is checked at run-time, not compile-time.

You can look at some of Frink's sample calculations to give you an idea of what calculations look like.

### More than just a sanity check

Using dimensions can put tight constraints on the form that code can take. For example, if a function takes as argument a length, and returns a length, and there are no other dimensionful values involved, then we know that the code can do only one thing: multiply the input by a dimensionless constant. So just as using strict types means that the code can sometimes 'wriite itself' because there's only one implementation that has the correct type, dimensionful code can also write itself to some extent. (It's a little like free theorems from Reynolds parametricity and I bet that it can be recast in that form.)

At my own workplace we recently had an issue where we were forced to rescale (in length) all of the constants in our code due to precision issues with a library we were using. There were many locations where the source code needed editing to introduce this new scaling constant. But if the code had been written using dimensionful types then it would have been clear exactly what needed rescaling - any data which had a non-trivial power of length in its type. So using dimensions in our code could have saved quite a bit of effort.

### For example, if a function

For example, if a function takes as argument a length, and returns a length, and there are no other dimensionful values involved, then we know that the code can do only one thing: multiply the input by a dimensionless constant.

Are you referring to a particular implementation of dimensioning? I would expect that the function  f x = x + 1 meter  could be typed as  Length -> Length . IIRC, Fortress requires the conversion between all units of a particular dimension to be defined, so I'd have guessed that Fortress would allow this typing.

### I qualified what I said slightly

I said "and there are no other dimensionful values involved" whereas you have introduced a dimensionful constant "1 meter".

There's a very interesting phenomenon in physics: there are very few constants with dimension. For example, take a fluid dynamics simulation. This might involve many thousands of lines of code and yet there'll only be a handful of dimensionful constants: the fluid densities, the fluid viscosities, maybe some dimensions coming from the size of the elements the simulation is based on and a couple more. This is part of where the power of dimensionful types comes from: you know that there aren't going to be new constants like 1.2345 meters introduced in every other line of your code. Most constants that do crop up will tend to be dimensionless.

Consider, for example, this physical problem: we bend a wire into the shape of a sine wave oriented horizontally so that it follows y = l*sin(x/l) (l is a scaling). We place a bead on the wire at the midpoint between a peak and a valley (ie. on y=0). We now release the bead. How long does it take for the bead to hit the bottom of a valley, assuming no friction? You can probably see there is going to be a pretty messy bit of differential equation solving involved in getting the answer out. I've no idea what the exact answer is but but we can say immediately that it must take the form a*sqrt(l/g) where a is some dimensionless constant and g is the acceleration due to gravity, because that is the only expression that has the right dimensions. In a language that enforced type safety, if we wrote a function of type length -> acceleration -> time, and knew not to introduce dimensionful constants (maybe the compiler should warn us if we try to), we would be forced to write a*sqrt(l/g) simply because it would be the only thing that compiled.

### Thanks, that makes plenty of

Thanks, that makes plenty of sense. I interpretted "and there are no other dimensionful values involved" to mean that there are no other dimensionful parameters passed. My mistake :).

### Some theoretical work on Dimension types

His PhD thesis was on integrating dimension types into functional languages with HM-style type inference, and it also has a discussion of parametricity in the presence of dimensional analysis. An interesting result (IIRC) is that '0' is the only numeric constant that can safely be polymorphic in its dimension type.