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 simplym 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 writekilo (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 uselet speed = (kilo (m 160.0)) /! (hour 1.0). To compute the distance travelled at previous speed during 120 s, one would dolet distance = (normalize_si_value speed) *! (s 120.0)and the program can print5333.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. :-)
Comments
Sat 03 Dec 2011
I think it can be done to some extent using phantom types. Here's a simple sample in F# (I don't have OCaml handy):
> type Unit<'a> = Unit of float;;
type Unit<'a> = | Unit of float
> type Meter = interface end;;
type Meter =
interface
end
> type Mile = interface end;;
type Mile =
interface
end
> let meters x = Unit x : Unit<Meter>;;
val meters : float -> Unit<Meter>
> let miles x = Unit x : Unit<Mile>;;
val miles : float -> Unit<Mile>
> let (+) (x: Unit<'a>) (y: Unit<'a>) : Unit<'a> = match x, y with Unit x, Unit y -> Unit (x + y);;
val ( + ) : Unit<'a> -> Unit<'a> -> Unit<'a>
> (meters 10.0) + (meters 11.0);;
val it : Unit<Meter> = Unit 21.0
> (meters 10.0) + (miles 11.0);;
(meters 10.0) + (miles 11.0);;
-----------------^^^^^^^^^^
stdin(26,18): error FS0001: Type mismatch. Expecting a
Unit<Meter>
but given a
Unit<Mile>
The type 'Meter' does not match the type 'Mile'
>
Sat 03 Dec 2011
I have played with the idea of using phantom types for units, but I don't think it can work transparently in the OCaml language. The problematic part is the addition or substraction of unit exponents when multiplying or dividing values. To get a good phantom types solution, you would need to express those operations at the type level, and I don't think that is possible in OCaml right now. Unification is very good at checking and enforcing equality, and can be used for some other things, but general additions and substractions are a bit beyond reach (contrarily to Haskell where I think this can be done).
What you could possibly have are *explicit* type-level operations, with terms witnessing the result of an operation; I have written a toy example of this in case you're wondering what it means:
https://gitorious.org/gasche-snippe...
The point is that whenever you use a multiplication operation, you have to provide an explicit witness that the type-level addition is correct. This allows to encode any operation at the type level by defining its "witness formers" at the type level, in a style strongly reminding of Prolog.
This is of course not practical: your users will not appreciate this level of type-system hand-holding. Your choice of a dynamic library is better. The designers of the F# language have included a unit system in the type system, and they use it to attract scientific programmers.
http://msdn.microsoft.com/en-us/lib...
If you're interested, you can have a look at Adam Gundry's technical report. It amounts to hard-coding arithmetic operations ("abelian group") into the type system, but it's actually relatively interesting and elegant.
http://personal.cis.strath.ac.uk/~a...
Sun 04 Dec 2011
Here's an OCaml version: http://pastebin.com/QTWmpkZV
Sun 04 Dec 2011
Amusant, j'avais exactement le même sujet en tête (après avoir lu des choses sur des erreurs critiques [célèbres] induites par des confusions d'unités) mais dans un contexte plus formel, genre B au hasard ;-)
Mon 05 Dec 2011
Les seules limites sont, comme toujours, ceux de la vision. 08))
Tue 06 Dec 2011
@Alex Muscar: Your code does not correctly handle /! and *! operators. For example you cannot do 1 meter / 1 second :
But even if the type system is fixed, I think (and I'm not alone, see gasche comments) you cannot express types like m.s-2 and do operations on them.
@gasche: Thank you for the detailed response. The example type level operations you are giving is typically what I would like to have but you are right that doing the type annotation is not very practical. The F# pointer is very interesting, I did not know that F# had such capability. Regarding the report on the dedicated type system for units, this is currently a bit too advanced for me right now. ;-) But it is any way interesting to know that there is some work done is this area.
@GMR: I am also thinking at more formal approaches, although probably not using B. Stay tuned. ;-)
@Richard: Of course, one can make errors when defining constants and other inputs, as well as on equations. But at least checking units would allow to catch basic errors, like OCaml's typing system.
Thu 29 Dec 2011
All physicists are routinely checking their equations with those rules. See the above paper for details. But I would be pleased to be shown wrong. The problematic part is the addition or substraction of unit exponents when multiplying or dividing values. Your choice of a dynamic library is better.t but an expression was expected of type SI. The example type level operations you are giving is typically what I would like to have but you are right that doing the type annotation is not very practical.Hope you like my post on <a href="http://www.google.com">google</a> today.