Hacker News Reader

Comment by simiones | Hacker News Reader

This is precisely why (programming language) types are poor model of physics units, despite often being touted for this exact use case. 3m is not the same thing as "the value 3 of type meter". It is the multiplication of the dimensionless scalar 3 with the special "m" constant for meters.

That's why pow(3m, 2) = 9 m^2, and not `the value 9 of type meter`. Of course, you can define the type `square meter` as well, and define `pow -> meters -> positive integer -> square meters`. However this quickly becomes overwhelming once you start doing more complex expressions with multiple types. What is the type of `pow (3kg^2 * m/s, 3/2)`?

Edit to add: also, there is a simple fact that "sin(pi/2 kg)" is just not defined, in programming or math or physics or any other useful system. It's definitely not 1kg, just like sin ( (pi/2) * 2) is not sin (pi/2) * sin (2).

View on HN

> with the special "m" constant for meters.

Isn't the "special constant" exactly "value 1, type meters", defined as equal to "value <...very large number...> type atoms" etc?

If not, then what would be the result of the multiplication of 3 with "m"?

> Of course, you can define the type `square meter` as well, and define `pow -> meters -> positive integer -> square meters`

As long as your power is an integer, you can reduce it to multiplication. So what you'd really want to define is the result of "<value1 of type meter> * <value2 of type meter>", "(<value1 of type meter> * <value2 of type meter>) * <value3 of type meter>" etc.

What this gets you in the end is a type algebra, but that is also not exactly a new concept.

> If not, then what would be the result of the multiplication of 3 with "m"?

The answer is not, and the result of 3 multiplied by m is 3m. Just like 3 multiplied by pi is 3pi; or, perhaps more accurately, you can view m as a kind of vector unit, and 3m as the scalar product. Of course, none of this is exactly matching - dimensions are different from irrationals, vectors, complex numbers, etc, they are mostly a thing of their own.

> What this gets you in the end is a type algebra, but that is also not exactly a new concept.

Sure, that's why I said specifically programming language types. I am aware that type theory has way more complex operations on types. I think some of these may even be expressible in Idris or Haskell + some appropriate extension. But in almost all programming languages, even ones like OCaml, SML, plain Haskell, Rust, C++ with template magic, Scala, F# and what have you, there is no way to specify that the result of multiplying two values of type A is of type "A * A", especially not in a way that then allows you specify that the division of a value of type "A * A" by A has type A. So types as exposed in any of the common programming languages are horrible for modelling dimensions as used in even high school physics.

> dimensions are different from irrationals, vectors, complex numbers, etc, they are mostly a thing of their own.

I harbor a terrible internal mental model of dimensions which I have never really validated or explored fully, where I like to think they might be vector exponents, or something vaguely similar. If we assign each dimension to be a dimension of a vector - (length, mass, time, etc…) then a ‘distance’ might be e^((1,0,0,…)); a ‘duration’ e^((0,0,1,…)).

These have the requisite properties that when we multiply and divide them, we end up adding and subtracting these vectors.

So a distance times a distance is e^((2,0,0,…)) and a distance over a duration (a speed) is e^((1,0,-1,…))

They have the right basic algebraic behavior but who knows what terrible consequences they would have.

Reply on news.ycombinator.com