The good and bad of type checking, by example

I enjoyed watching Gilad Bracha present Dart to a group of Stanford professors and students. As one might expect, given Bracha's background, he spends considerable time on Dart's type system.

Several members of the audience seemed surprised to find a defender of Dart's approach to typing. They understand untyped languages such as JavaScript, and they understand strictly typed languages such as Java. However, they don't understand why someone would intentionally design a language where types, when present, might still fail to hold up at run time.

One blog post will never convince people one way or another on this question, but perhaps I can show the motivation and dissipate some of the stark mystification around Dart's approach. Let me provide two examples where type checking would complain about a program. Here's the first example:

String fileName = new File("output.txt");

I find examples like this very compelling. The programmer has made an easy mistake. There's no question it is a mistake; this code will always fail when it is run. Furthermore, a compiler can easily detect the mistake simply by assigning a type to each variable and expression and seeing if they line up. Examples like this make type checking look really good.

On the other hand, consider this example:

void drawWidgets(List<Widget> widgets) { ... }
List<LabelWidget> labels = computeLabels();
drawWidgets(labels);

This program is probably fine, but a traditional type checker is forced to reject it. Even though LabelWidget is a subclass of Widget, a List<LabelWidget> is not a subtype of List<Label>, so the function call in the last line will not type check. The problem is that the compiler has no way of knowing that drawWidgets only reads from its input list. If drawWidgets were to add some more widgets to the list, then there would be a type error.

There are multiple ways to address this problem. In Java, programmers are expected to rewrite the type signature of drawWidgets as follows:

void drawWidgets(List<? extends Widget> widgets) { ... }

In Scala, the answer would be to use an alternate List type that is covariant in its argument.

Whatever the solution, it is clear that this second example has a much different impact on developer productivity than does the first one. First of all, in this second example, the compiler is probably wrong, and it is just emitting an error to be on the safe side. Second, the corrected version of the code is much harder to understand than the original; in addition to parametric types, it also uses an bounded existential type variable. Third, it raises the bar for who can use this programming language. People who could be perfectly productive in a simply typed language will have a terrible time with quantifier-happy generic Java code. For a host of reasons, I feel that on net the type checker makes things worse in this second example. The cases where it prevents a real error are outweighed by all the problems.

Dart's type system is unusual in that it is consistent with both examples. It rejects code like the first example, but is quiet for code like the second one.