lecopivo
commented
1 year ago Yes that is definitely on the agenda. I already did some experimentation with physical units, have a look here . It keeps track of units and not only of dimensions. So you do not accidentally mix up metric system with imperial.
However, it is just an experiment. It is limited to mass, length and time. It is not easily extensible. Also it should play nicely with the rest of the code, for example if you differentiate trajectory of a particle then the derivative should have naturally dimensions of velocity.
It needs a lot more thought and experimentation, maybe get inspired by this project that has dimensional analysis. Also I feel that keeping track of only dimensions is not enough in practice. You really want to keep track of units as that is the biggest source of mistakes and frustration. Any thoughts on this?
This seems like a really cool project! I was wondering if you'd thought about adding a dimensions system, which would be a nice fit with Lean, since it requires somewhat dependent types.
For example, a quantity like momentum has dimensions $MLT^{-1}$ (mass, length, inverse time), so can only be added to another quantity with those dimensions, but can be multiplied by a quantity with any dimensions. One could translate this into a type system by having numbers like
n : (Dim (M 1) (L 1) (T (-1))with appropriate types for addition and multiplication.Keeping track of dimensions and ensuring that dimensional errors aren't made seems like a nice use-case of something like SciLean for physical problems like Hamiltonian mechanics.