There is no One Answer

Ryan: You’re falling directly into the fallacy I was adressing- assuming that static typing and unit testing are mutually exclusive. Or, at least if you have one, you don’t need the other. And that therefor, if I advocate using static typing, I must be advocating not using unit testing. It’s not a case of either or: in fact, I’m an advocate of using both.

Static typing, in a language with a good type system (by which I explicitly exclude Java, #, C++, and Pascal, and instead mean languages like SML, OCaml, and Haskell) can check for more errors, and more subtle errors, than most people suspect. It can be used to enforce constraints like “you can not ansynchronously read a file descriptor opened for synchronous I/O” or “a Postgresql cursor may not be used outside of the transaction it is declared in” (both of these I’ve seen enforced in Ocaml). And when it gives a gaurantee, it means it. And when the constraint is violated, the compiler tells you exactly where- file, line number, even what columns are the problem. I’ve occassionally seen Ocaml be 20 lines off (where the problem really was was 20 lines away from where Ocaml thought the problem is), but 99% of the time it’s dead on. It’s a great advantage to debugging, let me tell you. And it comes free with your language.

But you’re right that it doesn’t catch all errors. Neither does. Neither does the combination. But the more errors are caught, and sooner, the better.

The fundamental fallacy of Obie’s statement is the assumption that increased risk causes the programmer to exercise increased care- in other words, that the reason programmers create bugs is because they’re lazy and they don’t care. There are programmers for whom this is true- but dynamic typing doesn’t help them either, as it doesn’t change the fundamental fact that they’re lazy and apathetic. But the vast majority of programmers I’ve worked with are neither- but they are human. Mistakes will be made. The only question is what the cost of those mistakes are.

Dan: if you want to have real fun, grab an open-source C/C++ project, and then turn on all warnings. Not just the default ones, not just the -W -Wall ones (there are dozens of optional warnings GCC has that are not turned on by -W -Wall), all of them.

Brian

See, here is where we differ. I don’t see static typing as “banal and trivial” at all- but rather “basic, fundamental, and necessary”. I’d love to spend all my time discussing “deeper” concepts (and, in fact, I do spend most of my time talking about deeper concepts)- but it’s hard to discuss the possibility of journeying to the moon with someone who still beleives the earth is flat. “Can’t we drop the whole is the earth flat or round debate and move on to more interesting arguments in physics?” Um, no, not while the vast majority of people still believe it to be flat.

Looking back over my blog posts, my recent obsession has been much more about lazy, concurrent, asynchronous, and deferred computation rather than just static typing. Unfortunately, the trick with asynchronous computation in all of it’s form is less expressing the asynchronicity, so much as expressing it correctly. To my knowledge, asynchronous computation is by far the hardest thing programmers are doing right now.

And one of the reasons it’s so hard is that it is very easy to write code that mostly works, and only occasionally doesn’t. Which is why, of the two main ways we have to validate code correct (testing and typing), testing is useless in the face of this problem. Unless you’re willing to have unit tests that take days to run (yes, I have had to track down race conditions that only happened once every several days, even under extreme test loads). Typing, on the other hand, being the country cousin of code correctness proofs, has a lot of promise in attacking the problem. But it is very easy, in my mind at least, to make the argument that static typing is necessary (even if not sufficient) to solve the problem. So any deep post I do make is liable to have static typing as a prerequisite, either implicitly or explicitly.

Another point I will make is that typing is, itself, a deeper subject than most programmers know. I’ve been kind of reluctant to delve into the subject in a deep way myself, because I know how little I really know about the subject. But here’s a little something to whet your whistle on the subject, and maybe make you stare off into space a little bit. Consider the type ‘a -> (‘a -> ‘b) -> ‘b. There are two ways to interpret this. One is as an (Ocaml/SML style) type- this is the type of a function that takes an argument of type a and returns a function that takes an argument of a function that takes a type a and returns a value of type b, and returns a value of type b.

Another way to read this is as a statement in propositional logic: if statement a is true, this implies that if statement a implies statement b, then statement b is true. Here, the -> operator means “implies”, not “function type”. By constructs like this, it can be seen that every correctly typed program is, by looking at it in a different way, a proof in propositional logic.

After digesting this for a bit, it should come as no surprise that the “patron saints” of functional programming- Alonzo Church, Haskell Curry, etc.- weren’t studying programming or computation, they were studying the foundations of mathematical logic.