Unit Types for MiniZinc

Consider the following MiniZinc model of the knapsack problem where we need to choose exactly k different products from a given set PRODUCT, so that the total weight is under the limit, and we maximize profit.

The model runs and will give us answers, but unfortunately it does not define the correct problem. The modeller has used profit instead of wght on line 8. In line 8 we are summing up profits to see that they are under the weight limit. This is a unit type error of the model, comparing integers that represent two different kinds of things.

While there are unit type extensions for almost any programming language, in practice they are not commonly used. The problem is that the overhead of adding unit types to the program has to pay off in comparison to the extra development time to be worth it. For safety critical code this is clearly worthwhile (as the sad demise of the $125M Mars Climate Orbiter indicates¹¹1An investigation indicated that the failure resulted from a navigational error due to commands from Earth being sent in English units (in this case, pound-seconds) without being converted into the metric standard (Newton-seconds).). Given that debugging constraint models can be quite difficult, particularly if the solver simply fails after a large amount of computation, an important role of types in modelling languages is to provide type safety. Many subtle errors can be avoided if we use strong type checking based on the types. Here we introduce unit types for MiniZinc. Interestingly, the question of unit types for modelling languages for combinatorial problems is different from that of procedural languages, and we find the necessity for introducing new kinds of unit types to help prevent type errors in models.

The contributions of this paper are:

• $\mathrm{■}$

  A proposed definition of unit types for MiniZinc, including dimensions and units.

• $\mathrm{■}$

  The introduction of abstract units, and coercions between them, which results from the fact that we are often dealing with integer decisions, so arbitrary multiplication or division of units is not obviously meaningful.

• $\mathrm{■}$

  The introduction of counting types, used in models which count the occurrence of objects, a new form of unit type.

• $\mathrm{■}$

  The introduction of coordinate instead of the usual difference unit types to differentiate variables representing coordinates from those representing distances. These have been defined for other programming languages but less frequently.

• $\mathrm{■}$

  The definition of a unit type checker based on type erasure at the model level, resulting in zero overhead at solving time compared to models that do not use unit types.

• $\mathrm{■}$

  An exploration of existing MiniZinc models to determine how many of them could improve type safety utilizing unit types.

Unit types are refinements of numeric types that attach units of measurement to the numeric objects. They aim to find more type errors. Note that we introduce unit types as an addition on top of the current MiniZinc type system. Although the enhanced type system might reject models that use unit types, it does not influence the correctness of existing MiniZinc models.

A dimension is a kind of measurement, for example distance, time, mass, and worth are basic dimensions. Dimensions can be declared as “unit type $dimension$”. We assume $m$ distinct dimensions are available. A basic unit is an identifier such as metre (metre), sec (second), kg (kilogram), or dollar which has a dimension. A basic unit type can then be declared as “unit $dimension$: $u$”, where $dim(u)=dimension$. Or it can also be derived from an earlier declared or defined unit type $u^{\prime }$ as “unit $dimension$: $u$ = $c$@$u^{\prime }$” where $dim(u)=dim(u^{\prime })=dimension$. The basic unit types for a dimension $dimension$ define a graph with a node for each basic unit type and edges $(u,u^{\prime })$ with weight $c$ for each declared unit type definition.²²2Usually $c$ is an integer. Floating-point constants $c$ are allowed, but they result in automatic casts of integer expressions to float.

One basic unit type $u$ can be downcast to another $v$ of the same dimension by multiplying by the product of constants appearing in the path from $u$ to $v$, denoted $\downarrow$($u,v$), which equals $\perp$ if no path exists. We use $\perp$ to represent a type error/ill-defined type. We define the meet, largest common subunit, of two basic unit types of the same dimension ${\sqcap }_b(u,v)$ as the nearest common ancestor of $u$ and $v$ in the graph, or $\perp$ if none exists.

Figure 1 shows the graph resulting for dimension distance from the sample declarations on the left below. For example, ${\sqcap }_b$(km,mile) = cm, and ${\sqcap }_b$(km,mykd) = $\perp$; similarly $\downarrow$(mile,mm) = $1609394\times 10$, while $\downarrow$(mm,km) = $\perp$. Note how we can have multiple declared basic units for the same dimension, but we cannot coerce from one to the other.

A (complex) unit type $u$ for a numeric object $o$ takes the form $u\equiv b_1^{n_1}{b}_2^{n_2}\mathrm{\cdots }{b}_m^{n_m}$, where each $b_i,1\le i\le m$ is a basic unit type for dimension $i$, and each $n_i,1\le i\le m$ is an integer. The dimension of the type $u$ is $dim{(b_1)}^{n_1}\mathrm{\cdots }dim{(b_2)}^{n_m}$. For example, a speed may have unit type metre/sec, which is technically ${\text{metre}}^1{\text{sec}}^{-1}{\text{kg}}^0{\text{dollar}}^0$ and has dimension ${\text{distance}}^1{\text{time}}^{-1}{\text{mass}}^0{\text{worth}}^0$. Note that we do not allow complex unit types with two basic unit types of the same dimension. We usually omit writing terms where $n_i=0$. We denote by $\mathrm{𝟏}$ the dimensionless unit type (where $n_i=0,1\le i\le m$).

We can add shorthands for dimension expressions and (complex) unit type expressions. A declaration “unit type $short$ = $de$” defines $short$ as a shorthand for the dimension expression $de$. $de$ takes the form of $de\text{*}de$, $de\text{/}de$, $d{e}^n$, or $d$ where $d$ is a previously defined dimension or shorthand and $n$ is an integer. Similarly, (complex) unit type shorthands can be defined as “unit $dimension$: $u$ = $ue$” where $ue$ is defined as above except that $d$ must be a basic or shorthand unit type, and $dim(ue)=dimension$. For example, the declarations below define velocity as a shorthand for distance over time, and a unit of velocity which is always treated as its two components.

We extend the meet operation to a single dimension with power as follows: ${\sqcap }_d(b_i^{n_i},b_i^{\prime }{}_{}{}^{n_i^{\prime }})$ equals $\perp$ if $dim(b_i)\ne dim(b_i^{\prime })$ or $n_i\ne n_i^{\prime }$; otherwise it equals ${\sqcap }_b{(b_i,b_i^{\prime })}^{n_i},n_i\ge 0$ or $b_i^{n_i}$ if $\downarrow (b_i,b_i^{\prime })\ne \perp$, or $b_i^{\prime }{}_{}{}^{n_i}$ if $\downarrow (b_i^{\prime },b_i)\ne \perp$, or $\perp$ otherwise. So for positive powers we use the meet operation, for negative powers we require that one unit is downcastable to the other, and the resulting type is the downcastable type, inverse powers swap the direction to smaller units.

We can then extend meet to two complex unit types: $\sqcap (b_1^{n_1}\mathrm{\cdots }{b}_m^{n_m},c_1^{k_1}\mathrm{\cdots }{c}_m^{k_m})$ is defined as ${\mathrm{\Pi }}_i{\sqcap }_d(b_i^{n_i},c_i^{k_i})$ if none of the dimensional meets results in $\perp$, and $\perp$ otherwise. We can similarly extend downcasting from one complex type to another as $\downarrow (b_1^{n_1}\mathrm{\cdots }{b}_m^{n_m},c_1^{k_1}\mathrm{\cdots }{c}_m^{k_m})$ as if no downcasts results in $\perp$ and $n_i=k_i,1\le i\le m$, or $\perp$ otherwise. This allows us to, for example, determine that $\sqcap ({\text{km}}^2{\text{sec}}^{-1},{\text{m}}^2{\text{hour}}^{-1})$ is ${\text{m}}^2{\text{hour}}^{-1}$ and $\downarrow ({\text{km}}^2{\text{sec}}^{-1},{\text{m}}^2{\text{hour}}^{-1})$ is ${1000}^2\times {(60\times 60)}^{--1}=3600000000$.

We can multiply two complex unit types $u\otimes v$ together: $(b_1^{n_1}\mathrm{\cdots }{b}_m^{n_m})\otimes (c_1^{k_1}\mathrm{\cdots }{c}_m^{k_m})$. This is defined as $x_1^{n_1+k_1}\mathrm{\cdots }{x}_m^{n_m+k_m}$, where $x_i=b_i$ if $b_i=c_i\vee k_i=0$, and $x_i=c_i$ if $n_i=0$, and the result is $\perp$ if neither of these conditions hold for any dimension. Note that this requires that we do not multiply unit types with different basic types for the same dimension together.³³3It is possible to introduce automatic coercion during multiplication, but there are quite a few non-obvious cases, so at present we restrict multiplication. The coercions could always be explicitly added to the model to allow a multiplication. We can invert a unit type $u\equiv b_1^{n_1}\mathrm{\cdots }{b}_m^{n_m}$ to obtain $\mathrm{𝟏}/u$ as $b_1^{-n_1}\mathrm{\cdots }{b}_m^{-n_m}$. Division of unit types is just inversion followed by multiplication: $u/v=u\otimes (\mathrm{𝟏}/v)$. For example, ${\text{km}}^1{\text{sec}}^{-1}\otimes {\text{km}}^1$ gives unit type ${\text{km}}^2{\text{sec}}^{-1}$ and $\mathrm{𝟏}/({\text{km}}^1{\text{sec}}^{-1})={\text{km}}^{-1}{\text{sec}}^1$.

Note that while meet and down casting are a bit complex to define, actual models mainly use simple cases, as there are usually one or two basic unit types for each dimension.

The main role of unit types is to prevent making unit type errors. They restrict the possible correct arithmetic expressions we can write. Below, we give our candidate syntax to work with unit types in existing MiniZinc models, and the type computation rules for important classes of arithmetic expression. Importantly, unit types are checked at the model level (without the data) and then erased, incurring no runtime overhead when solving the problem.

A constant $c$ can be created of arbitrary unit type $u$ using the @ symbol, $c\text{@}u$. The operator should have a high precedence to ensure it binds tightly to prevent confusion about which expression it influences. A variable can be declared with a unit type by appending the unit type onto the type declaration using the @ symbol as follows: “$[\text{var}][\text{int}|\text{float}]\text{@}u\text{:}id$” declares identifier $id$ to have unit type $u$. We can similarly define set or array arithmetic parameters or decisions with unit types. During type inference/checking, the type of identifier $id$ is its declared unit type $u$.

Here are the most important typing rules for this new syntax. The complete set of typing rules is given in Appendix B.

• $\mathrm{■}$

  $type(k\mathrm{@}u)=u$. Constants simply have the annotated unit type.

• $\mathrm{■}$

  $type(e_1+e_2)=\sqcap (type(e_1),type(e_2))$. Addition (and subtraction) require unit types which have a meet (i.e. they have the same dimensions and there is a coercion to a common unit).

• $\mathrm{■}$

  $type(e_1\times e_2)=type(e_1)\otimes type(e_2)$. Multiplication of unit types is free in the dimension of the indices but restrictive in the basic unit types.

• $\mathrm{■}$

  $type(e_1\text{div}{e}_2)=type(e_1)\otimes type(\mathrm{𝟏}/e_2)$. Division of unit types is simply inversion followed by multiplication.

Most other integer operations act similarly to $+$. For example, $\max ,\min$ and if-then-else-endif have type given by the meet of their (last 2) arguments.

Returning to the example from the introduction, we might add units types as follows

The first line makes the standard library unit declarations available to the model. The parameters are now specified in terms of units. With these declarations, we immediately get the following unit type error on the second last line of the original model: unit mismatch: expected ‘‘dollar’’, but got ‘‘kg’’.

To produce meaningful error messages for unit mismatches, the original units as written by the modeller (or propagated through multiplication or division) are always used in any user-facing messaging, in addition to the computed normalized units. This ensures that the modeller is not faced with error messages only mentioning constructs they never wrote, and the normalized units allow for easy comparison of the two units to see the exact mismatch. For example, for the following model an error will be produced for the last line stating: unit mismatch: expected ‘‘vel = ‘‘m*sˆ-1’’ but got ‘‘vel/s = m*sˆ-2’’.

One of the differences of discrete optimization models from normal programs is that they often reason about counts of different kinds of objects. We want to ensure that we do not make unit errors in our model when dealing with counting. Consider a variation of our running model where we use 0/1 variables to define the chosen products.

What unit type do k and the chosen variables have? They are counts of PRODUCT. We extend any enumerated type in MiniZinc to also be used as the unit type for counting that enumerated type. In this model, the suggested unit type declarations are

The wght array records mass per PRODUCT, while the profit array records worth per PRODUCT. Since we are multiplying the counts of PRODUCTs chosen[p] by the product’s weight wght[p], it is clear that the constraint on line 8 is unit correct.

Note that the two declarations PRODUCT: k and int@PRODUCT: k are quite different, the first k holds a (non-numeric) product, while the second k holds an integer count of products.

A counting type is simply a new dimension together with a basic unit. So each enumerated type E adds a new basic unit also named E and a new dimension also named E to the unit type system, where $dim(\text{E})=\text{E}$.

Consider the following MiniZinc model for a simple scheduling problem with precedences between pairs of tasks:

Each task has a duration d, and we wish to decide its start time s (all in minutes). The constraint in lines 6-7 ensures that the first task in each row of pt must be completed before the second task. Finally, no two tasks should overlap. The model is unit type correct, and runs and can give answers, but it is wrong!

In MiniZinc and almost all languages, we consider the numeric types to be essentially differences. That is, they are a value that can be added to each other, or subtracted or multiplied. But there is a different use of numeric types as absolute coordinates in some numerical system. It does not make sense to add these coordinates usually: consider 11^∘C and 25^∘C, while it certainly makes sense to determine their difference $25\text{<sup class="ltx\_sup">∘</sup>}\text{C}-11\text{<sup class="ltx\_sup">∘</sup>}\text{C}=8\text{<sup class="ltx\_sup">∘</sup>}\text{C}$, how are we to interpret $11\text{<sup class="ltx\_sup">∘</sup>}\text{C}+25\text{<sup class="ltx\_sup">∘</sup>}\text{C}$? Adding two temperatures does not make any sense.

This arises in models where we are reasoning both about absolute coordinates in some unit and the differences. Coordinate unit types and difference unit types are supported in some other unit type systems [9].

Suppose we are computing the end position we reach, given a fixed duration of running at a fixed velocity, given an unknown start position. Then the start and end position are both coordinates (in some coordinate space), while the length, velocity, and duration are non-coordinate (difference) values. We use the notation coord($u$) to define a coordinate unit type of basic unit type $u$. The model that separates these different types is written:

Coordinate types are much more restricted than ordinary unit types, they support the following typed arithmetic operations only:

• $\mathrm{■}$

  $\text{coord}(x)+x=\text{coord}(x)$

• $\mathrm{■}$

  $\text{coord}(x)-x=\text{coord}(x)$

• $\mathrm{■}$

  $\text{coord}(x)-\text{coord}(x)=x$

So we can only add or subtract a (difference) unit value to a coordinate unit value to get another coordinate, or subtract one coordinate from another to get a (difference) unit value. Importantly, we cannot add two coordinate type values together, even if they have the same unit type. Similarly, we cannot multiply or divide a coordinate type, since this is equivalent to a repeated addition or its inverse.

Coordinate types appear frequently in scheduling and packing problems within the combinatorial problem class. We can restrict our definitions of scheduling and packing global constraints to enforce the correct use of coordinate types. For example, for disjunctive the start times are coordinates while the durations are usual (difference) unit types. With the unit typed definition (shown in the next section) we discover the error in the model at the beginning of the section. We have reversed the arguments to disjunctive. They both have the same units, so there is no unit error, but one is a coordinate type, the other not. The corrected model rewrites these two lines:

If we only rewrite just one of the two lines, we still get a type error.

Since coordinate types only seem to make sense for a single dimension, we restrict $coord(u)$ to only be defined for declared or derived basic unit types $u$. Again, this restriction is made to get stricter unit types, and hence discover more errors.

One of the strengths of constraint programming modelling languages including MiniZinc is the wide range of global constraints that they support. In order for units to be truly useful, we need to extend these global constraint definitions to use units accurately. To do so, we need to be able to define functions which are parametric in their unit types. We introduce (unit) type variables $v to appear as unit expressions. In MiniZinc the notation $$V indicates an arbitrary enumerated type.

We have developed a prototype implementation of the unit type extension to MiniZinc.⁵⁵5The prototype is available at https://www.minizinc.org/unit-types/. The implementation performs the type checking for the unit types, adds in the required coercions, and then erases the unit types from the model. Afterwards, type checking and compilation of MiniZinc continues as normal.

The concept of unit types in programming languages has a long history. For many years, it has been clear that programming languages can help avoid crucial problems by incorporating unit types [10]. The first implementation of these features was in the Pascal and Ada languages [13, 7, 3]. Since then, extensions have been proposed for many types of programming languages, including functional languages [11, 12] and object-oriented languages [1].

Research in database systems has also explored the use of unit types. Works like [8] propose extending database schemas to include unit types. In particular, when dealing with international data, where the same data might be recorded with different units, the use of unit types enables robust data storage, retrieval, and manipulation across datasets.

These days, the incorporation of units directly within programming languages and database systems seems to have dwindled. However, this can be directly attributed to the “meta” capability of modern systems, allowing the functionality to be implemented as external libraries. The widespread adoption of libraries like Boost.Units [16], mp-units [15], astropy.units [2], Pint [9], postgresql-unit [4], and many others [14] in various programming environments underscores the continued importance of unit type safety. These libraries provide extensive unit catalogues and enforce unit consistency during calculations, reducing the risk of errors in modern day scientific and engineering applications.

In the field of constraint modelling, the Pyomo constraint modelling library [5] is the only modelling tool that we are aware of that enables the use of unit types. Based on the Pint Python package, Pyomo allows users to specify units of decision variables and provides helper functions to check what the units of expressions are and to check whether they are consistent. Because Python and Pyomo do not use a strong typing system, the user is charged with ensuring the consistency of the model is checked.

In comparison to Pyomo, once unit types are added to a MiniZinc model, the checking of these types is always enforced by the compiler. In addition, the static type checking and type erasure in MiniZinc mean that using unit types incurs no significant time overhead during the translation. The additional unit type variants, counting types and coordinate types, are not available in Pyomo. Similar to Pyomo, MiniZinc’s interfaces to other languages, such as MiniZinc Python, might in the future be extended to connect to existing unit type libraries, such as Pint. By extending these interfaces to handle unit information from other library, developers can verify that unit-aware data is consistent with their unit-aware MiniZinc model.

Unit types provide stronger type safety than is usual for even strongly typed languages. While unit type extensions have been defined for almost every programming language, they are still rarely used, even though they can detect rather subtle bugs, which can have catastrophic effect (as exemplified by the Mars Climate Orbiter debacle). The problem with unit types for developers is that the overhead of using them may not appear to pay off. The trade-off for modelling languages is much more attractive, since debugging subtle errors in a model is much more challenging than in procedural code. Interestingly, there are kinds of unit types that only arise in discrete optimization, so-called counting types. In this paper, we define a lightweight but fairly complete system of unit types suitable for discrete optimization modelling languages. We have fully implemented this as an extension of the MiniZinc modelling language. In practice, we see a fairly small overhead for using them, with potentially large gains in avoiding subtle modelling errors. Unit types will be available in MiniZinc in a near future release.