4 ms·

How would a basic type system protect against incorrectly interpreting an imperial floating point value as a metric floating point value? That seems like an esp

How would a basic type system protect against incorrectly interpreting an imperial floating point value as a metric floating point value? That seems like an especially weak example, and fundamentally falls under the realm of logical fault endemic of every possible programming language. There are legitimate gripes about C/C++, especially in a space with hostile actors an unknown inputs, but that example was particularly weak.

joshmarlow 10y ago
> How would a basic type system protect against incorrectly interpreting an imperial floating point value as a metric floating point value? You could wrap your value in a typed data structure: enum LengthUnit { Feet(f64), Meters(f64), } And provide conversion functions between them, then only operate on one type, `LengthUnit::Meters` and throw errors if `LengthUnit::Feet` is passed in. I'm using Rust syntax here because it's fresher on my mind, but you could do the same with Haskell, OCaml, F#, etc. IIRC, OCaml would optimize away the outer structure so you wouldn't have much/if any performance hit. Presumably compilers for the other languages could/would do the same. EDIT: for formatting and clarity.
marvy 10y ago
> How would a type system protect against unit confusion? That this is a mistake that is possible to make in any language, but nevertheless this is also a problem that could be caught by a sufficiently good type system, if it was put to sufficiently good use. In fact, part of the justification for allowing user defined literals in C++ was precisely to make it easy and convenient to avoid mistakes like the Mars Climate Orbiter. Bjarne Stroustrup himself used that as an example in at least one talk he gave about C++11.
cwzwarich 10y ago
Andrew Kennedy's PhD thesis was about extending Hindley-Milner type inference to support units of measure. It basically boils down to extending unification to support equations over free abelian groups, which had been solved earlier in an abstract context. The approach could be integrated into just about any HM-derived language, and is shipping as part of F#.
- dwenzek 10y ago
  Thanks! I was aware of the feature but not of its author. https://blogs.msdn.microsoft.com/andrewkennedy/ https://blogs.msdn.microsoft.com/andrewkennedy/ https://channel9.msdn.com/Blogs/Charles/Andrew-Kennedy-F-Units-of-Measure https://channel9.msdn.com/Blogs/Charles/Andrew-Kennedy-F-Uni...
dualogy 10y ago
> How would a basic type system protect against incorrectly interpreting an imperial floating point value as a metric floating point value "Better" / richer / more refined (aiming/aspiring at least!) type systems than C/++/Java/C#/Go/etc aim to make it ever-more "powerfully convenient, effortless, and free-of-cost to denote eg. such different units as uniquely distinct (yet 'compatible' when explicit conversion is finally expressly (and visibly (and searchably)) called for) types" that all source code cannot possibly mismatch accidentally without the compiler catching it --- however the issue remains that we don't, and possibly can't have type systems that also enforce such styles (rather than just relying on a developer's/team's own discipline & resolve to adhere to such convention even in the face of deadlines & budget/schedule pressures) unless we actually totally forbid primitives like lone (semantics ambiguous) ints, lone (likewise) floats etc. Similar to "bool blindness", there's the general issue of "primitive/scalar-type blindness" always lingering. Probably some PhD candidate will write a Haskell extension for such a scenario some day soon. Though of course the next thing the deadline-driven developer will do is construct a single "semantic" int type used for all different semantic sorts kinds and types of "ints"......
- gpderetta 10y ago
  For what is worth, C++ type system (which is more powerful than most, actually) make it simple to encode units (including composite units, exponents and ratios) and computing the exact units of complex expressions. See Boost.Units or std::chrono design. And with zero cost abstraction and little syntactic overhead of course.
  - pjmlp 10y ago
    The problem is getting embedded devs to use it, or when they do use it, not to write "C with C++ compiler" code.
    - gpderetta 10y ago
      of course, but it would be even harder to get them to use any other language other than C or C++.
spc476 10y ago
A simple example would be instead of this: int temperature_a; int temperature_b; or even: Temperature a; Temperature b; you would have: Celsius a; Fahrenheit b; And an assignment between a and b would be an error, as Celcius and Fahrenheit are different types. Going along this path then, if you can extend the type system enough: Yards width; Yards length; Acre size = width * length; /* this would be okay */ Yards width; Yards length; Yards height; Acre money_bin = width * length * height; /* error */ /* as acre is a measure of area, not volume */ Think of the type of calculations that the Unix command 'units' does, but built into a language instead of an application.
- dkersten 10y ago
  The Frink[1] language has units like this built in. Its pretty cool what you can do with it. I definitely agree that doing that or, at least, something like your code samples, is a good bug-avoidance idea. [1] https://frinklang.org/ https://frinklang.org/

joshmarlow 10y ago

> How would a basic type system protect against incorrectly interpreting an imperial floating point value as a metric floating point value? You could wrap your value in a typed data structure: enum LengthUnit { Feet(f64), Meters(f64), } And provide conversion functions between them, then only operate on one type, `LengthUnit::Meters` and throw errors if `LengthUnit::Feet` is passed in. I'm using Rust syntax here because it's fresher on my mind, but you could do the same with Haskell, OCaml, F#, etc. IIRC, OCaml would optimize away the outer structure so you wouldn't have much/if any performance hit. Presumably compilers for the other languages could/would do the same. EDIT: for formatting and clarity.

marvy 10y ago

> How would a type system protect against unit confusion? That this is a mistake that is possible to make in any language, but nevertheless this is also a problem that could be caught by a sufficiently good type system, if it was put to sufficiently good use. In fact, part of the justification for allowing user defined literals in C++ was precisely to make it easy and convenient to avoid mistakes like the Mars Climate Orbiter. Bjarne Stroustrup himself used that as an example in at least one talk he gave about C++11.

cwzwarich 10y ago

Andrew Kennedy's PhD thesis was about extending Hindley-Milner type inference to support units of measure. It basically boils down to extending unification to support equations over free abelian groups, which had been solved earlier in an abstract context. The approach could be integrated into just about any HM-derived language, and is shipping as part of F#.

dwenzek 10y ago
Thanks! I was aware of the feature but not of its author. https://blogs.msdn.microsoft.com/andrewkennedy/ https://blogs.msdn.microsoft.com/andrewkennedy/ https://channel9.msdn.com/Blogs/Charles/Andrew-Kennedy-F-Units-of-Measure https://channel9.msdn.com/Blogs/Charles/Andrew-Kennedy-F-Uni...

dualogy 10y ago

> How would a basic type system protect against incorrectly interpreting an imperial floating point value as a metric floating point value "Better" / richer / more refined (aiming/aspiring at least!) type systems than C/++/Java/C#/Go/etc aim to make it ever-more "powerfully convenient, effortless, and free-of-cost to denote eg. such different units as uniquely distinct (yet 'compatible' when explicit conversion is finally expressly (and visibly (and searchably)) called for) types" that all source code cannot possibly mismatch accidentally without the compiler catching it --- however the issue remains that we don't, and possibly can't have type systems that also enforce such styles (rather than just relying on a developer's/team's own discipline & resolve to adhere to such convention even in the face of deadlines & budget/schedule pressures) unless we actually totally forbid primitives like lone (semantics ambiguous) ints, lone (likewise) floats etc. Similar to "bool blindness", there's the general issue of "primitive/scalar-type blindness" always lingering. Probably some PhD candidate will write a Haskell extension for such a scenario some day soon. Though of course the next thing the deadline-driven developer will do is construct a single "semantic" int type used for all different semantic sorts kinds and types of "ints"......

gpderetta 10y ago
For what is worth, C++ type system (which is more powerful than most, actually) make it simple to encode units (including composite units, exponents and ratios) and computing the exact units of complex expressions. See Boost.Units or std::chrono design. And with zero cost abstraction and little syntactic overhead of course.
- pjmlp 10y ago
  The problem is getting embedded devs to use it, or when they do use it, not to write "C with C++ compiler" code.
  - gpderetta 10y ago
    of course, but it would be even harder to get them to use any other language other than C or C++.

spc476 10y ago

A simple example would be instead of this: int temperature_a; int temperature_b; or even: Temperature a; Temperature b; you would have: Celsius a; Fahrenheit b; And an assignment between a and b would be an error, as Celcius and Fahrenheit are different types. Going along this path then, if you can extend the type system enough: Yards width; Yards length; Acre size = width * length; /* this would be okay */ Yards width; Yards length; Yards height; Acre money_bin = width * length * height; /* error */ /* as acre is a measure of area, not volume */ Think of the type of calculations that the Unix command 'units' does, but built into a language instead of an application.

dkersten 10y ago
The Frink[1] language has units like this built in. Its pretty cool what you can do with it. I definitely agree that doing that or, at least, something like your code samples, is a good bug-avoidance idea. [1] https://frinklang.org/ https://frinklang.org/