Relational Parametricity and Units of Measure

Type systems for programming languages with numeric types can be extended to support the checking of units of measure. Quantification over units then introduces a new kind of parametric polymorphism with a corresponding Reynolds (1983) style of representation independence principle: that the behaviour of programs is invariant under changes to the units used. We prove this `dimensional invariance’ result and describe four consequences. The first is that the type of an expression can be used to derive equations which describe its properties with respect to scaling [akin to Wadler’s (1989) `theorems for free’ for System F]. Secondly, there are certain types which are inhabited only by trivial terms. For example, we prove that a fully polymorphic square root function cannot be written using just the usual arithmetic primitives. Thirdly, we exhibit interesting isomorphisms between types and, for first-order types, we relate these to the central theorem of classical dimensional analysis. Finally, we suggest that, for any expression whose behaviour is dimensionally invariant, there exists some equivalent expression whose type reflects this behaviour, a consequence of which would be a full abstraction result for a model of the language.