When writing a computer program that interact or handle with the physical word, a common need is to manipulate physical units like meter, second or km/h. Most of the time it is up to the programmer to ensure that the physical units are correctly used, even if there are rules to check them (divide only meters by meters, ...). All physicists are routinely checking their equations with those rules. Why not programmers?

So here is a draft of OCaml library to do just that: computations on physical values while ensuring physical units rules are followed (for example, you only add meters to meters, not meters to seconds). Here are the SIunits.mli and SIunits.ml files.

The use of the library are quite simple:

  • A set of functions to create values with units from simple floats. For example meter 1.0 (or simply m 1.0) creates a value containing 1 meter;
  • A set of utility functions to handle SI prefixes like kilo, to normalize a value (i.e. to remove the scaling factor) or to print it with its units. For example, to enter a length of 160 km one would write kilo (m 160.0);
  • A set of four operators, +!, -!, *! and /! to do basic computations on those values. For example, to enter a speed of 160 km/h, one would use let speed = (kilo (m 160.0)) /! (hour 1.0). To compute the distance travelled at previous speed during 120 s, one would do let distance = (normalize_si_value speed) *! (s 120.0) and the program can print 5333.333333 .m;

Internally, I have followed the proposal of "Checking SCADE Models for Correct Usage of Physical Units" paper by using a vector of 8 units: 7 base units (following those defined in the SI system) plus one power of 10 unit for the scaling factor (to handle kilo, mega or more exotic units like hour). In fact, to be really exhaustive one would need some additional units but the current code is really a draft. Then, the rule for addition or subtraction is to check that the units are identical, while for multiplication and division the units of the two numbers are added or subtracted. See the above paper for details.

There is a lot of work to transform this draft code into a real, usable and exhaustive, library:

  • Power and root operators;
  • Comparison operators;
  • Decision operators;
  • Dimensionless units;
  • Absolute or relative values;
  • More prefixes and exotic units;
  • And of course of lot of tests for above code.

Right now, I do not intend to extend the current code but if other people are interested, I could work on it and open an OCaml Forge project. If there is a need, let me know.

And now a question for the OCaml experts: would it be possible to replace the dynamic checks currently implemented in this library by static checks using OCaml type system (for example using Phantom types)? I think this is not possible: the base units are like arrays of the same size, you need a more expressive type system to express constraints on them (like Coq's Dependent types). But I would be pleased to be shown wrong. :-)