Many people have
pondered upon the idea of checking the units of measure for numerical quantities
in programs by extending the type system to catch errors such as adding a length
to a time or using pounds instead of kilograms. Polymorphic type inference and
semantics for such a system was the subject of my thesis and subsequent papers.
Recently, I've designed and implemented a units-of-measure extension to the F# programming language. This feature is available
in the September 2008 Community Technical Preview of F#.
Types for Units-of-Measure in F# (pptx) (pdf)
Invited talk at the ML Workshop 2008
Types for Units of Measure (ppt) (html)
Presented at Microsoft Research Cambridge, May 1999.
Types for Units-of-Measure: Theory and Practice
Andrew Kennedy. Lecture notes for CEFP'09, Revised July 2010, in LNCS Volume 6299. Slides in pdf and pptx.
Formalizing an Extensional Semantics for Units of Measure
Andrew Kennedy. In 3rd ACM SIGPLAN Workshop on Mechanizing Metatheory (WMM) 2008.(Talk)
Relational Parametricity and Units of Measure
Andrew Kennedy. In Proceedings of the 24th Annual ACM Symposium on Principles of Programming Languages, Paris, France, January 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.
Programming Languages and Dimensions
Andrew Kennedy. PhD Thesis, University of Cambridge. Published as Technical Report No. 391, University of Cambridge Computer Laboratory, April 1996.
Scientists and engineers must ensure that the equations and formulae which they use are dimensionally consistent,
but existing programming languages treat all numeric values as dimensionless. This thesis investigates the extension of
programming languages to support the notion of physical dimension.
A type system is presented similar to that of the programming language ML but extended with polymorphic dimension types. An algorithm which infers most general dimension types automatically is then described and proved correct.
The semantics of the language is given by a translation into an explicitly-typed language in which dimensions are passed as arguments to
functions. The operational semantics of this language is specified in the usual way by an evaluation relation defined by a set of rules. This is used to show that if a program is well-typed then no dimension errors can occur during its evaluation.
More abstract properties of the language are investigated using a denotational semantics: these include a notion of invariance under changes in the units of measure used, analogous to parametricity in the polymorphic lambda calculus. Finally the dissertation is summarised and many possible directions for future research in dimension types and related type systems are described.
Andrew Kennedy. In Proceedings of the 5th European Symposium on Programming (ESOP): Lecture Notes in Computer Science volume 788, Springer-Verlag, 1994.
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.