Are Dart and Java type systems sound?
From Dart docs:
Soundness is about ensuring your program can’t get into certain invalid states. A sound type system means you can never get into a state where an expression evaluates to a value that doesn’t match the expression’s static type. For example, if an expression’s static type is
String
, at runtime you are guaranteed to only get a string when you evaluate it.Dart’s type system, like the type systems in Java and C#, is sound. It enforces that soundness using a combination of static checking (compile-time errors) and runtime checks. For example, assigning a
String
toint
is a compile-time error. Casting anObject
to a string usingas String
fails with a runtime error if the object isn’t a string.
This is an interesting point of view - yes type system is sound (based on the provided definition), but at the same time it means that the application can crash due to type error 🤔.
For example, if I would write:
public class HelloWorld{
public static void main(String []args){
String[] strs = { 1 };
}
}
It will not compile:
$javac HelloWorld.java
HelloWorld.java:4: error: incompatible types: int cannot be converted to String
String[] strs = { 1 };
^
1 error
But this will compile:
public class HelloWorld{
public static void main(String []args){
String[] strs = { "1" };
Object[] objs = strs;
objs[0] = 1;
String one = strs[0];
System.out.println("Hello World");
}
}
and fail:
$javac HelloWorld.java
$java -Xmx128M -Xms16M HelloWorld
Exception in thread "main" java.lang.ArrayStoreException: java.lang.Integer
at HelloWorld.main(HelloWorld.java:6)
I feel like something is twisted here.
Can we say that type system is sound, but static analyzer isn’t?
Or the other way around - if we can say that relying on dynamic type checks is enough to have a sound type system, can we say that Ruby is sound?
1 + "0"
// TypeError: String can't be coerce into Numeric
See also: Java is Unsound: The Industry Perspective
Read more: Is this a type error? (2), Is this a type error?