Type System vs Test Driven Development
groups.google.com
groups.google.com
xs == reverse (reverse xs)
QuickCheck will generate hundreds of random lists and make sure that the property holds. This can be enormously useful in smoking out odd problems in complex functional code.
For simpler testing scenarios, HUnit is OK, although it sometimes feels a bit clunky.
In my work, the types are usually so nailed-down there isn't any question about them. Yet the problems can be so nonlinear and ill-conditioned that even moderate testing-- say, hitting the code with 1000 test cases-- is just not enough to convince myself it's working correctly. It often happens that a unit test runs just fine at that level, but bumping it up to 10,000 or 100,000 cases reveals weaknesses in the code.
Illustrative example follows-- no need to read if you "get" that, in some fields, a type system simply doesn't detect the interesting bugs. A few months ago, I was testing methods for solving problems of sorption to room surfaces. In terms of types, it could hardly get more explicit. Take an object representing a sorption isotherm, plus two double-precision numbers giving gas- and sorbed-phase concentrations, and return the equilibrium concentration at the sorbent surface. The only way to specify the types more completely would be to tag all the numbers involved with units.
Guaranteeing convergence turned out to be a royal pain. To get a useful answer, you need to force convergence to very tight tolerances-- tight enough that, on ill-conditioned problems, you run the risk of asking for answers below the machine precision. That means you need two termination tests-- one on the defining equation (is the error close enough to zero?), and one on the returned result (is the current best answer within a tight enough bracket?). And within that framework, it's very easy to create algorithms that, due to finite-precision effects, fall into infinite loops because they fail to actually change a bracket point when they add a small number to it.
So again, types were not an issue. The only way I was sure I had all the convergence pitfalls out of the way was extensive unit testing. And the baby tests I ran during initial development-- sampling 1000 combinations out of a database of sorbents and chemicals-- simply didn't do it. Once I had "working" code, and stepped up sampling to the 100,000 range, it was easy to discover oddball combinations that would cause problems.
Why can't a type system keep track of units? Why can't it be aware of precision? If it's possible for you to find a proof that a particular implementation of your algorithm won't fall into an infinite loop, then there is a type system that can verify that your algorithm will terminate. Of course, actually designing a sound type system with this property could be quite tricky, and I have no idea what the resulting language would look like -- but it would be possible.