A mathematical formalisation of dimensional analysis
terrytao.wordpress.com
terrytao.wordpress.com
“There are several reasons why it is advantageous to retain the limitation to only perform dimensionally consistent operations. One is that of error correction: one can often catch (and correct for) errors in one’s calculations by discovering a dimensional inconsistency, and tracing it back to the first step where it occurs.”
This is basically describing the “stack trace” you get when typechecking a program.
“By performing dimensional analysis, one can often identify the form of a physical law before one has fully derived it.”
This is tantamount to saying that it’s possible to glean an implementation from a type, which is true—the implementations of all total functions with a given type are (I think) recursively enumerable.
Different units of the same kind could define implicit conversions—for example, metres and yards are both of kind “length”. Each kind would be associated with an underlying type or interface—for example, length only makes sense for scalar values, such as integers and floats.
F# units of measure are an implementation of this special case. You could generalise it, though, to associate arbitrary static metadata with a type. That seems potentially useful, and like something someone should do.
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.
Nevertheless, for some audience, in which I am included, the connection to type theory seems blatantly obvious and it would've been a better article for us had it been presented in that light.
"...explaining for instance why in any trigonometric identity such as
sin(x+y) = sin(x) cos(y) + cos(x) sin(y)
I never thought of it that way. I always converted to exponential notation to derive them, but you could use this units approach to provide what you needed.