I agree that units aren't types. However, I think there's validity to thinking about concepts such as acceleration vs. speed vs. mass etc. as distinct types.
Each of those can be specified with different units from different systems of measurement. Some of those are compatible with one another, given some transformations. E.g. for speed, one can convert X m/s into MPH: different units, but same type.
However, mass is incompatible with acceleration: there's no possible valid transformation for Y grams into m/^2. If I was writing a program, I would like the language to prevent me from putting in a mass value into a place where I need a velocity. If I was writing a physics "proof," it would similarly be invalid to intermix values from these two distinct concepts.
I agree that types are a decent way of representing measurement units for many common use cases.
But I think the difference between the two is more fundamental. It's true of course that you can't transform a mass into a speed.
However, the interesting thing is that you can multiply 5kg by 10 meters/second and get 50m×kg/s, and this is a meaningful operation (in this case, you get a momentum). You can then divide this by 5s and get 10m×kg/s² which is still meaningful (a change in momentum). Even more, you can now divide this by 5kg/s (a change in mass), and get 2m/s (speed).
The way multiplication and division work with measurement units, you can't easily define them as functions that take the measurement units of their parameters as types, since you'd constantly get new types. E.g. the type of `x = foldl (×) listOfMeterQuantties` would be `meter^len(listOfMeterQuantties)`. You could do this in a dependently-typed language of course, but it would be quite unnatural I think.
Essentially, the way you'd probably represent all this is to have a single type family that has a numeric parameter for every measurement unit you want to be able to represent. It would be something like PhysicalQuantity<X, Y, Z, W> == 1 m^X s^Y kg^Z k^W. + and - would be defined on pairs of PhysicalQuantity<X, Y, Z, W> and PhysicalQuantity<X, Y, Z, W>. × and / would be defined on pairs of PhysicalQuantity<X1, Y1, Z1, W1> and PhysicalQuantity<X2, Y2, Z2, W2> and they would produce PhysicalQuantity<X1+X2, Y1+Y2, Z1+Z2, W1+W2> (or - for division). How usable this would then be (i.e. the type of "1m" would be PhysicalQuantity<1,0,0,0>) is debatable. But even if it would be good enough, I think it is quite apparent that the type representation is nowhere near intuitive or direct.
Each of those can be specified with different units from different systems of measurement. Some of those are compatible with one another, given some transformations. E.g. for speed, one can convert X m/s into MPH: different units, but same type.
However, mass is incompatible with acceleration: there's no possible valid transformation for Y grams into m/^2. If I was writing a program, I would like the language to prevent me from putting in a mass value into a place where I need a velocity. If I was writing a physics "proof," it would similarly be invalid to intermix values from these two distinct concepts.