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.