3 ms·

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 ar

• 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.