> You generally can’t apply functions to dimensional units.
Perhaps not in mathematics, but in programming that's clearly possible. I guess programming is more general than mathematics.
Perhaps not in mathematics, but in programming that's clearly possible. I guess programming is more general than mathematics.
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).
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.
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.
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.