I've just gotten back from the awesome mloc.js conference. There was a talk about compiling C# to JavaScript and one of the benefits explained was static types. Someone from the audience asked, who needs types when you do Test Driven Development?
I tried to address the question in my talk on Roy but I talked to some developers afterwards and they thought that TDD is the only tool necessary for writing code that satisfied their specifications!
So here's a blog post where I'll try to show two cases where TDD doesn't solve my specifications. In the first case, we get a free proof (i.e. TDD is unnecessary). In the second case, we aren’t able to encode some of our constraints in tests or types, so we need to use mathematical reasoning to derive a satisfactory implementation (i.e. TDD isn't enough).
Imagine that we know that we need a function that returns its argument. The input is polymorphic - it can be any value. In a typed language the function would look like:
α → α
This means, for any value input, the output value must have the same type. For example. if we supplied the empty string, α would be instantiated as the String type and the function would become:
String → String
Easy. Now let's try to implement this function:
id :: α → α
id a = ???So the problem is that we don't know what the input type is inside the function. All we know is that it's the polymorphic type α - the same type as the value we have to return.
In a total language, the only possible α we can return is the input. In a partial language, there are some ways to lie to the type-system and say we have an α; we rely on programmers to not do that (just like we rely on programmers to write working tests).
This means there is only a single possible implementation for this function:
id :: α → α
id a = aIf this satisfies a type-checker, we're done. No need to write a test
- the compiler proved it correct! This is a concept called parametricity.
Types can give you assurance that your code is correct. Tests only give you confidence that your code is correct. But the identity function is the most trivial of all functions, you could definitely TDD that in a few minutes and have high confidence of correctness.
Let's do something more complicated but also something used everyday
in functional programming: the map function.
The map function works for anything that is a Functor. Lists and
arrays are immediate examples. The interesting thing is that for any
Functor, there's only a single possible implementation of map. In
fact, Haskell can automatically write a proven implementation with
the -XDeriveFunctor flag:
{-# LANGUAGE DeriveFunctor #-}
data TestResult a = Success a | Failure String | Skipped deriving FunctorThe above defines a type called TestResult which has three separate
states. The Success state has a polymorphic value which can be
mapped over. Haskell finds the polymorphic value and writes the map
function for us!
Getting the compiler to automatically derive a proven implementation: better than TDD.
You can't encode runtime guarantees as tests. Daniel Spiewak gave me an awesome example: asymptotic complexity.
We need a sort function. Given a list/array of integers, we want to get a sorted list back. Here's some test-driven tests for the function:
prop_head_is_minimum xs = not (null xs) ==> head (sort xs) == minimum xs
prop_last_is_maximum xs = not (null xs) ==> last (sort xs) == maxmimum xs
prop_is_sorted xs = isSorted $ sort xs
where isSorted [] = True
isSorted [x] = True
isSorted (x:y:xs) = x < y && isSorted (y:xs)The above uses property-based testing (via
QuickCheck). The xs is a
value that is automatically generated by the test framework by
looking at the type signature - we don't have to worry about boundary
conditions or interesting cases; they will be
generated. Real World Haskell has
a
great Chapter about property-based testing
for anyone new to the concept.
Anyway, let's use the tests to write an implementation for sort:
sort :: [Int] -> [Int]
sort [] = []
sort xs = select xs []
where select [] ys = ys
select xs' ys = select (delete (maximum xs') xs') $ maximum xs':ysAwesome! TDD gave us code that works. We're done, right?
Well, hopefully we almost always want the asymptotically optimal algorithm to solve our problem. You might have noticed that the above code is selection sort - an algorithm with best/worse/average time complexity of O(n^2).
Sadly, we can't write a test or a type to satisfy our specification. We need to actually perform some (asymptotic) analysis to derive our code, instead of relying on tests!
TDD isn't enough. We still need analysis.
This post isn't saying that TDD shouldn't be used - it's absolutely fine to do TDD. This post is just to point out that TDD doesn't completely replace types nor analysis of code.
When you work in a typed language, you don't have to write tests for some functions. They're proven to be correct by the type checker. But you can't rely exclusively on types or tests. You have to use analysis to ensure runtime guarantees are satisfied.
Analysis is the method for writing code that satisfies our constraints. Neither TDD nor types are the single answer to writing code that does what we want.
TDD can be useful. Types can be useful. Analysis is necessary.