The types will save us!
So, that went over well. My goal was simply to point out that strong and static typing are not the same thing (and, correspondingly, that weak and dynamic typing are not the same thing), and somehow the comment thread got derailed into people trotting out exotic type systems and theoretical work to try to prove… well, I’m not sure exactly what they want to prove. But one big thing that seems to be causing trouble is this statement:
a common myth of some type systems is “if it passes type checks, it must be correct”. Most people who fall into that pit learn sooner or later that type errors are just one class of errors, and that the strictest, “safest” typing in the world can’t stop you from writing a program that does something stupid.
Boy, did some people ever have problems with that statement. Unfortunately, it’s true: type errors are a subset of the assorted errors a programmer can make, not the set of all such errors. For example, consider a language with a function add, of type int -> int -> int, and so intended to implement integer addition. Now let’s assume the programmer made a boneheaded error in his algorithm, and add 2 2 returns 5. Well, it passes the type check, so it must be correct, right?
If this seems like a contrived example, imagine a function of type float -> float -> float. Might not seem so contrived anymore; floating-point numbers are the very devil to get right.
A story about Hilda
For a better example, consider a data type I was looking at a little earlier tonight: US Social Security numbers. At first, they look like they’re easy as pie to work with: three digits, a hyphen, two digits, another hyphen and four more digits. You can even normalize out the hyphens and just say that an SSN is a nine-digit number. So you could just set up your favorite language’s equivalent of a user-defined type, and you’d be good to go. Right?
Well, you’d be good until you ran into 000-00-0000, which isn’t a valid SSN. So you refine your definition a bit and you’re good to go. Oh, and the first group can’t be “666” because that has strongly-negative religious connotations. So that’s another refinement to the definition. And all is well and good, until you run up against 987-65-4320, which is a well-formed SSN but is also permanently invalid — 987-65-4320 through 987-65-4329 are reserved for promotional and explanatory documents which need to show example numbers. But again, this isn’t a terribly hard refinement to make, and you can get back to a definition which rigorously guarantees you’re working with valid data.
Until you run into 078-05-1120. If you don’t catch that as invalid, employees of the Social Security Administration will reserve the right to laugh at you. But why? It looks right:
- It’s in the correct format.
- Its area (the first set of digits) is allocated (to New York) and in use (you’re checking for that, right?).
- Its group number (the second set of digits) is allocated for its area (you are checking for that, right?).
- Its serial number (the final set of digits) is valid, and in fact this very number was issued by the SSA once upon a time.
But it’s still not a valid number. For a short span of years, it was the Social Security number of Hilda Whitcher, a secretary at the E. H. Feree Company, which manufactured mens’ wallets. You may be able to guess where this is going, but I’ll finish the historical anecdote because it’s amusing: back in the days when Social Security was new, the E. H. Feree Company decided that a selling point of its wallets would be the ease with which you could carry your Social Security card. And to promote this, they included an example card in every wallet, with an example Social Security number. Hilda Whitcher’s Social Security number. Many confused customers assumed this was now their SSN, and began to use it; eventually, the number was invalidated and Hilda got a new one, but people were still trying to use her original SSN decades later. As a result, it’s a poor SSN checker that doesn’t recognize and reject this infamous number.
So now you get to special-case your definition of a Social Security number to deal with a few odd numbers which have been permanently invalidated by the SSA. And that’s after you’ve figured a way to keep up with new block allocations — the SSA updates those monthly.
Any type system which could correctly describe the byzantine and ever-changing nature of this particular data type would need to be Turing-complete in its own right, at which point you’re left wondering whether your type system needs a type system. Philosophers (I love relating things back to my degree) and mathematicians ran into similar problems in the twentieth century, when they realized that certain paradoxes of language could only be resolved by resorting to a “metalanguage” which could talk about language. But then they needed a “metametalanguage” to talk about the “metalanguage”, and it turned out it was turtles all the way down, which turned out not to matter because Kurt Gödel had come along and proved that you could always trick a language into talking about itself anyway.
What’s the point?
Types are great. But they’re not everything, and shouldn’t try to be everything; it’ll just end in tears (though you guys who are implementing the predicate calculus and rules of inference in a type system have a warm and fuzzy place in my heart). Sooner or later you’ll run into classes of errors which can only be unearthed by a robustly programmable way to check your code, and the name for that is “unit test”, not “type system”. “If it compiles, it must be correct” wasn’t true back when some people believed it, and “if it passes type checks, it must be correct” isn’t true now.
And now I’ve said more than I ever intended to on the topic, so I’ll shut up.