Types and units are very different concepts. In fact it's quite hard to formalize the way units are used in everyday physics. For example, what is the type of

Types and units are very different concepts. In fact it's quite hard to formalize the way units are used in everyday physics. For example, what is the type of the / operation such that 4m/2s = 2m/s, but also 4kg/2kg = 2? It's not impossible of course, but it is highly tedious and complex to actually define these types in a formal way. Not to mention, linear algebra (matrix operations) gets REALLY ugly to define formal types for really fast if you allow different measurement units for every matrix element, like you often do in physics. And, just like the others, I never met a physics class that didn't enforce unit maths at every step of computation, starting in sixth grade. But this is done with a simple informal system, not type theory of all things. The informal system of measurement units being essentially to treat the units as special values that act as factors and obey all the usual rules of multiplication and division, and don't allow addition or subtraction.