Types for units-of-measure in f#: invited talk

ABSTRACT

Bugs caused by units-of-measure errors can have catastrophic consequences, the most famous of which was the loss in September 1999 of NASA's Mars Climate Orbiter probe, caused by a confusion between newtons (the SI unit of force) and lbf (the Imperial unit of force).

This talk will describe support for static checking and inference of units-of-measure in the F# programming language. From the programmer's perspective, the feature is not intrusive. Numeric constants are annotated with their units, user-defined types may be parameterized on units, and the compiler does the rest, flowing unit-of-measure information through to inferred types. Behind the scenes, there are a number of technical subtleties. The type inference algorithm achieves principal types through the use of (a) Abelian group unification and (b) a change-of-basis procedure when inferring polymorphic types for let-bound variables. Type schemes are presented to the programmer in a consistent style that is related to the Hermite normal form from linear algebra. In addition, there are a number of interesting interactions with F#'s support for object-oriented programming.

The talk will of course include a demonstration, and also a selection of case studies in the domains of machine learning, games programming, physics simulation, and finance.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

General Terms:
Languages

Keywords:
dimension types, ml, polymorphic type inference