UPDATE (26 March 2017): In class, most people said the below example is not an example of unsoundness because the program will throw a well-known exception rather than allow undefined behavior. Whether this is sound or not may depend on your point of view, as Cornell professor Ross Tate explains, although the short version is that the Java designers generally consider this sound. I may discuss the definition of soundness we used in class and explore this apparent gap between “the type system guarantees what you expect from the annotations” and “no undefined behavior occurs” in a future post, but for now I recommend waiting for a summary of our class discussion on the PRL blog.
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:
|
1 2 3 4 |
String[] strings = new String[1]; Object[] objects = strings; objects[0] = new Integer(42); String s = strings[0]; |
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.