3 ms·

But, that's a good example of why implicit casts are bad! b = (int16)a; This contains two casts... one explicit cast to int16, and one implicit cast bac

But, that's a good example of why implicit casts are bad! b = (int16)a; This contains two casts... one explicit cast to int16, and one implicit cast back to int32. In languages without implicit casts, this would be an error.

astrange 5y ago
Many languages "without implicit casts" e.g. Java still have this problem because they allow widening casts. I don't think it makes sense to ban them in a language with powerful enough checks, like dependent types. If you have two variables and one is typed "int 1-10" and the other is typed "int 1-5", and it fails at runtime if it doesn't fit in the destination range, why do you need to type something that says you really meant to assign one to the other? Just assign it.
- klodolph 5y ago
  > Many languages "without implicit casts" e.g. Java still have this problem because they allow widening casts. I'm reading this as, "Many red boxes are blue circles." If the language allows implicit widening casts, it has implicit casts. I don't think more powerful checks are necessary. It's just that the implicit conversions in C are a bit wild, and they result in unexpected behavior and surprise programmers, and from experience, making all casts explicit is not such a burden (except for stuff like char ptr -> const char ptr). I think the fantasy here is simple... as much as we want to explore new ways to make safe programs with better type systems and runtime checks, there is still some design space near C which is safer but not really more complicated.
  - ChrisSD 5y ago
    Tbh, I don't think you're the first person to think that but the trouble with making a "safer C" is that it's not C. Or to be more precise, it looks like C but isn't C compatible. This has ended up killing most attempts. Apparently nobody actually wants an almost-C language (alternatively, nobody has yet managed to successfully market one). There seems to be an uncanny valley effect with C-like languages. The best you can do is have non-standard compiler extensions on top of ISO C.
    - klodolph 5y ago
      No, this approach is more common and successful than you might think. We're not talking about making an entirely new language which is incompatible with C. You adopt a style guide, an accompanying static analysis tool, and maybe add some annotations to your source code. Your code is still C-compatible and you can still use the same compilers. Static analysis of general C programs is quite difficult, and turning on an analyzer for an existing codebase typically results in obscene numbers of false positives. However, if you pair a static analyzer with a strict style guide which restricts the language, you can make the static analyzer much more powerful and useful. This could be MISRA, it could be a formal verification system, or it could be something else entirely.
  - astrange 5y ago
    > I'm reading this as, "Many red boxes are blue circles." If the language allows implicit widening casts, it has implicit casts. The problem is that people state things like "Java doesn't have implicit casts for correctness." But then it does have implicit casts, so now is there still correctness? Another case is Haskell, where the wiki tells you: > Conversion between numerical types in Haskell must be done explicitly. This is unlike many traditional languages (such as C or Java) that automatically coerce between numerical types. But what this actually means is instead of `a = b` you do `a = fromInteger b`. This is obviously also an implicit cast, because Haskell has type inference. So again, you're not writing a proof that your conversion is correct. You're just writing a different, longer "yes I really mean to assign this" statement.
    - klodolph 5y ago
      > The problem is that people state things like "Java doesn't have implicit casts for correctness." But then it does have implicit casts, so now is there still correctness? I am a bit too tired to engage with this kind of outright insanity. If you have a problem with what "people state", but not specifically with what I state or what has been stated in this conversation, then go have arguments with "people". The idea that "Java has correctness" or "Java does not have correctness" does not make any sense. Java is a language, it's the programs that you write with it that are correct or incorrect. > This is obviously also an implicit cast, because Haskell has type inference. Incorrect, it is an explicit conversion. There is no such thing as a "cast" in Haskell, there are only functions which convert values of one type to values of another type. (well, in FFI code, there are functions which "cast" pointers and the like, but that's FFI.) And yes, you're not writing a proof that the conversion is correct. This is... blindingly obvious, so I have no idea what kind of point you are trying to make. "Ordinary Haskell code is not formally verified" is not news.
      - astrange 5y ago
        > I am a bit too tired to engage with this kind of outright insanity. If you have a problem with what "people state", but not specifically with what I state or what has been stated in this conversation, then go have arguments with "people". Touchy! I am claiming the people who want always explicit casts have not actually used a system where they're all explicit much (because like in Java, some are still implicit) and would find it annoying if they did. That could result in performance compromises, like using int arrays everywhere instead of smaller types. Which is fine for scalar values, but for arrays it wastes memory. > Java is a language, it's the programs that you write with it that are correct or incorrect. Surely this language feature is intended to promote correctness. What else are errors for? > Incorrect, it is an explicit conversion. But `a = (uint16_t)b` and `a = fromInteger b` aren't the same thing - in one you have to name the destination type and in the other you don't. One is more explicit than the other. Is one of them bad? > "Ordinary Haskell code is not formally verified" is not news. It is news to people who don't do numeric programming. "If it compiles it probably works" / "if it compiles it's probably correct" is a real thing said about the language said on this forum. C clearly has issues (the implicit unsigned short->int promotion is totally wrong) but I think trapping on overflows at runtime would be a much better improvement than adding compile errors.

astrange 5y ago

Many languages "without implicit casts" e.g. Java still have this problem because they allow widening casts. I don't think it makes sense to ban them in a language with powerful enough checks, like dependent types. If you have two variables and one is typed "int 1-10" and the other is typed "int 1-5", and it fails at runtime if it doesn't fit in the destination range, why do you need to type something that says you really meant to assign one to the other? Just assign it.

klodolph 5y ago
> Many languages "without implicit casts" e.g. Java still have this problem because they allow widening casts. I'm reading this as, "Many red boxes are blue circles." If the language allows implicit widening casts, it has implicit casts. I don't think more powerful checks are necessary. It's just that the implicit conversions in C are a bit wild, and they result in unexpected behavior and surprise programmers, and from experience, making all casts explicit is not such a burden (except for stuff like char ptr -> const char ptr). I think the fantasy here is simple... as much as we want to explore new ways to make safe programs with better type systems and runtime checks, there is still some design space near C which is safer but not really more complicated.
- ChrisSD 5y ago
  Tbh, I don't think you're the first person to think that but the trouble with making a "safer C" is that it's not C. Or to be more precise, it looks like C but isn't C compatible. This has ended up killing most attempts. Apparently nobody actually wants an almost-C language (alternatively, nobody has yet managed to successfully market one). There seems to be an uncanny valley effect with C-like languages. The best you can do is have non-standard compiler extensions on top of ISO C.
  - klodolph 5y ago
    No, this approach is more common and successful than you might think. We're not talking about making an entirely new language which is incompatible with C. You adopt a style guide, an accompanying static analysis tool, and maybe add some annotations to your source code. Your code is still C-compatible and you can still use the same compilers. Static analysis of general C programs is quite difficult, and turning on an analyzer for an existing codebase typically results in obscene numbers of false positives. However, if you pair a static analyzer with a strict style guide which restricts the language, you can make the static analyzer much more powerful and useful. This could be MISRA, it could be a formal verification system, or it could be something else entirely.
- astrange 5y ago
  > I'm reading this as, "Many red boxes are blue circles." If the language allows implicit widening casts, it has implicit casts. The problem is that people state things like "Java doesn't have implicit casts for correctness." But then it does have implicit casts, so now is there still correctness? Another case is Haskell, where the wiki tells you: > Conversion between numerical types in Haskell must be done explicitly. This is unlike many traditional languages (such as C or Java) that automatically coerce between numerical types. But what this actually means is instead of `a = b` you do `a = fromInteger b`. This is obviously also an implicit cast, because Haskell has type inference. So again, you're not writing a proof that your conversion is correct. You're just writing a different, longer "yes I really mean to assign this" statement.
  - klodolph 5y ago
    > The problem is that people state things like "Java doesn't have implicit casts for correctness." But then it does have implicit casts, so now is there still correctness? I am a bit too tired to engage with this kind of outright insanity. If you have a problem with what "people state", but not specifically with what I state or what has been stated in this conversation, then go have arguments with "people". The idea that "Java has correctness" or "Java does not have correctness" does not make any sense. Java is a language, it's the programs that you write with it that are correct or incorrect. > This is obviously also an implicit cast, because Haskell has type inference. Incorrect, it is an explicit conversion. There is no such thing as a "cast" in Haskell, there are only functions which convert values of one type to values of another type. (well, in FFI code, there are functions which "cast" pointers and the like, but that's FFI.) And yes, you're not writing a proof that the conversion is correct. This is... blindingly obvious, so I have no idea what kind of point you are trying to make. "Ordinary Haskell code is not formally verified" is not news.
    - astrange 5y ago
      > I am a bit too tired to engage with this kind of outright insanity. If you have a problem with what "people state", but not specifically with what I state or what has been stated in this conversation, then go have arguments with "people". Touchy! I am claiming the people who want always explicit casts have not actually used a system where they're all explicit much (because like in Java, some are still implicit) and would find it annoying if they did. That could result in performance compromises, like using int arrays everywhere instead of smaller types. Which is fine for scalar values, but for arrays it wastes memory. > Java is a language, it's the programs that you write with it that are correct or incorrect. Surely this language feature is intended to promote correctness. What else are errors for? > Incorrect, it is an explicit conversion. But `a = (uint16_t)b` and `a = fromInteger b` aren't the same thing - in one you have to name the destination type and in the other you don't. One is more explicit than the other. Is one of them bad? > "Ordinary Haskell code is not formally verified" is not news. It is news to people who don't do numeric programming. "If it compiles it probably works" / "if it compiles it's probably correct" is a real thing said about the language said on this forum. C clearly has issues (the implicit unsigned short->int promotion is totally wrong) but I think trapping on overflows at runtime would be a much better improvement than adding compile errors.