3 ms·

As far as I can tell, the correct way to handle units of measurement in a programming language is by extending unification to abelian groups, as in Andrew Kenne

As far as I can tell, the correct way to handle units of measurement in a programming language is by extending unification to abelian groups, as in Andrew Kennedy's work that was later implemented in F#: https://www.microsoft.com/en-us/research/publication/relational-parametricity-and-units-of-measure/ https://www.microsoft.com/en-us/research/publication/relatio... This seems superior to the GNAT solution. And support for dimensionality is somewhat orthogonal to the ergonomics of converting e.g. a u32 to a u64 that comes up in systems programming.

touisteur 4y ago
You're right that it is orthogonal to the size of the variable, but thinking in bounds, precision, and yes, types (that can carry many notions, including dimensionality) is more interesting, to me, than 'just' u32 to u64. In my experience, being prompted to think about what you actually mean and have a tool to express it and check it is a good way to write understandable and correct code.