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