27 September 2014
A type checker is a program that reads other programs and makes certain assertions about them. If your program passes the type checker, then depending on the type system the checker implements, you can make a great deal of important assumptions about the way your program works. But programmers aren't the only things that leverage the type checker -- other things do as well, such as compilers.
Wikipedia claims that "the main purpose of a type system is to reduce bugs in computer programs" . This is nonsense. The most popular type system in the world, that of C, plainly exists to make certain guarantees about C programs for C compilers to leverage. Programmer friendliness is a distant second.
I'm often struck by the number of people who don't realize this. Many, many important type systems were designed almost exclusively for the benefit of compilers. Much of the confusion over type systems can be traced to people who work in languages with human-friendly type systems (OCaml, Haskell) talking to people who work with compiler-friendly type systems (C, C++). Working with types in these languages are very, very different experiences, and, to be blunt, many of the people in the human-friendly camp don't seem to remember how inhuman the type systems in the compiler-friendly camp are.
Another source of confusion comes from people who use compiler-friendly type systems but think that they are using human-friendly type systems. The most obvious example of this Java, which has an atrocious type system, but somehow has legions of advocates who seem to be under the impression that its primary purpose is to help them rather than help the Java compiler create valid bytecode.
I don't believe that languages with human-friendly type systems are necessarily superior to other languages, or that you even have to choose. It seems very possible to have everything: an advanced type system, an advanced runtime, and an advanced compiler. But I recognize that depending on the particular circumstances around the development of a language, language designers might emphasize different things at different times.
A good example of this is the Go programming language. Go's type system is much better than that of C, but it still doesn't offer too much to humans. It is, however, fantastic for the Go compiler. The language designers have sacrificed power in the type system for simplicity in the compiler design (and, it seems to be implied, speed at both run and compile time).
To me, that seems like an acceptable tradeoff. Others might disagree. But next time you browse the mailing lists while SBT runs, ask yourself: are you making a tradeoff without even realizing it?