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.
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.
> 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.
> 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.
> 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.
> 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.
Hey, I'm only human. You made some inane comments.
> 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 claim is trivially false... Go and Rust have explicit casts, and they're reasonably popular. For example, in Go,
var x int16
var y int32
x = y // ERROR!
x = int32(y) // ok
The same is true in Rust.
let x: i16 = 1;
let y: i32 = x; // ERROR!
let y = i32::from(x); // ok
let z = i16::from(y); // ERROR!
> 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.
This is clearly false in practice, just look at extant Go and Rust code.
> 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?
If that's a rhetorical question, just make your point.
The fromInteger function is an explicit conversion. The conversion is explicit, but the destination type isn't explicit. The source type isn't explicit either, but apparently that's okay... consider the C code:
int x = (int)y;
Would you call the cast "implicit" because you don't know the type of y just by looking at the code? No, it's still an explicit cast. Maybe a "super duper mega explicit" cast would look like this:
int x = (float->int)y;
Reminds me of Scheme. You would want super duper explicit conversions in dynamic languages, because neither the source nor destination type are annotated. You want the destination type annotated in traditional type systems because otherwise the compiler would not be able to figure out what you are doing. Haskell does not need the source or destination type annotated, this is ok.
> It is news to people who don't do numeric programming.
I'd say that it's blindingly obvious to people with a rudimentary understanding of programming.
> 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.
You can already -ftrapv if you like, but "trapping on overflow" is a contributing factor to the Ariane 5 disaster, and the lesson there is that trapping on overflow is not necessarily a safe default. The cost of runtime overflow checks is surprisingly large, too, which is why people so often turn it off in languages that support it out of the box (like C# and Ada). The mitigations for these problems will involve some combination of run-time checks, compile-time checks, and testing.
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.
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.
I think the bug here is arguably also an implicit cast, from int16 back to int32. Languages that don't allow implicit casts at won't compile that last line.
I think it’s less a problem with explicit casts and more a problem of insufficient expressivity. If what you wanted was “cast to the type of b”, then something along the lines of C++’s decltype would be better:
b = static_cast<decltype(b)>(a);
And as other commenters have pointed out, if implicit widening is disallowed that would also prevent the potential bug.
The problem with mandating this is that it doesn't really express anything - the semantics are the same as `b = a;`. And there's a cost because it's quite verbose.
If what you want to express is "I know b and a have different storage sizes", that could be useful, but it doesn't do that because eg if you typo `b` for `a`, then `b = static_cast<decltype(b)>(b);` is still accepted.
> The problem with mandating this is that it doesn't really express anything - the semantics are the same as `b = a;`. And there's a cost because it's quite verbose.
Sure, but at least the problem is back to "should conversions/casts be implicit or explicit?", rather than "I cannot do what I want with explicit casts".
> If what you want to express is "I know b and a have different storage sizes"
You may not even know this (e.g., in generic code), and if you did want to ensure different storage sizes specifically, then you want a (static) assert.
> eg if you typo `b` for `a`, then `b = static_cast<decltype(b)>(b);` is still accepted.
That would also apply to the version with implicit casts/conversions, wouldn't it?
If C lets you shoot yourself in the foot, it doesn't mean that you should do it! If you cast something then you need to take a moment to think about it first and check if it makes sense and whether it is really needed.
