Type Inference for Units of Measure

Adam Gundry

Units of measure are an example of a type system extension involving a nontrivial equational theory. Type inference for such an extension requires equational unification. This complicates the generalisation step required for let-polymorphism in ML-style languages, as variable occurrence does not imply dependency. Previous work on units of measure (by Kennedy in particular) integrated free abelian group unification into the Damas-Milner type inference algorithm, but struggled with generalisation. I describe an approach to problem solving based on incremental minimal-commitment refinements in a structured context, and hence present abelian group unification and type unification algorithms which make type generalisation direct.

Latest version: Type Inference for Units of Measure (PDF), updated 24th June 2011, rejected from TFP 2011 post-proceedings

Supplementary material: Type Inference for Units of Measure - Technical Report (PDF), updated 24th June 2011

Haskell code: download the source tarball

Slides: TFP talk (PDF) on 16th May 2011, SPLS talk (PDF) on 15th March 2011.

Previous version: Type Inference for Units of Measure (PDF), updated 1st April 2011, published in TFP 2011 pre-proceedings

Up to Adam Gundry's home page