5 ms·

Java isn't sound and the poor semantics of null are critical to proving it. Not that this takes away from your larger point exactly, but Java+null is no longer

by tel 9y ago

Java isn't sound and the poor semantics of null are critical to proving it. Not that this takes away from your larger point exactly, but Java+null is no longer a good example.

evmar 9y ago
As I was saying in the comment, Java is sound* by their definition of what soundness means, and it is exactly why it's a great example. You probably have some intuition about some desired property you have (like "doesn't crash/throw at runtime"), but that is a different property than soundness. You can certainly evaluate a type system against that property as well. But a type system that completely proves a program does not crash at runtime must be able to e.g. prove that it never runs out of memory, that recursive functions terminate, and the resulting allowable programs cannot do very much. * It turns out Java accidentally turned out to be unsound in a really obscure corner case, unrelated to the nulls thing. https://hackernoon.com/java-is-unsound-28c84cb2b3f https://hackernoon.com/java-is-unsound-28c84cb2b3f
- leshow 9y ago
  You seem to be including the halting problem in your definition of type soundness, those aren't the same things. Java has always had covariant arrays, which are not sound. Whether it was intentional or not is irrelevant to the question of 'does this language have a sound type system?'.
  - evmar 9y ago
    I agree that termination isn't part of soundness. I was trying to explain how null pointer exceptions are compatible with soundness in Java. As far as I understand it, Java covariant arrays are sound because the language is defined to throw before the unsound assignment happens. The link I had above claims as much. Maybe I have the definition wrong too?
    - leshow 9y ago
      Perhaps you're right there since the check is moved to runtime, I must have glossed over that. If you look at one of the sibling comments though, it's a bit of a moot point. There's a paper showing a number of unsound bits of code in Java and Scala that use nulls to do pernicious things like transmute types.
    - catnaroek 9y ago
      Type soundness is always relative to a kind of error that a type system is designed to rule out. So any type system can be made trivially sound by decreeing that its purpose is not to eliminate any kind of error. This is why “mathematically civilized” is a much better term. For example, even if you don't mind null pointer exceptions, it is not mathematically civilized to add one extra case to everyone's case analyses.
- tel 9y ago
  That's exactly the unsoundness proof I was talking about and it is indeed caused by a bad interaction between generics, existentials, and null.
  - evmar 9y ago
    I see. Sorry for misunderstanding your comment.

by tel 9y ago

Java isn't sound and the poor semantics of null are critical to proving it. Not that this takes away from your larger point exactly, but Java+null is no longer a good example.

evmar 9y ago

As I was saying in the comment, Java is sound* by their definition of what soundness means, and it is exactly why it's a great example. You probably have some intuition about some desired property you have (like "doesn't crash/throw at runtime"), but that is a different property than soundness. You can certainly evaluate a type system against that property as well. But a type system that completely proves a program does not crash at runtime must be able to e.g. prove that it never runs out of memory, that recursive functions terminate, and the resulting allowable programs cannot do very much. * It turns out Java accidentally turned out to be unsound in a really obscure corner case, unrelated to the nulls thing. https://hackernoon.com/java-is-unsound-28c84cb2b3f https://hackernoon.com/java-is-unsound-28c84cb2b3f

leshow 9y ago
You seem to be including the halting problem in your definition of type soundness, those aren't the same things. Java has always had covariant arrays, which are not sound. Whether it was intentional or not is irrelevant to the question of 'does this language have a sound type system?'.
- evmar 9y ago
  I agree that termination isn't part of soundness. I was trying to explain how null pointer exceptions are compatible with soundness in Java. As far as I understand it, Java covariant arrays are sound because the language is defined to throw before the unsound assignment happens. The link I had above claims as much. Maybe I have the definition wrong too?
  - leshow 9y ago
    Perhaps you're right there since the check is moved to runtime, I must have glossed over that. If you look at one of the sibling comments though, it's a bit of a moot point. There's a paper showing a number of unsound bits of code in Java and Scala that use nulls to do pernicious things like transmute types.
  - catnaroek 9y ago
    Type soundness is always relative to a kind of error that a type system is designed to rule out. So any type system can be made trivially sound by decreeing that its purpose is not to eliminate any kind of error. This is why “mathematically civilized” is a much better term. For example, even if you don't mind null pointer exceptions, it is not mathematically civilized to add one extra case to everyone's case analyses.
tel 9y ago
That's exactly the unsoundness proof I was talking about and it is indeed caused by a bad interaction between generics, existentials, and null.
- evmar 9y ago
  I see. Sorry for misunderstanding your comment.