Andrew Kennedy's PhD thesis was about extending Hindley-Milner type inference to support units of measure. It basically boils down to extending unification to support equations over free abelian groups, which had been solved earlier in an abstract context. The approach could be integrated into just about any HM-derived language, and is shipping as part of F#.
