The support for physical units in programming languages is a long-standing issue, which very few languages have even attempted to solve. This issue was mostly solved for Ada in 2012 by our colleagues Ed Schonberg and Vincent Pucci, who introduced special aspects for specifying physical dimensions on types. An aspect Dimension_System allows the programmer to define a new system of physical units, while an aspect Dimension allows setting the dimensions of a given subtype in the dimension system of its parent type. The dimension system in GNAT is completely checked at compile time, with no impact on the executable size or execution time, and it offers a number of facilities for defining units, managing fractional dimensions and printing out dimensioned quantities. For details, see the article "Implementation of a simple dimensionality checking system in Ada 2012" presented at the ACM SIGAda conference HILT 2012 (also attached below).

The GNAT dimension system did not attempt to deal with generics though. As noted in the previous work by Grein, Kazakov and Wilson in "A survey of Physical Units Handling Techniques in Ada":

The conflict between the requirements 1 [Compile-Time Checks] and 2 [No Memory / Speed Overhead at Run-Time] on one side and requirement 4 [Generic Programming] on the other is the source of the problem of dimension handling.

So the solution in GNAT solved 1 and 2 while allowing generic programming but leaving it unchecked for dimensionality correctness. Here is the definition of generic programming by Grein, Kazakov and Wilson:

Here generic is used in a wider sense, as an ability to write code dealing with items of types from some type sets.  In our case it means items of different dimension. For instance, it should be possible to write a dimension-aware integration program, which would work for all valid combinations of dimensions.

This specific issue of programming a generic integration over time that would work for a variety of dimensions was investigated earlier this year by our partners from Technical University of Munich for their Glider autopilot software in SPARK. Working with them, we found a way to upgrade the dimensionality analysis in GNAT to support generic programming, which recently has been implemented in GNAT.

The goal was to apply dimensionality analysis on the instances of a generic, and to preserve dimension as much as possible across type conversions. In our upgraded dimensionality analysis in GNAT, a conversion from a dimensioned type (say, a length) to its dimensionless base type (the root of the dimension system) now preserves the dimension (length here), but will look like valid Ada code to any other Ada compiler. Which makes it possible to define a generic function Integral as follows:

We are using above the standard Mks_Type defined in System.Dim.Mks as root type, but we could do the same with the root of a user-defined dimension system. The generic code is valid Ada since the arguments X and T are converted into the same type (here Mks_Type), in order to multiply them without compilation error. The result, which is now of type Mks_Type, is then converted to the final type Integrated_Type. With the original dimensionality analysis in GNAT, dimensions were lost during these type conversions.

However, with the upgraded analysis in GNAT, a conversion to the root type indicates that the dimensions of X and T have to be preserved and tracked when converting both to and from the root type Mks_Type. With this, still using the standard types defined in System.Dim.Mks, we can define an instance of this generic that integrates speed over time:

The GNAT-specific dimensionality analysis will perform additional checks for correct dimensionality in all such generic instances, while for any other Ada compiler this program still passes as valid (but not dimensionality-checked) Ada code. For example, for an invalid instance as:

GNAT issues the error:

One subtlety that we faced when developing the Glider software at Technical University of Munich was that, sometimes, we do want to convert a value from a dimensioned type into another dimensioned type. This was the case in particular because we defined our own dimension system in which angles had their own dimension to verify angular calculations, which worked well most of the time.

However, the angle dimension must be removed when multiplying an angle with a length, which produces an (arc) length, or when using an existing trigonometric function that expects a dimensionless argument. In theses cases, a simple type conversion to the dimensionless root type is not enough, because now the dimension of the input is preserved. We found two solutions to this problem:

• either define the root of our dimension system as a derived type from a parent type, say Base_Unit_Type, and convert to/from Base_Unit_Type to remove dimensions; or
• explicitly insert conversion coefficients into the equations with dimensions such that the dimensions do cancel out as required.

For example, our use of an explicit Angle_Type with its own dimension (denoted A) first seemed to cause trouble because of conversions such as this one:

where darc is of Angle_Type (dimension A) and EARTH_RADIUS of Length_Type (dimension L). First, we escaped the unit system as follows:

However, this bypasses the dimensionality checking system and can lead to dangerous mixing of physical dimensions. It would be possible to accidentally turn a temperature into a distance, without any warning. A safer way to handle this issue is to insert the missing units explicitly:

Here, Radian is the unit of Angle_Type, which we need to get rid of to turn an angle into a distance. In other words, the last term represents a coefficient with the required units to turn an angle into a distance. Thus, darc*1.0/Radian still carries the same value as darc, but is dimensionless as required per the equation, and GNAT can perform a dimensionality analysis also in such seemingly dimensionality-defying situations.

Moreover, this solution is less verbose than converting to the base unit type and then back. In fact, it can be made even shorter:

With its improved dimensionality analysis, GNAT Pro 18 has solved the conflict between requirements 1 [Compile-Time Checks] and 2 [No Memory / Speed Overhead at Run-Time] on one side and requirement 4 [Generic Programming] on the other side, hopefully making Grein, Kazakov and Wilson happier! The dimensionality analysis in GNAT is a valuable feature for programs that deal with physical units. It increases readability by making dimensions more explicit and it reduces programming errors by checking the dimensions for consistency. For example, we used it on the StratoX Weather Glider from Technical University of Munich, as well as the RESSAC User Case, an example of autonomous vehicle development used as challenge for certification.

For more information on the dimensionality analysis in GNAT, see the GNAT User's Guide. In particular, the new rules that deal with conversions are at the end of the section, and we copy them verbatim below:

  The dimension vector of a type conversion T(expr) is defined as follows, based on the nature of T:

 -  If T is a dimensioned subtype then DV(T(expr)) is DV(T) provided that either expr is dimensionless or DV(T) = DV(expr). The conversion is illegal if expr is dimensioned and DV(expr) /= DV(T). Note that vector equality does not require that the corresponding Unit_Names be the same.

    As a consequence of the above rule, it is possible to convert between different dimension systems that follow the same international system of units, with the seven physical components given in the standard order (length, mass, time, etc.). Thus a length in meters can be converted to a length in inches (with a suitable conversion factor) but cannot be converted, for example, to a mass in pounds.

 -  If T is the base type for expr (and the dimensionless root type of the dimension system), then DV(T(expr)) is DV(expr). Thus, if expr is of a dimensioned subtype of T, the conversion may be regarded as a “view conversion” that preserves dimensionality.

    This rule makes it possible to write generic code that can be instantiated with compatible dimensioned subtypes. The generic unit will contain conversions that will consequently be present in instantiations, but conversions to the base type will preserve dimensionality and make it possible to write generic code that is correct with respect to dimensionality.

 -  Otherwise (i.e., T is neither a dimensioned subtype nor a dimensionable base type), DV(T(expr)) is the empty vector. Thus a dimensioned value can be explicitly converted to a non-dimensioned subtype, which of course then escapes dimensionality analysis.

Thanks to Ed Schonberg and Ben Brosgol from AdaCore for their work on the design and implementation of this enhanced dimensionality analysis in GNAT.