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.

Cedric on type erasure

I've been meaning to get around to posting on type erasure, and Cedric Beust beat me to it:

The main problem is that reified generics would be incompatible with the current collections.... The extra type information also impacts the interoperability between languages within the JVM but also outside of it.

I completely agree. I used to rail on erasure until I got more experience with it.

The interoperability issue is one big reason I now like erasure. With erased types, the interop layer uses only a very simple type system. Knowledge of complicated type systems stays within the compilers for individual languages.

An additional reason is that it puts the cost of type checking in the compiler rather than in the runtime. With erased types, the compiler works hard to do its type checking, and if it signs off, the code is known to be type safe. At runtime, the types disappear and the code runs at full speed.

This property is more than just pretty. It is very helpful to an engineer trying to build anything using the language. When you write code, you want to know how it is going to perform. With erasure, the things you write convert directly to machine code, just with extra details added such as which variable goes in which register. With reification, you end up with extra crud being inserted everywhere. To understand performance under reified types, you have to reason about this additional type crud. You'd rather not have to.

Two kinds of type inference

There are two separate lines of work on type inference. While they are superficially similar, they face very different design constraints. Let me explain a few of those differences. To begin with, consider the following program. The two kinds of inference reach different conclusions about it.

  class Foo {
    var x: Object = "a string"
    var y: String = "initial value"
    def copy() {
      y = x    // type error, or no?
    }
  }

Should this example type check? There are two points of view.

One point of view is that the compiler is able to prove that x only ever holds strings. Therefore y only ever holds strings. Thus, there will never be a type error at run time, and so the code can be allowed to run as is. This point of view might be called information gathering. The tool analyzes the code, typically the whole program, and learns type information about that code.

Another point of view is that x holds objects and y holds strings, so the "x = y" line is a problem. Yes, the current version of x only holds circles. However, the "x = y" line is using x outside of its spec, and you don't want to use a variable outside of its spec even if you can temporarily get away with it. This point of view might be called slots and tabs. The slot y is not specced to hold the tab x. From this point of view, the indicated line is an error even though the program doesn't have any real problems.

Every user-facing type checker I am familiar with is based on the slots and tabs point of view. The idea is that programmers use types to provide extra structure to their programs. They don't want even nominal violations of the structure; they really want their types to line up the way they say they do. As a concrete example, imagine the author of Foo checks in their code, and someone else adds to the program the following statement: "foo.x = Integer.valueOf(12)". Now the nominal type error has become a real one, but the author of Foo has already gone home. It's better if the author of Foo found out the problem rather than someone else.

That's one example difference between the two kinds of type inference. A slots-and-tab checker will flag errors that an information-gatherer would optimize away. Here are three other design constraints that differ between the two.

Declarations are important for a type checker. For the type checker to know what the slots and tabs are specced as, it must have declared types. In the above example, if x and y did not have declared types on them, then the type checker for class Foo could not determine that there is a problem. To contrast, an information gatherer doesn't necessarily pay much attention to declarations. It can usually infer better information by itself, anyway.

Changing a published type checker breaks builds. For a language under development, once a type checker has been published, it takes great care to change it without breaking any existing builds. Consider the addition of generics to Java 1.5, where it took a great deal of energy and cleverness to make it backwards compatible with all the existing Java code in the world. To contrast, an information gathering type inference can be swapped around at whim. The only impact will be that programs optimize better or worse or faster or slower than before.

Type checkers must be simple. The type system of a slots-and-tabs type checker is part of the contract betwen the compiler and a human developer. Human beings have to understand these things, human beings that for the most part have something better to do with their time than study types. As a result, there is tremendous design pressure on a slots-and-tabs type checker to make the overall system simple to understand. To contrast, the sky is the limit for an information gatherer. The only people who need to understand it are the handful of people developing and maintaining it.

Overall, I wish there was some term in common use to distinguish between these two kinds of type inferencers. Alas, both kinds of them infer things, and the things both of them infer are types, so the terminology seems inevitable. The best that can be done is to strive to understand which kind of type inferencer one is working with. Developers on one or the other face different design constraints, and they will find different chunks of the published literature to be relevant.

Types are fundamentally good?

Once in a while, I encounter a broad-based claim that it's fundamentally unsound to doubt the superiority of statically typed programming languages. Bob Harper has recently posted just such a claim:

While reviewing some of the comments on my post about parallelism and concurrency, I noticed that the great fallacy about dynamic and static languages continues to hold people in its thrall. So, in the same “everything you know is wrong” spirit, let me try to set this straight: a dynamic language is a straightjacketed static language that affords less rather than more expressiveness.

Much of the rest of the post then tries to establish that there is something fundamentally better about statically typed languages, so much so that it's not even important to look at empirical evidence.

Such a broad-based claim would be easier to swallow if it weren't for a couple of observations standing so strongly against it. First, many large projects have successfully been written without a static checker. An example would be the Emacs text editor. Any fundamental attack on typeless heathens must account for the fact that many of them are not just enjoying themselves, but successfully delivering on the software they are writing. The effect of static types, whether it be positive or negative, is clearly not overwhelming. It won't tank a project if you choose poorly.

A second observation is that in some programming domains it looks like it would be miserable to have to deal with a static type checker. Examples would be spreadsheet formulas and the boot scripts for a Unix system. For such domains, programmers want to write something quickly and then have the program do its job. A commonality among these languages is that live data is often immediately available, so programmers can just as well run the code on live data as fuss around with a static checker.

Armed with these broad observations from the practice of programming and the design of practical programming languages, it's easy to find problems with the fundamental arguments Harper makes:

• "Types" are static, and "classes" are dynamic. As I've written before, run-time types are not just sensible, but widely used in the discussion of languages. C++ literally has "run-time types". JavaScript, a language with no static types, has a "typeof" operator whose return value is the run-time type. And so on. There are differences between run-time types and static types, but they're all still "types".
  
• A dynamic language can be viewed as having a single static type for all values. While I agree with this, it's not a very useful point of view. In particular, I don't see what bearing this single "unitype" has on the regular old run-time types that dynamic languages support.
  
• Static checkers have no real restrictions on expressiveness. This is far from the truth. There has been a steady stream of papers describing how to extend type checkers to check fairly straightforward code examples. In functional languages, one example is the GADTs needed to type check a simple AST interpreter. In object-oriented languages, the lowly flatten method on class List has posed difficulties, because it's an instance method on class List but it only applies if the list's contents are themselves lists. More broadly, well-typed collection libraries have proven maddeningly complex, with each new solution bringing with it a new host of problems. All of these problems are laughably easy if you don't have to appease a static type checker.
  
• Dynamic languages are slow. For some reason, performance always pops up when a computer person argues a position that they think is obvious. In this case, most practitioners would agree that dynamic languages are slower, but there are many cases where the performance is perfectly fine. For example, so long as Emacs can respond to a key press before I press the next key, who cares if it took 10 microseconds or 100 microseconds? For most practical software, there's a threshold beyond which further performance is completely pointless.
  

Overall, type checkers are wonderful tools. However, any meaningful discussion about just how they are wonderful, and to what extent, needs to do a couple of things. First, it needs some qualifiers about the nature of the programming task. Second, it needs to rest on at least a little bit of empirical data.

Typing arithmetic in Datalog

Unlike in imperative languages, arithmetic in Datalog can execute in different orders. If you write a formula z=x+y in an imperative language, then the meaning is that you compute x, you compute y, and then you add them together to produce z. If you want to understand the typing of such an expression, you first find the types of x and y, and then look at the numeric conversion rules to see what the type of z must be. If x is a 32-bit integer and y is a 64-bit floating-point number, then z will be a 64-bit floating-point number.

In Datalog, there are additional options for using the same formula. One option is to do as in an imperative language, compute x and y, and then use the arithmetic formula to compute z. However, you could just as well compute x and z and then subtract to find y. In total there are four different ways to use the formula: you could use it to compute x, y, or z, or if all three are already computed, you could add them up and verify that they are in a proper relation with each other. How can we reason about the typing implications about an arithmetic formula matching?

Call such a constraint an arithmetic type constraint. Such a constraint must treat x, y, and z symmetrically, so think of them as being in a set. That is, an arithmetic type constraint is defined by a set of variables. If the variables are x, y, and z, then the arithmetic constraint for them could be written arith({x,y,z}).

It appears to work well to treat an arithmetic constraint as equivalent to the following set of individual constraints:

 
  // constraints for arith({x,y,z}) are:
  x <= lub(y, z)
  y <= lub(x, z)
  z <= lub(x, y)

In these constraints, "<=" means subtype-of, and "lub" means least upper bound. The lub of two types is the smallest type that is a supertype of both of them. For numeric types, humor me and think of subtyping as including valid numeric upcasts, so int32 is a subtype of float64. This post is already too long to get into subtyping versus numeric conversion.

Try these equations on a few examples, and it appears to work well. For example, if x and y are already known to be int32, then these constraints imply that z is no larger than lub(int32,int32), which is just int32. As another example, if x is an int32 but y and z are completely unknown, then these constraints give no new bound to anything. As a final example, if all three variables already have a known type, but one of them is a larger type than the other two, then the third one can be shrunk to the lub of the other two.

In general, these constraints will only allow the types of three variables to be in one of the following four combinations:

• All three types are completely unknown.
• One type is known but the other two are unknown.
• All three types are the same.
• Two of the types are the same, and the third type is a subtype of the other two.

The first two cases will eventually lead to a compile-time error, because the programmer has introduced variables but not provided a way to reliably bind those variables to values. The third option is a normal, happy case, where there are no numeric conversions being applied. The fourth option is most interesting, in my view, because there is an operation between two types and the result is the lub of those two types. Notably absent from the list is any combination where all three types are different.

As one final wrinkle, it's arguably more programmer friendly to always perform arithmetic on at least 32-bit if not 64-bit values. Otherwise, when a programmer writes 127+1, they might get 8-bit arithmetic and thus an overflow. To make arithmetic work that way, it's possible to add a minimum type to an arithmetic constraint. For example, arith({x,y,z},int64) would be an arithmetic constraint over x, y, and z, and a minimum result type of 64-bit integers. This would be equivalent to the following combination of constraints:

  
  // constraints for arith({x,y,z}, int64) are:
  x <= lub(y, z, int64)
  y <= lub(x, z, int64)
  z <= lub(x, y, int64)

Type checkers aren't just error detectors

Type checking is frequently put forward as a way to find errors that otherwise would have slipped through testing. I've never found this a very compelling argument, though. Before software is released, or even a patch committed to the shared repository, the developers go through various kinds of effort to convince themselves that the latest changes to the software behave correctly. There are a myriad of ways to do that, ranging across code inspection, testing, and formal methods, but whatever ways are chosen, the software doesn't move forward until it's been verified. At that point, not that many type errors can realistically remain.

There are larger advantages to having a type checker. Let me describe three.

Data Modelling. A lot of what programmers do is develop a model of the data their programs work on. All modelling approaches I know, bar none, involve using types. For example, ORM, UML, XML DTDs, Protobuf schemas, and SQL schemas all use types prominently. If you have types in the programming language, then the program itself can embed parts of the data model explicitly.

A Second Perspective. In all software groups I have been a part of, most of the software written gets far less code review than would be beneficial. Software gets much better just by having people scan their eyes across it and think about it, but practicing engineers dread spending the time to do it. A type checker forces programmers to understand their code two ways: the logical behavior, and the type signatures. By doing so, they force programmers to do a little bit more code review.

Adding rigidity. Typed languages have a higher percentage of sensible programs in them. Just like it's easier to dial a TV than a radio, it's easier to code in a typed language. You can turn a TV dial to just any old location; you have to choose among a small, discrete number of settings. When writing new program code, you can write a rough sketch and then use the type checker to guide you on the details. For refactoring, you can make an inital change and let the IDE guide you to the other ones. It's much faster than if you have to run the test suite more often or have to filter through raw text searches.