Dimensional Analysis

From time to time, I come across ideas for introducing additional
checking of operands in expressions that go beyond mere types, that
try to take into account the actual dimensions of the units involved.
The intention is that this will reduce the likelihood of expressions
that, while they may be correct in conventional type-compatibility
terms (all the numbers might be of compatible floating types), can be
flagged if they fail a dimensional-analysis check.

I don’t think it’s practical to introduce new types for every single
unit you want to distinguish, since that would lead to a combinatorial
explosion in the necessary conversion operators. It’s far more natural
to build up the units in terms of basic primitives like the SI base
units, and allow derived units be expressed in terms of multiplication
and division of (powers of) the base units.

Some examples, in pseudocode:

    type velocity is units(metres / seconds);
    type energy is units(kilograms * metres * metres * seconds / seconds);

    kinetic_energy : energy;
    particle_velocity : velocity;
    particle_mass : units(kilograms);

Now suppose you have an expression like

    kinetic_energy := 0.5 * particle_mass * particle_velocity ** 3;

you can immediately see that is wrong, because the dimensions in the
source and destination of the assignment don’t match up. That power 3
is probably a typo, and should be a 2:

    kinetic_energy := 0.5 * particle_mass * particle_velocity ** 2;

Of course, this won’t catch errors like multiplication/division by
incorrect constant factors. Dimensional analysis is necessary for an
expression to make physical sense, but it is not sufficient.

At first sight, this can seem useful. But you have to be careful not
to carry it too far. For example, one scheme I saw wanted to specify
separate units for angles so that the arguments and results of trig
functions would be expressed in incompatible units. That I didn’t
think was a good idea.

So what do you think of this idea? Is it already in use in a
significant way in any Ada code? I figured if any language would be
looking at new ways of writing safer code, it would be the Ada crowd.
;)