> I think the right answer is a sound typed language.
What do you mean by a "sound typed language". Go and Java have unsound type systems, and run circles around JS and Dart. Considering your involvement with Dart, I find contradictory information [1].
I mean that if the type checker concludes than an expression or variable has type T, then no execution of the program will ever lead to a value not of type T being observed in that variable or expression.
In most languages today, this property it enforced with a combination of static and runtime checks. Mostly the former, but things like checked casts, runtime array covariance checks, etc. are common.
That in turn means that a compiler can safely rely on the type system to generate more efficient code.
Java intended to have a sound type system, but a hole or two have been found (which are fortunately caught at runtime by the VM). Go's type system is sound as far as I know. Dart's type system is sound and we certainly rely on that fact in the compiler.
There is no contradictory information as far as I know, but many people seem to falsely believe that soundness requires zero runtime checks, which isn't the case.
Wow that's a new one for me. But as far as I can tell, that isn't violating soundness because I don't think Java uses checked exceptions as static types in the type system. All this means is that some methods might unwind with an exception type you wouldn't expect it to unwind from.
Would you mind expanding on what you mean by "as static types"?
As I see it, it's definitely a part of Java's type system that things which throw a checked exception will require that you handle those checked exceptions. But now here comes `sneakyThrows` and the next thing you know your `Function#apply` (`R apply(I)`, not a `throws` to be seen in that declaration) is throwing a checked exception (not an `UndeclaredThrowableException` wrapping the checked exception, literally the checked exception ... unchecked).
But I'll admit I'm rather an amateur when it comes to such things.
To violate soundness, you'd need to get into a situation where an unexpected checked exception leads an expression or variable to end up with a value of some type that doesn't match the expression or variable's static type.
This would be easy if the hole worked in the other direction where an exception should be thrown but isn't. Because then you could probably do something like confuse the definite assignment analysis in a constructor body to make it think all fields are initialized by the end of the constructor, like:
class C {
final int x;
C(bool b) {
if (b) {
thingThatMustThrow();
} else {
x = 1;
}
}
}
Here, if the control flow analysis expected that `thingThatMustThrow()` will always throw an exception, then it might conclude that all paths that reach the end of the constructor body will definitely initialize `x`. But if that method doesn't throw an exception, then execution could proceed merrily along and `x` never get initialized.
(In practice, this isn't an issue because field definite initialization analysis is already unsound so the VM default initializes every field anyway.)
But in this case, it goes in the other direction. You have code that isn't expected to throw that does. I can't think of a situation where that would lead Java to end up with a value of the wrong type flowing somewhere unexpected.
Ah, "static" in the sense of "statically analyzable" because it's part of the typing phase. And "sound" here meaning only that the program can only assign values that match the statically determined types. Interesting that "soundness" doesn't include typing effects (at least in the literature), but I guess general typed effects are relatively new and we aren't yet at the point where Koka-like effect types are "expected functionality" when building a new programming language.
What do you mean by a "sound typed language". Go and Java have unsound type systems, and run circles around JS and Dart. Considering your involvement with Dart, I find contradictory information [1].
[1] - https://github.com/dart-lang/language/issues/1461