5 ms·

> But as both datums were stored as floating point numbers, which they always would be, in any reasonable implementation, static typing wouldn't have caught an

by nyssos 3y ago

> But as both datums were stored as floating point numbers, which they always would be, in any reasonable implementation, static typing wouldn't have caught anything. Types are not runtime representations, and any good nominal type system will allow you to avoid this sort of problem easily. For example, this Haskell code newtype Inches = Inches Double deriving Num newtype Centimeters = Centimeters Double deriving Num a :: Centimeters a = Centimeters 1.0 b :: Inches b = Inches 1.0 fine = a + a alsoFine = b + b mistake = a + b will give this type error Couldn't match expected type ‘Centimeters’ with actual type ‘Inches’ In the second argument of ‘(+)’, namely ‘b’ In the expression: a + b In an equation for ‘mistake’: mistake = a + b but both `a` and `b` will be doubles at runtime.

bjourne 3y ago
That is why I wrote "in any reasonable implementation". Embedding physical quantities in the type system is possible in many language but is not practical. Hence why safety-critical software doesn't contain declarations like yours. For example, what is the type of Inch * Inch? What is the type of Inch / Inch? Sure, perhaps if NASA and their subcontractors had used a common well-developed physical quantities library then the bug could have been caught during compile-time. But I think it is a moot point since most people don't use such libraries.
- esafak 3y ago
  > For example, what is the type of Inch * Inch? An area, inch^2. > What is the type of Inch / Inch? A unitless ratio? I don't understand why this is not practical in safety-critical software. nyssos demonstrated what I believe is the right way to do it.
  - bjourne 3y ago
    These semantics make the type incompatible with the Num class and attempting to plug your type into, say, a run of the mill ode solver likely won't do what you want. So you have two options. 1) Rewrite all code to become "quantity aware". Multiplying two Matrix[Inch] results in a Matrix[Inch2] and so on. 2) Litter your code with floatToInch and inchToFloat conversions. I think you can see why both options suck? If you really can't, then perhaps try finding some safety-critical software that relies on "physical quantity types" in some form or another?
    - deleted 3y ago
      [deleted]
    - freilanzer 3y ago
      > I think you can see why both options suck? Do they suck more than losing spacecraft?
      - bjourne 3y ago
        Absolutely. Littering a code base with centimeter-to-inch conversions or rewriting every numeric computation to become unit aware would for sure have caused more bugs than it would have prevented.
- gpderetta 3y ago
  It is possible and practical. For example the <chrono> in the C++ standard library.
  - fauigerzigerk 3y ago
    Very true, it is possible and practical, and chrono is a good example. But you can take a similar approach in dynamically typed languages as well. It wouldn't be hard to design a library that did something like this: some_duration = minutes(3) + seconds(2) Of course that doesn't change the fact that any function receiving a duration would only raise type errors at runtime. For instance, someone could try to pass the number of seconds as an integer rather than as a duration: remind_me_after(182) But any semantic testing would automatically catch type errors as well. remind_me_after would fail every single time assuming the implementation would be something like this: def remind_me_after(duration): reminder_api.set_reminder(now().as_seconds() + duration.as_seconds()) I think this is the reason why studies don't show huge differences in defects between dynamically and statically typed languages. You have to do semantic tests anyway, and they would cover most* type errors as well. What would it mean for code to be semantically correct while containing type errors? It would probably mean that the code is not in fact semantically correct because some semantic edge cases are not covered by the tests. * Not all of them because semantic tests could theoretically succeed by accident for some specific values that have incorrect types.
    - nyssos 3y ago
      > What would it mean for code to be semantically correct while containing type errors? It would probably mean that the code is not in fact semantically correct because some semantic edge cases are not covered by the tests. It can also mean that the code has incorrect subprograms, but that the program as a whole is protected from them by some hard to analyze condition. As an extreme example, one of these two programs "works": if goldbachConjectureCounterexampleExists() then print("Hello world!") else launchMissiles() if goldbachConjectureCounterexampleDoesNotExist() then print("Hello world!") else launchMissiles() but I don't know which and neither does the compiler. Rejecting them is a feature, not a bug.

by nyssos 3y ago

bjourne 3y ago

That is why I wrote "in any reasonable implementation". Embedding physical quantities in the type system is possible in many language but is not practical. Hence why safety-critical software doesn't contain declarations like yours. For example, what is the type of Inch * Inch? What is the type of Inch / Inch? Sure, perhaps if NASA and their subcontractors had used a common well-developed physical quantities library then the bug could have been caught during compile-time. But I think it is a moot point since most people don't use such libraries.

esafak 3y ago
> For example, what is the type of Inch * Inch? An area, inch^2. > What is the type of Inch / Inch? A unitless ratio? I don't understand why this is not practical in safety-critical software. nyssos demonstrated what I believe is the right way to do it.
- bjourne 3y ago
  These semantics make the type incompatible with the Num class and attempting to plug your type into, say, a run of the mill ode solver likely won't do what you want. So you have two options. 1) Rewrite all code to become "quantity aware". Multiplying two Matrix[Inch] results in a Matrix[Inch2] and so on. 2) Litter your code with floatToInch and inchToFloat conversions. I think you can see why both options suck? If you really can't, then perhaps try finding some safety-critical software that relies on "physical quantity types" in some form or another?
  - deleted 3y ago
    [deleted]
  - freilanzer 3y ago
    > I think you can see why both options suck? Do they suck more than losing spacecraft?
    - bjourne 3y ago
      Absolutely. Littering a code base with centimeter-to-inch conversions or rewriting every numeric computation to become unit aware would for sure have caused more bugs than it would have prevented.
gpderetta 3y ago
It is possible and practical. For example the <chrono> in the C++ standard library.
- fauigerzigerk 3y ago
  Very true, it is possible and practical, and chrono is a good example. But you can take a similar approach in dynamically typed languages as well. It wouldn't be hard to design a library that did something like this: some_duration = minutes(3) + seconds(2) Of course that doesn't change the fact that any function receiving a duration would only raise type errors at runtime. For instance, someone could try to pass the number of seconds as an integer rather than as a duration: remind_me_after(182) But any semantic testing would automatically catch type errors as well. remind_me_after would fail every single time assuming the implementation would be something like this: def remind_me_after(duration): reminder_api.set_reminder(now().as_seconds() + duration.as_seconds()) I think this is the reason why studies don't show huge differences in defects between dynamically and statically typed languages. You have to do semantic tests anyway, and they would cover most* type errors as well. What would it mean for code to be semantically correct while containing type errors? It would probably mean that the code is not in fact semantically correct because some semantic edge cases are not covered by the tests. * Not all of them because semantic tests could theoretically succeed by accident for some specific values that have incorrect types.
  - nyssos 3y ago
    > What would it mean for code to be semantically correct while containing type errors? It would probably mean that the code is not in fact semantically correct because some semantic edge cases are not covered by the tests. It can also mean that the code has incorrect subprograms, but that the program as a whole is protected from them by some hard to analyze condition. As an extreme example, one of these two programs "works": if goldbachConjectureCounterexampleExists() then print("Hello world!") else launchMissiles() if goldbachConjectureCounterexampleDoesNotExist() then print("Hello world!") else launchMissiles() but I don't know which and neither does the compiler. Rejecting them is a feature, not a bug.