Wednesday, January 25, 2012

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();

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.

Sunday, January 22, 2012

DNS takedowns alive and well

I wrote earlier that PROTECT-IP and SOPA are getting relatively too much attention. Specifically, I mused about this problem:
First, DNS takedowns are already happening under existing law. For example, the American FBI has been taking down DNS names for poker websites in advance of a trial. SOPA and PROTECT-IP merely extend the tendrils rather than starting something new.

Today I read news that indeed, the FBI has taken down the DNS name for I'm not sure the American public is in tune with precisely what its federal government is doing.

The news has other sad aspects than the use of DNS takedowns. A few other aspects lept out for me:

  • There has been not yet been a trial. If I ask most Americans about how their legal system works, I expect one of the first things people would say is that, in America, people are innocent until proven guilty.
  • There is twenty years of jail time associated with the charges. Isn't that a little harsh for copyright violations? I think of jail as how you penalize murderers, arsonists, and others who are going to be a threat to the public if they are left loose. Intellectual property violations somehow seem to not make the cut.
  • It's an American law, but New Zealand police arrested some of the defendants.
  • The overall demeanor of the authorities comes off as rather thuggish. For example, they seized all manner of unrelated assets of the defendants, including their cars.
I am glad SOPA and PROTECT-IP went down. However, much of what protesters complained about is already happening.

Monday, January 2, 2012

DNS takedowns under fire in the U.S.

I get the impression that SOPA, the latest version of a U.S. bill to enable DNS takedowns of non-American web sites, is under a lot of pressure. A major blow to its support is that the major gaming console companies backing out.

I am certainly heartened. However, the problem is still very real, for at least two reasons.

First, DNS takedowns are already happening under existing law. For example, the American FBI has been taking down DNS names for poker websites in advance of a trial. SOPA and PROTECT-IP merely extend the tendrils rather than starting something new.

Second, this bill won't be the last. So long as the Internet uses DNS, there is a vulnerability built right into the protocols. Secure DNS doesn't make it any better; on the contrary, it hands the keys to the DNS over to national governments.

The only long term way to fix this problem is to adjust the protocols to avoid a single point of vulnerability. It requires a new way to name resources on the Internet.