Dimension Types ^{⋆}

Andrew Kennedy

University of Cambridge Computer Laboratory Pembroke Street Cambridge CB2 3QG United Kingdom

                       Andrew.Kennedy@cl.cam.ac.uk

Abstract. Scientists and engineers must ensure that physical equations are dimensionally consistent, but existing programming languages treat all numeric values as dimensionless. This paper extends a strongly-typed programming language with a notion of dimension type. Our approach improves on previous proposals in that dimension types may be polymorphic. Furthermore, any expression which is typable in the system has a most general type, and we describe an algorithm which infers this type automatically. The algorithm exploits equational unification over Abelian groups in addition to ordinary term unification. An implementation of the type system is described, extending the ML Kit compiler. Finally, we discuss the problem of obtaining a canonical form for principal types and sketch some more powerful systems which use dependent and higher-order polymorphic types.

1 Introduction

One aim behind strongly-typed languages is the detection of common programming errors before run-time. Types act as a constraint on the range of allowable expressions and stop ‘impossibilities’ happening when a program is run, such as the addition of an integer and a string.

In a similar way, scientists and engineers know that an equation cannot be correct if constraints on dimensions are broken. One can never add or subtract two values of differing dimension, and the multiplication or division of two values results in values whose dimensions are also multiplied or divided. Thus the sum of values with dimensions speed and time is a dimension error, whereas their product has dimension distance.

The addition of dimensions to a programming language has been suggested many times [KL78, Hou83, Geh85, Män86, DMM86, Bal87]. Some of this work is seriously flawed and most systems severely restrict the kind of programs that can be written. House’s extension to Pascal is much better [Hou83]. In a monomorphic language it allows functions to be polymorphic over the dimension of arguments. Since the submission of this paper an anonymous referee has pointed out work by Wand and O’Keefe on dimensional inference in the style of ML type inference [WO91]. In some ways this is similar to the approach taken here and a comparison with their system is presented later in this paper.

⋆ Appeared in European Symposium on Programming ’94, LNCS Volume 788

2 Some issues

2.1 Dimension, Unit and Representation

There is often confusion between the concepts of dimension and unit [Man87]. Two quantities with the same dimension describe the same kind of property, be it length, mass, force, or whatever. Two quantities with different units but the same dimension differ only by a scaling factor. A value measured in inches is 12 times the same value measured in feet—but both have the dimension length. We say that the two units are commensurate [KL78, DMM86]. These units have simple scaling conversions. More complicated are units such as temperature measured in degrees Celsius or Fahrenheit, and even worse, amplitude level in decibels.

Base dimensions are those which cannot be defined in terms of other dimensions. The International System of Units (SI) defines seven of these—length, mass, time, electric current, thermodynamic temperature, amount of substance and luminous intensity. Derived dimensions are defined in terms of existing dimensions, for example, acceleration is distance divided by time squared. Dimensions are conventionally written in an algebraic form inside square brackets [Lan51], so for example the dimensions of force are written [MLT^{−2}].

Similarly there are base units—the SI base dimensions just listed have respective units metres, kilograms, seconds, Amperes, Kelvin, moles and Candela. Examples of derived units include inches (0.0254 metres) and newtons (kgms^{−2}).

There is also the issue of representation: which numeric type is used to store the numeric value of the quantity in question. Electrical quantities are often represented using complex numbers, whereas for distance reals are more common, and for either of these many languages provide more than one level of precision.

Dimensionless quantities are common in science. Examples include refractive index, coefficient of restitution, angle and solid angle. The last two should properly be considered dimensionless though it is tempting to think otherwise. An angle is the ratio of two lengths (distance along an arc divided by the radius) and a solid angle is the ratio of two areas (surface area on a sphere divided by the square of the radius).

2.2 Types and Polymorphism

How do these concepts of dimension, unit, and representation fit with the conventional programming language notion of type?

Expressions in a strongly typed language must be well-typed to be acceptable to a compiler. In functional languages, for example, the rule for function application insists that an expression e_{1} e_{2} has type τ_{2} if e_{1} has an arrow type of the form τ_{1} → τ_{2} and the argument e_{2} has type τ_{1}.

In a similar way, mathematical expressions must be dimensionally consistent. Expressions of the form e_{1} + e_{2} or e_{1} − e_{2} must have sub-expressions e_{1} and e_{2} of identical dimension. But in e_{1}e_{2} (product) the sub-expressions may have any dimension, say δ_{1} and δ_{2} giving a resultant dimension for the whole expression of δ_{1}δ_{2}.

So it appears that dimensions can be treated as special kind of type in a programming context. But there is the question of what to do about representation. Do we associate particular dimensions with fixed numeric types (so current is always represented by a complex number, distance by a real), or do we parameterise numeric types on dimension and give the programmer the flexibility of choosing different representations for different quantities with the same dimension?

A monomorphic dimension type system is of limited value. For non-trivial programs we would like to write general-purpose functions which work over a range of dimensions. Even something as simple as a squaring function cannot be expressed in a monomorphic system. A modern polymorphic language would use quantified variables to express the idea that this function squares the dimension of its argument, for any dimension.

2.3 Type inference

Type systems such as that of Standard ML are designed so that the compiler can infer types if the programmer leaves them out. It turns out that this is possible for a dimension type system too.

A desirable property of inferred types is that they are the most general type, sometimes called principal. Any other valid typing can be obtained from this most general type by simple substitution for type variables. Our system does have this feature, and an algorithm is described which finds the principal type if one exists.

3 The idea

The system described here is in the spirit of ML [MTH89, Pau91]. It is polymorphic, so functions such as mean and variance can be coded to work over values of any dimension. The polymorphism is implicit—dimension variables are implicitly quantified in the same way as ML type variables. It is possible for the system to infer dimension types automatically, as well as check types which the programmer specifies.

Although it is described as an extension to ML, any language with an ML-like type system would suffice; indeed, it could even be added as an extension to a monomorphically-typed language as House did with Pascal. It is a conservative extension to ML in the sense that ML-typable programs remain typable, though functions may be given a more refined type than before.

We start with a set of base dimensions such as mass, length, and time, perhaps represented by the identifiers M, L and T as is conventional. Dimensions are written inside square brackets, for example [MLT^{−2}]. This notation cannot be confused with the ML list value shorthand, although some languages such as Haskell use [τ] to denote the list type.

For polymorphic dimensions we need dimension variables. We use d_{1}, d_{2}, … to distinguish them from ordinary type variables α, β, . . .. The unit dimension (for dimensionless quantities) is indicated by [1].

We assume some kind of construct for declaring base dimensions. This could be extended to provide derived dimensions; we do not discuss this possibility here. The provision of multiple units for a single dimension is also an easy extension to the system.

3.1 Dimension types

We introduce new numeric types parameterised on dimension. The most obvious candidates are real and complex, with speeds having type [LT^{−1}] real and electric current [Current] complex. The parameter is written to the left of the type constructor in the style of Standard ML.

For the remainder of this paper we will only consider a single type constructor. In a type of the form [δ]real, δ is a dimension expression which is completely separate from other type-forming expressions and which may only appear as a parameter to numeric types.

3.2 Arithmetic

We give the following type schemes to the standard arithmetic operations:

+, −  : ∀d. [d] real × [d] real → [d] real

      ∗  : ∀d_{1}d_{2}. [d_{1}] real × [d_{2}] real → [d_{1}d_{2}] real
      /  : ∀d_{1}d_{2}. [d_{1}] real × [d_{2}] real → [d_{1}d_{2}^{−1}] real
      sqrt  : ∀d. [d^{2}] real → [d] real
      exp, ln, sin, cos, tan : [1] real → [1] real

It is often useful to coerce an integer into a dimensionless real, for which we provide a suitable function:

                        real : int → [1] real

Finally, it turns out that we need a polymorphic zero:

                          zero : ∀d. [d] real

3.3 Some examples

Use of zero. Without a polymorphic zero value we would not even be able to test the sign of a number, for example, in an absolute value function:

   fun abs x = if x < zero then zero-x else x

with type ∀d. [d] real → [d] real. It is also essential as an identity for addition in functions such as the following:

   fun sum []      = zero
     | sum (x::xs) = x + sum xs;

This has the type scheme ∀d. [d] reallist → [d] reallist.

Statistical functions. Statistics provides a nice set of example functions because we would want to apply them over a large variety of differently dimensioned quantities. We list the code for mean and variance functions:

   fun mean xs = sum xs / real (length xs);
   fun variance xs =
     let val n = real (length xs)
         val m = mean xs
     in sum (map (fn x => sqr (x - m)) xs) / (n - real 1) end;

Their principal types, with those of some other statistical functions, are:

      mean  : ∀d. [d] reallist → [d] real
      variance : ∀d. [d] reallist → [d^{2}] real
      sdeviation : ∀d. [d] reallist → [d] real
      skewness : ∀d. [d] reallist → [1] real
      correlation : ∀d_{1}d_{2}. [d_{1}] reallist → [d_{2}] reallist → [1] real

Differentiation. We can write a function which differentiates another function numerically. It accepts a function f as argument and returns a new function which is the differential of f. We must also provide an increment h.

   fun diff h f = fn x => (f (x+h) - f (x-h)) / (real 2 * h)

This has type scheme

   ∀d_{1}d_{2}. [d_{1}] real → ([d_{1}] real → [d_{2}] real) → ([d_{1}] real → [d_{2}d_{1}^{−1}] real)

Unlike the statistical examples, the type of the result is related to the type of more than one argument.

Root finding. Here is a tiny implementation of the Newton-Raphson method for finding roots of equations:

   fun newton (f, f', x, eps) =
     let val dx = f x / f' x
         val x' = x - dx
     in if abs dx < eps then x' else newton (f, f', x', eps) end;

It accepts a function f, its derivative f', an initial guess x and an accuracy eps. Its type is

        ∀d_{1}d_{2}. ([d_{1}] real → [d_{2}] real) × ([d_{1}] real → [d_{1}^{−1}d_{2}] real)×
            [d_{1}] real × [d_{1}] real → [d_{1}] real

Powers. To illustrate a more unusual type, here is a function of three arguments.

   fun f (x,y,z) = x*x + y*y*y + z*z*z*z*z

This has the inferred type scheme

            ∀d. [d^{15}] real × [d^{10}] real × [d^{6}] real → [d^{30}] real

4 A dimension type system

We formalise the system by considering a very small ML-like language. Dimension expressions are defined by:

δ ::= d | B | δ · δ | δ^{−1} | 1

where B is any base dimension and d is any dimension variable. The shorthand d^{n} (n ∈ ℕ) will be used to stand for the n-fold product of d with itself, and occasionally we will write d_{1}d_{2} instead of d_{1} · d_{2}.

Now we define monomorphic type expressions by:

τ ::= α | [δ] real | τ → τ

where α is any type variable. Polymorphic type expressions, also called type schemes are defined by

σ ::= τ | ∀α.σ | ∀d.σ

We have extended the usual ML-style type schemes with quantification over dimension variables, which must be distinct from type variables in order to distinguish the two kinds of quantification. The flavour of polymorphism used for dimension types is the same as ordinary ML-like polymorphism. This leads to the usual problems but does mean that inference is straightforward. We shall have more to say on this subject later.

Finally, expressions are defined by

e ::= x | n | e e | λx.e | let x = e in e

where x is a variable and n is a real-valued constant such as 3.14. The full set of inference rules is now given, based on Cardelli [Car87]. Only two new rules are required—generalisation and specialisation for dimension quantification. A_{x} denotes the type assignment obtained from A by removing any typing statement for x.

VAR A ⊢ x : σ A(x) = σ  REAL A ⊢ n : [1] real

GEN {A ⊢ e : σ \atop A ⊢ e : ∀α.σ} α not free in A  SPEC {A ⊢ e : ∀α.σ \atop A ⊢ e : σ[τ/α]}

DGEN {A ⊢ e : σ \atop A ⊢ e : ∀d.σ} d not free in A  DSPEC {A ⊢ e : ∀d.σ \atop A ⊢ e : σ[δ/d]}

ABS {A_{x} ∪ \{x : τ\} ⊢ e : τ′ \atop A ⊢ λx.e : τ → τ′}  APP {A ⊢ e : τ → τ′  A ⊢ e′ : τ \atop A ⊢ e e′ : τ′}

LET {A ⊢ e : σ  A_{x} ∪ \{x : σ\} ⊢ e′ : τ \atop A ⊢ let x = e in e′ : τ}

In addition to these rules we have equations relating dimensions:

δ_{1}δ_{2} =_{D} δ_{2}δ_{1}  (commutativity)
(δ_{1}δ_{2})δ_{3} =_{D} δ_{1}(δ_{2}δ_{3}) (associativity)
1 · δ =_{D} δ  (identity)
δδ^{−1} =_{D} 1  (inverses)

and an inference rule relating equivalent types:

DEQ {A ⊢ e : τ_{1}  ⊢ τ_{1} =_{D} τ_{2} \atop A ⊢ e : τ_{2}}

where =_{D} is lifted to types by the obvious congruence.

It will be observed that none of the rules explicitly introduces types involving base dimensions. We assume that there is a means of declaring constants which represent a base unit for a particular base dimension. For the length dimension, for example, we might have have a constant metre of type [L] real.

5 Dimensional Type Inference

5.1 Unification—algorithm Unify

At the heart of most type inference algorithms is the process of unification. Given an equation of the form

τ_{1} =^{?} τ_{2}

we wish to find the most general unifier, a substitution S such that

1. S(τ_{1}) = S(τ_{2})

2. For any other unifier S′ there is a substitution S′′ such that S′′ ∘ S = S′.

If equality is purely syntactic, there is a straightforward algorithm first devised by Robinson. It accepts a pair of types τ_{1} and τ_{2} and returns their most general unifier or fails if there is none.

Unify(α, α)  = the identity substitution
Unify(α, τ) = Unify(τ, α) = if α is in τ then fail (no unifier exists)

else return the substitution {α ↦ τ}

Unify(τ_{1} → τ_{2}, τ_{3} → τ_{4}) = S_{2} ∘ S_{1}

where S_{1} = Unify(τ_{1}, τ_{3})

and S_{2} = Unify(S_{1}(τ_{2}), S_{1}(τ_{4}))

To extend this to deal with types of the form [δ] real, we unify dimensions using another algorithm DimUnify. The additional clause is simply

Unify([δ_{1}] real, [δ_{2}] real) = DimUnify(δ_{1}, δ_{2})

5.2 Dimensional Unification—algorithm DimUnify

We require an algorithm DimUnify which accepts two dimension expressions δ_{1} and δ_{2} and returns a substitution S over the dimension variables in the expressions such that

1. S(δ_{1}) =_{D} S(δ_{2})

2. For any other unifier S′ there is a substitution S′′ such that S′′ ∘ S =_{D} S′.

This kind of unification is sometimes called equational, in contrast to ordinary Robinson unification which is syntactic or free. In our dimension type system, we want to unify with respect to the four laws listed earlier: associativity, commutativity, identity and inverses. It turns out that this particular brand of unification is decidable and unitary [Baa89, Nut90]: there is a single most general unifier if one exists at all. This has the consequence that, as for ML polymorphic types, if an expression is typable then it has a most general type from which any other type may be derived by simple substitution for dimension variables.

We will use Lankford’s algorithm for Abelian group unification [LBB84]. It relies on the solution of linear equations in integers, for which there exist several algorithms including one by Knuth [Knu69]. Our treatment is slightly different in that we consider only a single equation.

First we transform the equation to the normalised form

d_{1}^{x_{1}} · d_{2}^{x_{2}} ⋯ d_{m}^{x_{m}} · B_{1}^{y_{1}} · B_{2}^{y_{2}} ⋯ B_{n}^{y_{n}} =^{?}_{D} 1

where d_{i} and B_{j} are distinct dimension variables and base dimensions.

Start by setting S to the empty substitution. If m = 0 and n = 0 then we are finished already. If m = 0 and n ≠ 0 then fail: there is no unifier. Otherwise, find the dimension variable with exponent x_{k} of smallest absolute value in the equation. If x_{k} is negative, first take reciprocals of both sides by negating all exponents. Without loss of generality, we can assume that k = 1.

1. If ∀i. x_{i} mod x_{1} = 0 and ∀j. y_{j} mod x_{1} = 0, then the unifier is the following, composed with S.

d_{1} ↦ d_{2}^{−x_{2}/x_{1}} ⋯ d_{m}^{−x_{m}/x_{1}} · B_{1}^{−y_{1}/x_{1}} ⋯ B_{n}^{−y_{n}/x_{1}}

2. Otherwise introduce a new variable d and compose with S the substitution

d_{1} ↦ d · d_{2}^{−⌊x_{2}/x_{1}⌋} ⋯ d_{m}^{−⌊x_{m}/x_{1}⌋} · B_{1}^{−⌊y_{1}/x_{1}⌋} ⋯ B_{n}^{−⌊y_{n}/x_{1}⌋}

to transform the equation to

d^{x_{1}} · d_{2}^{x_{2} modx_{1}} ⋯ d_{m}^{x_{m} modx_{1}} · B_{1}^{y_{1} modx_{1}} ⋯ B_{n}^{y_{n} modx_{1}} =^{?}_{D} 1

If at this stage there are no variables in the equation other than d then there is no solution—no unifier exists. Otherwise find the smallest exponent again and repeat the procedure.

This method must terminate because on each iteration we reduce the size of the smallest nonzero coefficient in the equation.

5.3 Inference—algorithm Infer

The type inference algorithm for ML is well-known and has been presented in many places. Our version differs in two respects—quantified dimension variables are instantiated at the same time as quantified type variables (when e is a variable), and generalization over free dimension variables is added to the usual generalization over free type variables (when e is a let-expression).

Given a type assignment A and an expression e, the algorithm Infer determines a pair (S, τ) where τ is the most general type of e and S is a substitution over the type and dimension variables in A under which this is true.

Infer(A, x) = (I, τ[d′_{1}/d_{1}, …, d′_{m}/d_{m}, α′_{1}/α_{1}, …, α′_{n}/α_{n}])

where A(x) is ∀d_{1} … d_{m}.∀α_{1} … α_{n}.τ d′_{1}, …, d′_{m} are fresh dimension variables α′_{1}, …, α′_{n} are fresh type variables

Infer(A, e_{1}e_{2}) = (S_{3} ∘ S_{2} ∘ S_{1}, S_{3}(α))

where (S_{1}, τ_{1}) = Infer(A, e_{1}) (S_{2}, τ_{2}) = Infer(S_{1}(A), e_{2}) S_{3} = Unify(S_{2}(τ_{1}), τ_{2} → α) α is a fresh type variable

Infer(A, λx.e) = (S, S(α) → τ)

where (S, τ) = Infer(A_{x} ∪ {x : α}, e) α is a fresh type variable

Infer(A, let x = e in e′) = (S_{2} ∘ S_{1}, τ_{2})

where (S_{1}, τ_{1}) = Infer(A, e) (S_{2}, τ_{2}) = Infer(S_{1}(A_{x}) ∪ {x : ∀d_{1}, …, d_{m}.∀α_{1}, …, α_{n}.τ_{1}}, e′) d_{1}, …, d_{m} are free dimension variables in τ_{1} not in S_{1}(A) α_{1}, …, α_{n} are free type variables in τ_{1} not in S_{1}(A)

The algorithm’s correctness is shown by two theorems [Lei83, Dam85].

Theorem 1 (Soundness of Infer). If Infer(A, e) succeeds with result (S, τ) then there is a derivation of S(A) ⊢ e : τ.

Theorem 2 (Syntactic Completeness of Infer). If there is a derivation of S(A) ⊢ e : τ then Infer(A, e) is a principal typing for e, i.e. it succeeds with result (S_{0}, τ_{0}) and S =_{D} S′ ∘ S_{0}, τ =_{D} S′(τ_{0}) for some substitution S′.

To prove these theorems we first devise a syntax-oriented version of the inference rules and prove that they are equivalent to the rules given here. Then the proofs follow more straightforwardly by induction on the structure of e; these will appear in a fuller version of this paper.

6 Implementation

The dimension type system described in this article has been implemented as an extension to the ML Kit compiler [Rot92], which is a full implementation of Standard ML as defined in [MTH89].

In order to fit naturally with the rest of Standard ML, the concrete syntax of dimension types is necessarily messy. Dimension variables are distinguished from ordinary type variables and identifiers by an initial underline character, as in _a. Base dimensions are ordinary identifiers declared by a special construct. This might also be used to introduce constants representing the base units for the dimension specified, as mentioned in section 4:

   dimension M unit kg;
   dimension L unit metre;
   dimension T unit sec;

It would be easy to extend this to permit derived dimensions, in a fashion similar to ML type definition.

Dimension expressions are enclosed in square brackets, as is conventional. This happens to fit nicely with the notation for parameterised types. The unit dimension is simply []. Exponents are written after a colon (e.g. area is [L:2]) and product is indicated by simple concatenation (e.g. density is [M L:~3]).

Any new type or datatype may be parameterised by dimension, by type, or by a mixture of both. Assuming a built-in real type we could define complex by

   datatype [_a] complex = make_complex of [_a] real * [_a] real

Built-in functions as defined in the prelude are given new types, for example:

   val sqrt : [_a:2] real -> [_a] real
   val sin : [] real -> [] real
   val + : [_a] real * [_a] real -> [_a] real
   val * : [_a] real * [_b] real -> [_a _b] real

The one major problem is ML’s overloading of such functions. The Definition of Standard ML gives types such as num*num -> num to arithmetic and comparison functions. A type-checker must use the surrounding context to determine whether num is replaced by real or int. We want to give dimensionally polymorphic types to these functions. This makes the Definition’s scheme unworkable, especially in the case of multiplication. The current implementation has alternative names for dimensioned versions of these operations.

7 Some Problems

7.1 Equivalent types

ML type inference determines a most general type, if there is one, up to renaming of type variables. For example, the type scheme ∀αβ. α × β is equivalent to ∀αβ. β × α. This equivalence is easy for the programmer to understand.

For dimension types, we have principal types with respect to the equivalence relation =_{D}, but there is no obvious way of choosing a canonical representative for a given equivalence class—there is no “principal syntax”. Type scheme ∀d_{1} … d_{n}.τ_{1} is equivalent to ∀d_{1} … d_{n}.τ_{2} if there are substitutions S_{1} and S_{2} over the bound variables d_{1} to d_{n} such that

\begin{matrix}S_{1}(τ_{1}) =_{D} τ_{2} \\ and \\ S_{2}(τ_{2}) =_{D} τ_{1} \end{matrix}

This is not just =_{D} plus renaming of type and dimension variables. For example, the current implementation of the system described in this article assigns the following type scheme to the correlation example of section 3.3.

           ∀d_{1}d_{2}. [d_{1}] reallist → [d_{2}d_{1}^{−1}] reallist → [1] real

which is equivalent to

            ∀d_{1}d_{2}. [d_{1}] reallist → [d_{2}] reallist → [1] real

by the substitutions d_{2} ↦ d_{2}d_{1} (forwards) and d_{2} ↦ d_{2}d_{1}^{−1} (backwards). The second of these types is obviously more “natural” but I do not know how to formalise this notion and modify the inference algorithm accordingly.

In some cases there does not even appear to be a most natural form for the type. The following expressions are different representations of the principal type scheme for the differentiation function of section 3.3.

   ∀d_{1}d_{2}. [d_{1}] real → ([d_{1}] real → [d_{2}] real) → ([d_{1}] real → [d_{2}d_{1}^{−1}] real)

and

    ∀d_{1}d_{2}. [d_{1}] real → ([d_{1}] real → [d_{1}d_{2}] real) → ([d_{1}] real → [d_{2}] real)

7.2 Dependent types

Consider a function for raising real numbers to integral powers:

   fun power 0 x = 1.0
     | power n x = x*power (n-1) x

Because the dimension of the result depends on an integer value, our system cannot give any better type than the dimensionless

                      int → [1] real → [1] real

This seems rather limited, but variable exponents are in fact rarely seen in scientific programs except in dimensionless expressions such as power series. A dependent type system would give a more informative type to this function:

                  ∀d. Πn ∈ int . [d] real → [d^{n}] real

There are also functions which intuitively should have a static type expressible in this system, but which cannot be inferred. Geometric mean is one example. It seems as though its type should be ∀d.[d] real list → [d] real, like the arithmetic mean mentioned earlier. Unfortunately its definition makes use of rpower and prod both of which have dimensionless type:

   fun rpower (x,y) = exp(y*ln x);
   fun prod []      = 1.0
     | prod (x::xs) = x*prod xs;
   fun gmean xs = rpower(prod xs, 1.0 / real (length xs))

7.3 Polymorphism

Recursive definitions in ML are not polymorphic: occurrences of a recursively defined function inside the body of its definition can only be used monomorphically. For the typical ML programmer this problem rarely manifests itself. Unfortunately it is a more serious irritation in our dimension type system.

   fun prodlists ([], [])       = []
     | prodlists (x::xs, y::ys) = (x*y) :: prodlists (ys,xs)

The function prodlists calculates products of corresponding elements in a pair of lists, but bizarrely switches the arguments on the recursive call. Naturally this makes no difference to the result, given the commutativity of multiplication, but whilst a version without the exchange is given a type scheme

         ∀d_{1}d_{2}. [d_{1}] reallist × [d_{2}] reallist → [d_{1}d_{2}] reallist

the version above has the less general

            ∀d. [d] reallist × [d] reallist → [d^{2}] reallist

An analagous example in Standard ML is the (useless) function shown here:

   fun funny c x y = if c=0 then 0 else funny (c-1) y x

This has inferred type ∀α. int → α → α → int but might be expected to have the more general type ∀αβ. int → α → β → int. Extensions to the ML type system to permit polymorphic recursion have been proposed. It has been shown that the inference problem for such a system is undecidable [Hen93, KTU93].

The lack of polymorphic lambda-abstraction also reduces the generality of inferred types:

   fun twice f x = f (f x);
   fun sqr x     = x*x;
   fun fourth x  = (twice sqr) x;

The following type schemes are assigned:

twice : ∀α. (α → α) → (α → α)

                   sqr : ∀d. [d] real → [d^{2}] real
                   fourth : [1] real → [1] real

We would like fourth to have type ∀d. [d] real → [d^{4}] real but cannot have it because this would require sqr to be used at two different instances inside twice, namely ∀d. [d] real → [d^{2}] real and ∀d. [d^{2}] real → [d^{4}] real.

This is a serious problem but not unpredictable so long as the programmer fully understands the nature of ML-style polymorphism. The same situation occurs in ordinary ML if we change the definition of sqr to be (x, x). This time we expect fourth to have the type ∀α. α → (α × α) × (α × α) but the expression is untypable because sqr must be used at the two instances ∀α. α → α × α and ∀α. α × α → (α × α) × (α × α). In fact, we cannot even write such a term in the second-order lambda calculus. It requires either a higher-order type system such as F_{ω}, or a system with intersection types, in which we could give twice the type

∀αβγ. (α → β) ∧ (β → γ) → (α → γ)

and pass in sqr at two instances.

8 Related work

8.1 House’s extension to Pascal

Before Wand and O’Keefe’s recent work, the only attempt at a polymorphic dimension type system was the extension to Pascal proposed by House [Hou83]. In that system, types in procedure declarations may include a kind of dimension variable, as in the following example:

   function ratio(a : real newdim u; b : real newdim v)
     : real dim u/v;
   begin
     ratio := a/b
   end;

Compared with modern notions of polymorphism, this is rather strange; the newdim construct introduces a new variable standing for some dimension, and dim makes use of already-introduced variables. It is as though newdim contains an implicit quantifier.

8.2 Wand and O’Keefe’s system

Wand and O’Keefe define an ML-like type system extended with a single numeric type paramaterised on dimension [WO91]. This takes the form Q(n_{1}, …, n_{N}) where n_{i} are number expressions formed from number variables, rational constants, addition and subtraction operations, and multiplication by rational constants. It differs from the [δ] real type of this paper in two ways:

1. A fixed number of base dimensions N is assumed. Dimension types are expressed as a N-tuple of number expressions, so if we have three base dimensions M, L and T, then Q(n_{1}, n_{2}, n_{3}) represents the dimension [M^{n_{1}}L^{n_{2}}T^{n_{3}}].

2. Dimensions have rational exponents. This means, for instance, that the type of the square root function can be expressed as

∀i, j, k. Q(i, j, k) → Q(0.5 ∗ i, 0.5 ∗ j, 0.5 ∗ k)

in contrast to

∀d. [d^{2}] real → [d] real

in our system, and this function may be applied to a value of type Q(1, 0, 0), whereas our system disallows its application to [M] real.

Their inference algorithm, like ours, generates equations between dimensions. But in their system there are no “dimension constants” (our base dimensions) and equations are not necessarily integral, so Gaussian elimination is used to solve them.

Wand and O’Keefe’s types are unnecessarily expressive and can be nonsensical dimensionally. Consider the type ∀i, j, k. Q(i, j, k) → Q(i, 2 ∗ j, k) which squares the length dimension but leaves the others alone, or ∀i, j, k. Q(i, j, k) → Q(j, i, k) which swaps the mass and length dimensions. Fortunately no expression in the language will be assigned such types. Also, non-integer exponents should not be necessary—polymorphic types can be expressed without them and values with fractional dimension exponents do not seem to occur in science.

They propose a construct newdim which introduces a local dimension. In our system the dimension declaration could perhaps be used in a local context, in the same way that the datatype construct of ML is used already.

The problem of finding canonical expressions for types presumably occurs in their system too, as well as the limitations of implicit polymorphism described here.

9 Conclusion and Future Work

The system described in this paper provides a natural way of adding dimensions to a polymorphically-typed programming language. It has been implemented successfully, and it would be straightforward to add features such as derived dimensions, local dimensions, and multiple units of measure within a single dimension.

To overcome the problems discussed in section 7 it might be possible to make the system more polymorphic, but only over dimensions in order to retain decidability. An alternative which is being studied is the use of intersection types.

So far no formal semantics has been devised for the system. This would be used to prove a result analagous to the familiar “well-typed programs cannot go wrong” theorem for ML.

Acknowledgements

This work was supported financially by a SERC Studentship. I would like to thank Alan Mycroft, Francis Davey, Nick Benton and Ian Stark for discussions on the subject of this paper, and the anonymous referees for their comments.

References

[Baa89] F. Baader. Unification in commutative theories. Journal of Symbolic Computation, 8:479–497, 1989.

[Bal87] G. Baldwin. Implementation of physical units. SIGPLAN Notices, 22(8):45– 50, August 1987.

[Car87] L. Cardelli. Basic polymorphic typechecking. Science of Computer Programming, 8(2):147–172, 1987.

[Dam85] L. Damas. Type Assignment in Programming Languages. PhD thesis, Department of Computer Science, University of Edinburgh, 1985.

[DMM86] A. Dreiheller, M. Moerschbacher, and B. Mohr. PHYSCAL—programming Pascal with physical units. SIGPLAN Notices, 21(12):114–123, December 1986.

[Geh85] N. H. Gehani. Ada’s derived types and units of measure. Software—Practice and Experience, 15(6):555–569, June 1985.

[Hen93] F. Henglein. Type inference with polymorphic recursion. ACM Transactions on Programming Languages and Systems, April 1993.

[Hou83] R. T. House. A proposal for an extended form of type checking of expressions. The Computer Journal, 26(4):366–374, 1983.

[KL78] M. Karr and D. B. Loveman III. Incorporation of units into programming languages. Communications of the ACM, 21(5):385–391, May 1978.

[Knu69] D. Knuth. The Art of Computer Programming, Vol. 2, pages 303–304. Addison-Wesley, 1969.

[KTU93] A. J. Kfoury, J. Tiuryn, and P. Urzyczyn. Type reconstruction in the presence of polymorphic recursion. ACM Transactions on Programming Languages and Systems, April 1993.

[Lan51] H. L. Langhaar. Dimensional Analysis and Theory of Models. John Wiley and Sons, 1951.

[LBB84] D. Lankford, G. Butler, and B. Brady. Abelian group unification algorithms for elementary terms. Contemporary Mathematics, 29:193–199, 1984.

[Lei83] D. Leivant. Polymorphic type inference. In ACM Symposium on Principles of Programming Languages, 1983.

[Män86] R. Männer. Strong typing and physical units. SIGPLAN Notices, 21(3):11–

20, March 1986.

[Man87] R. Mankin. letter. SIGPLAN Notices, 22(3):13, March 1987.

[MTH89] R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, Cambridge, Mass., 1989.

[Nut90] W. Nutt. Unification in monoidal theories. In 10th International Conference on Automated Deduction, volume 449 of Lecture Notes in Computer Science, pages 618–632. Springer-Verlag, July 1990.

[Pau91] L. C. Paulson. ML for the Working Programmer. Cambridge University Press, 1991.

[Rot92] N. Rothwell. Miscellaneous design issues in the ML Kit. Technical Report ECS-LFCS-92-237, Laboratory for Foundations of Computer Science, University of Edinburgh, 1992.

[WO91] M. Wand and P. M. O’Keefe. Automatic dimensional inference. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1991.