Static typing: the presumption of guilt

I was listening to Software Engineering Radio recently; the interview with Gilad Bracha on Newspeak. In it, Gilad talks at length about dynamic typing, and its superiority over static typing. This was the best argument for dynamic typing I’d heard, and it slotted perfectly with my growing respect for dynamic typing.

Some background information: Gilad Bracha co-wrote the second and third Java Language Specifications. He is the creator of Newspeak, a dynamically typed languaged influenced by Self and Smalltalk. While a statically typed language has metadata in the form of type information, Newspeak types can have rich and arbitrary metadata, but its use is not enforced by a type-checker. Tools can be used to read this metadata and give the programmer useful information about the state of the program, but there are no rules its use.

It’s best if I just let Gilad do the talking. I could paraphrase his points but I wouldn’t say it as well.

Gilad Bracha I have a long-standing religious war going on this thing [typing]. I’ve spent a lot of my time working with types; unlike most proponents of dynamic languages I’ve spent a lot of work building static type systems, and I know what they are. And I know what they are good for: they’re mainly good for documentation – documentation for both man and machine. The idea that they make your programs more reliable is a myth. They also have the advantage that it is easier to optimise, but that’s not essential, that’s been proven time again. Most of the hotspot technology that makes Java fast was developed for Self and Smalltalk. It doesn’t necessarily rely on the typing. Some things do, because the typing’s there and people tend to use that. But the real value is that humans who read this can quickly get an idea of what this thing does, and machines can do that, so you can do better name completion, better refactoring, etc., etc.

Markus Völter So with machines you don’t necessarily mean the compiler, but the tooling for the language.

GB Yes. And so I’m all for having what I call pluggable, or optional type systems. The difference is the conventional approach is the type system is part of the language. If you don’t pass the type-checker your program isn’t legal; it won’t run; the compiler will spit it back in your face. The idea with an optional type system is, OK, you write these types; you can run a type-checker; it can tell you what it thinks; it does not affect your semantics; it doesn’t change what the program does, and it certainly doesn’t prevent you from running the program just as if it had no types at all.

MV Why would you run a program whose type-checker, even if it’s optional, tells you your types are wrong?

GB Because what type-checkers do is they attempt to prove that your program conforms to the type system. The type system guarantees you that, if you conform to it, certain types of bad thing won’t happen. That doesn’t mean that if you don’t conform to it bad things will happen. They do not prove that your program is bad; they prove that your program isn’t good, according to their definition of good. And their definition of good is always too restrictive inherently, because the only way to tell if it’s really good is the runtime semantics.

MV But if I try to add 2 to a string, that will never make sense, right?

GB If you add 2 to a string, it may never make sense … but that isn’t really the problem. This is the kind of toy example that theoreticians give you, but that really isn’t the problem. The problems are much more subtle than that. And there are a lot of things that do make sense. It’s sort of like the Anglo-Saxon legal system versus I believe the Napoleonic one: are you innocent until proven guilty or are you guilty until proven innocent? We generally don’t assume that someone should be arrested because he can’t prove that he didn’t do anything wrong. A type system is essentially Napoleonic law. It arrests you because you can’t show that you’re worthy. That’s one issue, the flexibility. There are other issues, which really boil down to documentation.

One of the amusing arguments that people bring up often nowadays: they’ve learned to appreciate IDEs – something that comes from the Smalltalk world, essentially, and the early Lisp world, and so forth – and now they tell you “our IDEs can do such a wonderful job refactoring, and without type information you probably can’t do as well”. And they sort of neglect the fact that where did refactoring come from? It came from Smalltalk. And the Java world, they didn’t invent this, because one of the things these type systems do is it makes it hard to invent things. It makes it hard to do meta-programming, it makes it hard to do things that the language designer didn’t anticipate as typical use-cases. Because then your type-checker says “no, I can’t prove that that’s OK” and it’s very hard to be creative. The wonderful thing about dynamic typing is it lets you express anything that is computable. And type systems don’t – type systems are typically decidable, and they restrict you to a subset. People who favour static type systems say “it’s fine, it’s good enough; all the interesting programs you want to write will work as types”. But that’s ridiculous – once you have a type system, you don’t even know what interesting programs are there.