5 ms·

I once attended a meeting where a Professor from a University somewhere in Chicago gave a brilliant demonstration of using a similar type system for dealing wit

I once attended a meeting where a Professor from a University somewhere in Chicago gave a brilliant demonstration of using a similar type system for dealing with values in Electrical Engineering. It made quite sure you couldn't do things like add volts and amps. [Edit] it also handled things like parallel resistances, etc. It was in C++ if I recall correctly. This is a great idea, that I've haven't had cause to use yet.

masklinn 4y ago
FWIW that's a pretty basic application called "units of measure". Some languages like F# have that natively.
- mrkeen 4y ago
  I wish static typing were as uncontentious as units of measure.
  - masklinn 4y ago
    I wouldn't say that UOM are uncontentious, things can get dicey around reference units and precision for instance, or the combinatorial explosion of composite units.
    - mrkeen 4y ago
      Right, but if you told your professor you sometimes represent distance in Volts (to make your calculations simpler) you'd get some funny looks. You could even double-down on it: "Have there been any studies that prove that using units of measure helps you get the right answer?"
      - tsimionescu 4y ago
        Funnily enough, there are some applications for converting mechanics problems to analogous electricity problems to leverage circuit simulation software such as PSPICE to help solve things like transcendental equations.
        hither_shores 4y ago
        Yes, but the mapping doesn't change the relationship between the units of measure, which is the actual meaning as far as the type system is concerned. It's just a change of names.
        tsimionescu 4y ago
        Sure, I wasn't meaning to detract from the comment above, just to point out what I thought was an interesting related fact.
mdm12 4y ago
Unit of measures are a great example of what a type system can do, and something not enough languages support. F#[1] and Scala[2] are two that I know of that do support UOMs. Like you, I haven't had the need to use them in the domains I work in, but I imagine that they would be invaluable in certain contexts. [1] https://learn.microsoft.com/en-us/dotnet/fsharp/language-reference/units-of-measure https://learn.microsoft.com/en-us/dotnet/fsharp/language-ref... [2] https://github.com/typelevel/squants https://github.com/typelevel/squants
- leephillips 4y ago
  Julia has this via a package: Measurements.jl.
- docandrew 4y ago
  Packages exist for Ada, too: http://archive.adaic.com/tools/CKWG/Dimension/Physical_units_with_GNAT_GPL_2013-AUJ35.1.pdf http://archive.adaic.com/tools/CKWG/Dimension/Physical_units...
- throwawaymaths 4y ago
  It's also something that some languages seriously screw up. Consider multiplying a time (which is typed in go) with a numerical value... suppose what I want is a user to input number of time intervals to wait. So the user wants 5, and the interval is 2500 milliseconds. The way you get 12500 milliseconds out of that made me want to throw my computer out the window.
  - Chinjut 4y ago
    I don't understand. What should you get instead?
    - morelisp 4y ago
      Go does not have operator overloading, and numeric operators must have identical types. So if you have `var x int = 5` and `var t time.Duration = 2500 * time.Millisecond`, you have to `time.Duration(x) * t` or `time.Duration(x * int(t))`. It's slightly better than languages with no operator overloading nor newtypes at all (well, actually a lot better given other things you can use newtypes for) but without operator overloading using it just for units, with no other API machinery, is usually a bad idea.
photochemsyn 4y ago
This approach to typing could have saved the Mars Climate Orbiter, i.e a pounds of force type vs. a newtons type. > "A NASA review board found that the problem was in the software controlling the orbiter's thrusters. The software calculated the force the thrusters needed to exert in pounds of force. A separate piece of software took in the data assuming it was in the metric unit: newtons.... Propulsion engineers, like those at Lockheed Martin who built the craft, typically express force in pounds, but it was standard practice to convert to newtons for space missions. One pound of force is about 4.45 newtons. Engineers at NASA's Jet Propulsion Lab assumed the conversion had been made, and didn't check." https://www.wired.com/2010/11/1110mars-climate-observer-report/ https://www.wired.com/2010/11/1110mars-climate-observer-repo... There could be issues with memory use, but it could also be implemented as an API, i.e. ensuring values exported from one software package to another were of the correct type, but then store them internally as simple types... Switching everything to a unified metric system would make more sense in the long run, however.
- est 4y ago
  More like an i18n or l10n issue than types.
  - morelisp 4y ago
    I think you've inadvertently stumbled on another great example, distinct types for TranslatedMessage, LocalizedNumber, etc. from ordinary string has been a cornerstone of localization enforcement on at least two large applications I've worked on.
wirthjason 4y ago
I’m not sure the Chicago reference but if you’re talking about C++ the Units library is a good option. https://github.com/mpusz/units https://github.com/mpusz/units
hgomersall 4y ago
It's possible to go even further than just protecting against the wrong unit in the wrong place. You can generalise units: https://docs.rs/dimensioned/latest/dimensioned/ https://docs.rs/dimensioned/latest/dimensioned/ (Edit, that's not possible in c++)
- jdrek1 4y ago
  > (Edit, that's not possible in c++) Mind expanding on that? Because what that readme there shows is absolutely possible in C++, I have used a similar system for dealing with natural units.
  - hgomersall 4y ago
    I'm happy to admit I'm wrong on that. My understanding is the bit that makes (kg.m)/s^2 type equivalent to a N, equivalent to J/m is not implementable in the same generic way.
    - pencilguin 4y ago
      All unit systems decompose each unit to primitives, that can then be aliased for notational convenience. So, a result of J/m decomposes the same as a N.
tsimionescu 4y ago
Note that most such solutions break (or become much much much more complex) if you want anything more than simple arithmetic from them. For example, matrix multiplication with typed values (where each element of the matrix can have a different type/unit of measure) is extremely ugly code, and basically no such library supports it - even for matrices of fixed size (say, code that could multiply 3x3 matrices with 9 type parameters - which is not unrealistic in physical simulations). This is a fundamental limitation of types - they tend to scale poorly to very complex non-uniform structures. That's not to say that they shouldn't be used when they do scale nicely, though!
- tremon 4y ago
  matrix multiplication with typed values (where each element of the matrix can have a different type/unit of measure) Is this really a common occurrence? In most situations I've come across, it's the matrix itself (rows/columns) that has a unit of measurement, not the invididual columns. Tensors, rotation matrices, lighting maps: they all use the same units of measurement.
  - tsimionescu 4y ago
    Matrix multiplication is often used for solving systems of linear equations, and you often have systems of linear equations involving different physical quantities (such as position, speed, time and mass if solving some classical mechanics equations, or pressure, volume, temperature, and time for thermodynamics etc). And while it may be relatively common to start out and end up with matrices that have a single unit for each row (but different units on different rows), intermediate results will often end up with different combinations of units in each element.

masklinn 4y ago

FWIW that's a pretty basic application called "units of measure". Some languages like F# have that natively.

mrkeen 4y ago
I wish static typing were as uncontentious as units of measure.
- masklinn 4y ago
  I wouldn't say that UOM are uncontentious, things can get dicey around reference units and precision for instance, or the combinatorial explosion of composite units.
  - mrkeen 4y ago
    Right, but if you told your professor you sometimes represent distance in Volts (to make your calculations simpler) you'd get some funny looks. You could even double-down on it: "Have there been any studies that prove that using units of measure helps you get the right answer?"
    - tsimionescu 4y ago
      Funnily enough, there are some applications for converting mechanics problems to analogous electricity problems to leverage circuit simulation software such as PSPICE to help solve things like transcendental equations.
      - hither_shores 4y ago
        Yes, but the mapping doesn't change the relationship between the units of measure, which is the actual meaning as far as the type system is concerned. It's just a change of names.
        tsimionescu 4y ago
        Sure, I wasn't meaning to detract from the comment above, just to point out what I thought was an interesting related fact.

mdm12 4y ago

Unit of measures are a great example of what a type system can do, and something not enough languages support. F#[1] and Scala[2] are two that I know of that do support UOMs. Like you, I haven't had the need to use them in the domains I work in, but I imagine that they would be invaluable in certain contexts. [1] https://learn.microsoft.com/en-us/dotnet/fsharp/language-reference/units-of-measure https://learn.microsoft.com/en-us/dotnet/fsharp/language-ref... [2] https://github.com/typelevel/squants https://github.com/typelevel/squants

leephillips 4y ago
Julia has this via a package: Measurements.jl.
docandrew 4y ago
Packages exist for Ada, too: http://archive.adaic.com/tools/CKWG/Dimension/Physical_units_with_GNAT_GPL_2013-AUJ35.1.pdf http://archive.adaic.com/tools/CKWG/Dimension/Physical_units...
throwawaymaths 4y ago
It's also something that some languages seriously screw up. Consider multiplying a time (which is typed in go) with a numerical value... suppose what I want is a user to input number of time intervals to wait. So the user wants 5, and the interval is 2500 milliseconds. The way you get 12500 milliseconds out of that made me want to throw my computer out the window.
- Chinjut 4y ago
  I don't understand. What should you get instead?
  - morelisp 4y ago
    Go does not have operator overloading, and numeric operators must have identical types. So if you have `var x int = 5` and `var t time.Duration = 2500 * time.Millisecond`, you have to `time.Duration(x) * t` or `time.Duration(x * int(t))`. It's slightly better than languages with no operator overloading nor newtypes at all (well, actually a lot better given other things you can use newtypes for) but without operator overloading using it just for units, with no other API machinery, is usually a bad idea.

photochemsyn 4y ago

This approach to typing could have saved the Mars Climate Orbiter, i.e a pounds of force type vs. a newtons type. > "A NASA review board found that the problem was in the software controlling the orbiter's thrusters. The software calculated the force the thrusters needed to exert in pounds of force. A separate piece of software took in the data assuming it was in the metric unit: newtons.... Propulsion engineers, like those at Lockheed Martin who built the craft, typically express force in pounds, but it was standard practice to convert to newtons for space missions. One pound of force is about 4.45 newtons. Engineers at NASA's Jet Propulsion Lab assumed the conversion had been made, and didn't check." https://www.wired.com/2010/11/1110mars-climate-observer-report/ https://www.wired.com/2010/11/1110mars-climate-observer-repo... There could be issues with memory use, but it could also be implemented as an API, i.e. ensuring values exported from one software package to another were of the correct type, but then store them internally as simple types... Switching everything to a unified metric system would make more sense in the long run, however.

est 4y ago
More like an i18n or l10n issue than types.
- morelisp 4y ago
  I think you've inadvertently stumbled on another great example, distinct types for TranslatedMessage, LocalizedNumber, etc. from ordinary string has been a cornerstone of localization enforcement on at least two large applications I've worked on.

wirthjason 4y ago

I’m not sure the Chicago reference but if you’re talking about C++ the Units library is a good option. https://github.com/mpusz/units https://github.com/mpusz/units

hgomersall 4y ago

It's possible to go even further than just protecting against the wrong unit in the wrong place. You can generalise units: https://docs.rs/dimensioned/latest/dimensioned/ https://docs.rs/dimensioned/latest/dimensioned/ (Edit, that's not possible in c++)

jdrek1 4y ago
> (Edit, that's not possible in c++) Mind expanding on that? Because what that readme there shows is absolutely possible in C++, I have used a similar system for dealing with natural units.
- hgomersall 4y ago
  I'm happy to admit I'm wrong on that. My understanding is the bit that makes (kg.m)/s^2 type equivalent to a N, equivalent to J/m is not implementable in the same generic way.
  - pencilguin 4y ago
    All unit systems decompose each unit to primitives, that can then be aliased for notational convenience. So, a result of J/m decomposes the same as a N.

tsimionescu 4y ago

Note that most such solutions break (or become much much much more complex) if you want anything more than simple arithmetic from them. For example, matrix multiplication with typed values (where each element of the matrix can have a different type/unit of measure) is extremely ugly code, and basically no such library supports it - even for matrices of fixed size (say, code that could multiply 3x3 matrices with 9 type parameters - which is not unrealistic in physical simulations). This is a fundamental limitation of types - they tend to scale poorly to very complex non-uniform structures. That's not to say that they shouldn't be used when they do scale nicely, though!

tremon 4y ago
matrix multiplication with typed values (where each element of the matrix can have a different type/unit of measure) Is this really a common occurrence? In most situations I've come across, it's the matrix itself (rows/columns) that has a unit of measurement, not the invididual columns. Tensors, rotation matrices, lighting maps: they all use the same units of measurement.
- tsimionescu 4y ago
  Matrix multiplication is often used for solving systems of linear equations, and you often have systems of linear equations involving different physical quantities (such as position, speed, time and mass if solving some classical mechanics equations, or pressure, volume, temperature, and time for thermodynamics etc). And while it may be relatively common to start out and end up with matrices that have a single unit for each row (but different units on different rows), intermediate results will often end up with different combinations of units in each element.