A Typechecker Plugin for Units of Measure

Domain-specific constraint solving in GHC Haskell

Adam Gundry

Typed functional programming and units of measure are a natural combination, as F# ably demonstrates. However, encoding statically-checked units in Haskell’s type system leads to inevitable disappointment with the usability of the resulting system. Extending the language itself would produce a much better result, but it would be a lot of work! In this paper, I demonstrate how typechecker plugins in the Glasgow Haskell Compiler allow users to define domain-specific constraint solving behaviour, making it possible to implement units of measure as a type system extension without rebuilding the compiler. This paves the way for a more modular treatment of constraint solving in GHC.

Latest version: A Typechecker Plugin for Units of Measure (PDF), updated 17th July 2015, to appear in Haskell Symposium 2015 © Adam Gundry 2015. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record will appear in the proceedings of the Haskell Symposium 2015, doi:10.1145/2804302.2804305.

Previous version: A Typechecker Plugin for Units of Measure (PDF), updated 3rd March 2015, submitted to Haskell Symposium 2015

Haskell code: uom-plugin on GitHub

Up to Adam Gundry's home page