Units / dimensional analysis in physics is really a kind of type system. I was very big into using that for error checking when I used to do physics and engineering calculations professionally. (Helps with self-documenting too.) I invented my own weird way to do it that would allow them to be used in places where actual proper types & type-checking systems weren’t supported—like most numerical calculation packages, or C, or Microsoft Excel, etc.
the more you constrain what you and others can do, the easier it is to reason about it, and check much more properties. So type systems often forbid programs that would actually run without runtime errors, but which are completely messed up to think about.
Yeah a case where this came up for me is angles (radians, degrees, steradians, etc.). If you treat radians as a “unit” subjected to dimensional analysis, you wind up needing to manually insert and remove the radian unit in a bunch of places, which is somewhat confusing and annoying. Sometimes I found it was a good tradeoff, other times not—I tended to treat angles as proper type-checked units only for telescope and camera design calculations, but not in other contexts like accelerometers or other things where angles were only incidentally involved.
Units / dimensional analysis in physics is really a kind of type system. I was very big into using that for error checking when I used to do physics and engineering calculations professionally.
Definitely!
Dimensional analysis was the first place this analogy jumped to me when reading Fly By Night Physics, because it truly used dimensions not only to check results, but also to infer the general shape of the answer (which is also something you can do in type systems, for example a function with a generic type a→a can only be populated by the identity function, because it cannot not do anything else than return its input).
Although in physics you need more tricks and feels to do it correctly. Like the derivation of the law of the pendulum just from dimensional analysis requires you to have the understanding of forces as accelerations to know that you can us g here.
Dimensions are also a perennial candidate for things that should be added to type systems, with people working quite hard at implementing it (just found this survey from 2018).
I invented my own weird way to do it that would allow them to be used in places where actual proper types & type-checking systems weren’t supported—like most numerical calculation packages, or C, or Microsoft Excel, etc.
I looked at the repo, and was quite confused how you did it, until I read
A complete set of independent base units (meters, kilograms, seconds, coulombs, kelvins) are defined as randomly-chosen positive floating-point numbers. All other units and constants are defined in terms of those. In a dimensionally-correct calculation, the units all cancel out, so the final answer is deterministic, not random. In a dimensionally-incorrect calculations, there will be random factors causing a randomly-varying final answer.
That’s a really smart trick! I’m sure there are some super advanced cases where the units might cancel out wrongly, but in practice they shouldn’t, and this let’s you interface with all the random software that exists! (Modulo the run it twice, as you said, because the two runs correspond to two different drawings of the constants)
Yeah a case where this came up for me is angles (radians, degrees, steradians, etc.). If you treat radians as a “unit” subjected to dimensional analysis, you wind up needing to manually insert and remove the radian unit in a bunch of places, which is somewhat confusing and annoying.
Another interesting thing with radiants is that when you write a literal expression, it will look quite different than in degrees (involving many more instances of π), so inspection can fix many errors without paying the full price of different types.
Units / dimensional analysis in physics is really a kind of type system. I was very big into using that for error checking when I used to do physics and engineering calculations professionally. (Helps with self-documenting too.) I invented my own weird way to do it that would allow them to be used in places where actual proper types & type-checking systems weren’t supported—like most numerical calculation packages, or C, or Microsoft Excel, etc.
Yeah a case where this came up for me is angles (radians, degrees, steradians, etc.). If you treat radians as a “unit” subjected to dimensional analysis, you wind up needing to manually insert and remove the radian unit in a bunch of places, which is somewhat confusing and annoying. Sometimes I found it was a good tradeoff, other times not—I tended to treat angles as proper type-checked units only for telescope and camera design calculations, but not in other contexts like accelerometers or other things where angles were only incidentally involved.
Definitely!
Dimensional analysis was the first place this analogy jumped to me when reading Fly By Night Physics, because it truly used dimensions not only to check results, but also to infer the general shape of the answer (which is also something you can do in type systems, for example a function with a generic type a→a can only be populated by the identity function, because it cannot not do anything else than return its input).
Although in physics you need more tricks and feels to do it correctly. Like the derivation of the law of the pendulum just from dimensional analysis requires you to have the understanding of forces as accelerations to know that you can us g here.
Dimensions are also a perennial candidate for things that should be added to type systems, with people working quite hard at implementing it (just found this survey from 2018).
I looked at the repo, and was quite confused how you did it, until I read
That’s a really smart trick! I’m sure there are some super advanced cases where the units might cancel out wrongly, but in practice they shouldn’t, and this let’s you interface with all the random software that exists! (Modulo the run it twice, as you said, because the two runs correspond to two different drawings of the constants)
Another interesting thing with radiants is that when you write a literal expression, it will look quite different than in degrees (involving many more instances of π), so inspection can fix many errors without paying the full price of different types.
my package “is of somewhat limited use … semantic consistency is detected in a rather obscure way”, haters gonna hate 😂
Oh, I didn’t see it actually mentioned your package. 😂