Type Inference for Units of Measure

submited by

Style Pass

2024-12-13 22:00:07

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