This article appears to be describing a type system without making use of anything type-theoretical. Maybe it’s just my inexperience with mathematical language, but the presentation seems to suffer badly as a result. The system in question is actually rather simple.
“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.
Agreed -- it was difficult to get motivated to read deeply into the article when I was wondering why there is more to say than "values in physics should be strongly typed".
The system itself is interesting, though. In the simple case, a dimension associated with a value is a product of nonzero integer powers of units of different kinds—in the type theory sense—which may be the empty set for dimensionless values.
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.
But dimensional analysis has an automatic method of transforming objects of one type to another. When you talk about "strongly typed", I think you mean the programming concept, in which there is no such automatic method.
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.
Many type systems do include a notion of automatic (implicit) conversion between types. This doesn’t preclude strong typing in the usual sense; then again, “strong” is kind of a soft term, which isn’t really used in type theory.
It's possible, because you aren't a mathematician, that you aren't aware of who Terrence Tao is. He is one of the most celebrated mathematicians of our time, and a prolific one at that. His goal is emphatically not to explain what dimensional analysis is, but to provide a basis for a mathematical formalism for it that does not fully exist yet.
That doesn't seem to be any sort of refutation of the given complaint. Sure, Terrence Tao is a great mathematician, and he may trying to do something that type theorists haven't done yet, and we can reasonably give him the benefit of the doubt and assume that, even though he didn't mention it, he may well be familiar with type theory and left out reference to it on purpose.
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.
It's not the same as type theory because the relationships between physical units are actually tied by real mathematical operations. A float and a string do not combine in any sensible way (aside from type-casting, which is entirely different). This suggests that type theory as you are familiar with isn't as connected as you might think.
There are plenty of systems making use of the algebraic operations of product (tuple) and sum (disjoint union) on types. These are regularly extended with notions of exponentiation, division, subtraction, complement, union, and intersection. There is little formal reason why an algebra of types shouldn’t include even more interesting operations.
OK, but what kind of experience does Tao (I was actually well aware of who he was) have with programming and type theory in particular? By the way, is not the type theory already a formalism? Cannot we construct formal proofs with it? Is it possible that he reinvents the wheel and describes a rather trivial thing in an overcomplicated roundabout way? Do you imply that a 'real' mathematical formalism is better than a formalism from the computer science? After all, equivalence is essential to mathematics, pretty everything can be represented and intuitively understood in a different equivalent way. This article is too long for me to crack it that fast, so maybe I am just not quite there yet in understanding.
It isn't a mathematical formalism. I have studied books on lambda calculus and all that. A computer scientist's understanding of what "well-defined" means is very different from a mathematician's. It's not to say that it doesn't work, just that the standard is very very different. The standard of well-definedness for a physicist and a mathematician is also very different. Example: compare what constitutes a "good enough" definition of a real number to these three disciplines.
Could you elaborate on your perception of definitions of lambda calculus? Or, say, SK calculus. They’re very simple systems and entirely syntax-directed, so I’m curious to know where they “go wrong”—how would you prefer a definition be presented?
You're analogy may be a nice one, but I don't feel this detracts from the details of the piece. I am a professional developer and have a MSc in Mathematics yet the maths in this article is at the very upper reach of what I can understand. Terence Tao is, by most accounts, a brilliant mathematician, with both clarity of vision and nitty gritty technical excellence. Sometimes different disciplines talk of the same things in different languages, it's true, but to declare that the description in your discipline trumps that of another's before you understand both in detail is miss-guided.
I didn’t mean to come off as elitist or anything. It’s definitely interesting to see the line of thinking, and to learn about the formalisms used along the way. But it would benefit, in my mind, from a stronger conclusion: “Look at this system I have derived for physics, using pure mathematics. Observe all its glorious juicy detail. Now look at how elegantly I can express it using type theory.”
I used scare quotes because the trace has more to do with the structure of the AST than the evaluation of the program. In Haskell, for instance, a type error is given in descending order of detail: “no instance for (Num String) arising from a use of ‘+’, in the expression 5 + a, in the expression let a = "foo" in 5 + a, …”
I know it's a side point, but I loved the comment:
"...explaining for instance why in any trigonometric identity such as
sin(x+y) = sin(x) cos(y) + cos(x) sin(y)
the number of odd functions (sine, tangent, cotangent, and their inverses) in each term has the same parity."
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.
19 comments
[ 2.7 ms ] story [ 49.4 ms ] thread“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.
[1]: http://hackage.haskell.org/package/unittyped-0.1
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
the number of odd functions (sine, tangent, cotangent, and their inverses) in each term has the same parity."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.