This was referenced in the post but if you’re looking for a packaged up implementation that does take advantage of some type family level stuff see Richard Eisenberg’s units library

This is really cool! One question: how would you handle cases where two different units have the same dimension? For example, both energy and torque are kg*(m/s)^2 (although torque is a vector and energy a scalar).

What do you mean by “handle” here? Even outside of any dimensional analysis software, there’s nothing that you can do to change that torque is dimensionally equivalent to energy.

(People are often quick to dismiss this equivalence as a coincidence, but it’s not; it’s deeply related to conservation laws and the algebraic structure of physics in ways that I don’t entirely understand.)

A rich enough type system can express the algebraic properties of different objects, which might help. For example, you could specify that torque quantities are bivectors or that they are in the Lie algebra of… well, something, or that they have a particular tensor structure. But all of those are separate from dimensional analysis, and I’ve never seen a tractable way of representing those kinds of properties in software. Not to say it doesn’t exist, I just haven’t seen it.

What do you mean by “handle” here? Even outside of any dimensional analysis software, there’s nothing that you can do to change that torque is dimensionally equivalent to energy.

By handle I mean make attempting to two different units with the same dimension a compiler error.

That’s the thing. Torque and energy are the same unit. They’re usually used differently, but they’re mathematically the same except for the way they’re usually embedded in tensors.

You could make angles dimensional, but that would be wrong for other reasons. Any system of coherent units necessarily treats torque and energy the same.

I feel this is closely related to fractional types, where 1/x is interpreted as a promise to receive some x. Then some type 1/x*y represents some computation that requires an x, produces an y. Clearly this post corresponds with that intuition.

This was referenced in the post but if you’re looking for a packaged up implementation that does take advantage of some type family level stuff see Richard Eisenberg’s units library

This is really cool! One question: how would you handle cases where two different units have the same dimension? For example, both energy and torque are kg*(m/s)^2 (although torque is a vector and energy a scalar).

What do you mean by “handle” here? Even outside of any dimensional analysis software, there’s nothing that you can do to change that torque is dimensionally equivalent to energy.

(People are often quick to dismiss this equivalence as a coincidence, but it’s not; it’s deeply related to conservation laws and the algebraic structure of physics in ways that I don’t entirely understand.)

A rich enough type system can express the algebraic properties of different objects, which might help. For example, you could specify that torque quantities are bivectors or that they are in the Lie algebra of… well, something, or that they have a particular tensor structure. But all of those are separate from dimensional analysis, and I’ve never seen a tractable way of representing those kinds of properties in software. Not to say it doesn’t exist, I just haven’t seen it.

By handle I mean make attempting to two different units with the same dimension a compiler error.

That’s the thing. Torque and energy are the same unit. They’re usually used differently, but they’re mathematically the same except for the way they’re usually embedded in tensors.

You could make angles dimensional, but that would be wrong for other reasons. Any system of coherent units necessarily treats torque and energy the same.

@stepchowfun did you come up with this ex-nihilo or are there other examples of this you can point to?

I feel this is closely related to fractional types, where 1/x is interpreted as a promise to receive some x. Then some type 1/x*y represents some computation that requires an x, produces an y. Clearly this post corresponds with that intuition.

See https://www.cs.indiana.edu/~sabry/papers/fractionals.pdf