As part of this semester’s History of Programming Languages course at Northeastern, Matthias tasked the students (and people like me who just sit in from time to time) to figure out how they would explain type soundness to the typical software developer who’s not familiar with programming languages research or formal semantics. The in-class discussion is tomorrow, so watch the PRL blog for a summary of the full class discussion. In the meantime, here’s what I came up with:
Type soundness is a formal means of proving that your language’s type system won’t “lie” to you. For example of what I mean by lying, take the following example Java snippet:
String strings = new String;
Object objects = strings;
objects = new Integer(42);
String s = strings;
This snippet type-checks, but it appears to do something weird: line 3 inserts an integer into an array, but when we retrieve that item from the array, somehow we can magically treat it as a string! That shouldn’t happen: the whole point of the type system should ensure that if we have a variable of type
String, then it should definitely be a string.
It turns out that at run-time, when an item is inserted into an array, Java will check that the type of the item matches the actual type of the array and throw an
ArrayStoreException if they don’t match.
This is an example of how Java’s type system is unsound: the type-checker confirms that “objects” is an array of
Objects (into which we expect to be able to store any kind of object), but in reality it can only store strings.
A sound type system is one that guarantees a type-related error will not occur if the program type-checks. Exactly what a “type-related error” is depends on the particular language, but generally it means applying an operation to the wrong kind of arguments, such as inserting an integer into an array of strings, or concatenating a boolean onto a string.
Sound type systems reduce the amount of reasoning programmers have to do by ensuring that certain kinds of executions will never happen. An unsound type system, on the other hand, helps find bugs, but programmer can’t rely on the type-checker to prove that no type-related bugs exist in their program.