Relational Parametricity and Units of Measure

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.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Units of Measure in F#

Andrew Kennedy (the author of the article himself) started a blog series on Units of Measure in F#:

From the archives.

From the archives.

I think this is a different

I think this is a different paper, actually -- the one you link to is a 1994 ESOP paper primarily describing how unit inference can be done, whereas the one I posted is about the "free theorems" these types enable. It's well worth linking to the older discussion, though!

I didn't mean it was the

I didn't mean it was the same paper, just wanted to link to the discussion. Sorry for the confusion.

a new release of F# that works on Mono

There's a new release of F# coming out...

And happily it seems to work on Mono (Release Candidate 1)