Lambda the Ultimate

Relational Parametricity and Units of Measure, Andrew J. Kennedy, POPL 1997.

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-style 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 `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 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.

There's a new release of F# coming out with support for measure types, and so I thought I'd post a link to Andrew's paper about the subject. Now, if you've done any physics or engineering, you're probably familiar with the fact that units can sometimes really strongly constrain what form your equations can take. If you studied dimensional analysis more carefully than I did, you might even have learned that this is a consequence of the Buckingham pi theorem -- you can prove that if you have an equation with n variables involving k physical units, you can recast it as an equation with (n - k) dimension-free variables. Kennedy shows that the analogue of this theorem for programs in his language is a form of parametricity result at first order, which is quite slick.