Hmm, I don't see any reason why a type system couldn't have automatic conversions like this. I remember reading about a system recently where certain typing rul

Hmm, I don't see any reason why a type system couldn't have automatic conversions like this. I remember reading about a system recently where certain typing rules would actually insert runtime code. In this particular case, it was a type system for C that would insert runtime asserts if it couldn't prove things statically, but this approach would certainly work for converting between units as well. In fact, you can even bludgeon an existing type system like Haskell's--a language well-known for not being dependently typed--into doing automatic conversions with units. This is exactly what the unittyped package[1] does, in fact. It's actually very cool. [1]: http://hackage.haskell.org/package/unittyped-0.1 http://hackage.haskell.org/package/unittyped-0.1