3 ms·

> 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 c

> 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.
- kelnos 5y ago
  > "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. Yes. "Probably", as you said. "Probably" is much, much weaker than "formally verified".
- klodolph 5y ago
  > Touchy! 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.

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.

kelnos 5y ago
> "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. Yes. "Probably", as you said. "Probably" is much, much weaker than "formally verified".
klodolph 5y ago
> Touchy! 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.