Type systems help with “a class of errors”: factual, but not true.

A common characterization of type systems is to say they help with “a certain class of errors”. This is literally true, but usually serves to obscure the real issues. Perhaps I can help reveal them.

In one way, this is meant to say “hey, your code may pass the type checker, but that doesn't mean it's bug-free”. This is probably something many people who have never used latent typing need to hear and internalize; as I previously said in bold, type systems partially prove correctness. Untested code may still crash or give wrong results, no matter how wonderful the type checker says it is. Type checking cannot replace testing, and perhaps it may never entirely.

But saying “a certain class of errors” is usually meant to imply that this is just an itty-bitty area of erroneous programming that's going to be found and squashed in testing anyway. This leads to bad thinking in two ways:

First, limited to “a certain class” though it may be, the type system prevents errors in that area. As previously stated, that's in a whole other universe than what testing can provide.

Secondly, and more importantly, it ignores that once you have a powerful type system, you can design your programs so that they pull more information about the program into the type system, so that the typer can eliminate more errors.

Take a type for pain relief

For example, consider the ubiquitous java.lang.NullPointerException and its relatives in other programming environments. Irritating, shows up everywhere, often too far away from the real cause of the error for the backtrace to be a great deal of help, and has a nasty habit of not popping up until real users try your program.

Haskell users just laugh at this, because they pulled the idea of a missing object into the type system:

     data Maybe a = Nothing | Just a 

Here | means “or”, and a is the type we're wrapping up in a Maybe. Now, when an operation can fail, everyone using that operation has to propagate or suppress the failure using either explicit matching or the (very powerful, but more on that later) higher-order functions provided for the purpose.

Much of typeful programming is thinking of ways to use the features of the type system to expand the range of things that can be automatically proven about the program. What you see in C and Java are poor examples of that, as I will briefly touch on next.