Types don't substitute for tests

When reading discussions about the benefits of types in software construction, I've come across the following claim:

When I use types, I don't need as many unit tests.

This statement is not consistent with my understanding of either types or test-driven design. When I've inquired into reasoning behind the claim, it often boils down to the following:

Types provide assurance over all possible arguments (universal quantification). Unit tests provide assurance only for specific examples (existential quantification). Therefore, when I have a good type system I don't need to rely on unit tests.

This argument does not hold in my experience, because I use types and unit tests to establish different kinds of properties about a program.

Types prove that functions within a program will terminate successfully for all possible inputs (I'm ignoring questions of totality for the sake of simplifying the discussion).

Unit tests demonstrate that functions yield the correct result for a set of curated inputs. The practice of test-driven design aims to provide confidence that the inputs are representative of the function's behaviour through the discipline of expanding a function's definition only in response to an example that doesn't yet hold.

All of the examples that I use in my practice of test-driven design are well-typed, whether or not I use a type system. I do not write unit tests that exercise the behaviour of the system in the presence of badly-typed input, because in an untyped programming language it would be a futile exercise and in a typed programming language such tests would be impossible to write.

If I write a program using a type system, I still require just as many positive examples to drive my design and establish that the generalisations I've created are faithful to the examples that drove them. Simply put, I can't think of a unit test that I would write in the absence of a type system that I would not have to write in the presence of one.

I don't use a type system to prove that my functions return the output I intend for all possible inputs. I use a type system to prove that there does not exist an input, such that my functions will not successfully terminate (again, sidestepping the issue of non-total functions). In other words, a type checker proves the absence of certain undesirable behaviours, but it does not prove the presence of the specific desirable behaviours that I require.

Type systems are becoming more sophisticated and are capable of proving increasingly interesting properties about programs. In particular, dependently typed programming languages like Idris can be used to establish that lists are always non-empty or the parity of addition.

But unless the type system proves that there is exactly one inhabitant of a particular type, I still require a positive example to check that I've implemented the right well-typed solution. And even if the type provably has only one inhabitant, I would still likely write a unit test to help explain to myself how the abstract property enforced by the type system manifests itself.

A type system is complementary to unit tests produced by test-driven design. The presence of a type system provides additional confidence as to the correctness of a program, but as I write software it does not reduce the need for examples in the form of unit tests.

Overlapping magisteria

I've written that unit tests and acceptance tests represent two non-overlapping magisteria. I've realised I need to revise this.

Unit tests and acceptance tests specify internal and external behaviour respectively. There is no inherent reason why external behaviour should be trivially translatable to internal behaviour, because the structure of the internals need not bear any resemblance to the model the system presents to the world.

However, that is only true of systems in general. Systems produced using a domain-driven design methodology deliberately enforce structural similarity between the system's implementation and the domain it represents.

Because of this, it's possible to make inferences between external and internal properties of the system. For example, if a

LoginFailure

object returns

true

to the method

shouldLockAccount()

when its

int

field called

previousAttempts

is

2

or greater, there's a good chance that if a user thrice enters the wrong password that their account will be disabled.

If we know something about a well-designed system's external behaviour, we can generally extrapolate about its internal behaviour (and vice-versa).

Acceptance tests make big claims

If we have good acceptance tests, why do we need unit tests?

Acceptance tests tell us a lot. When they pass, they tell us things like:

• A feature works from an end-user perspective.
• All the components required to serve user requests have been wired up correctly. 
• The supporting infrastructure has been installed and configured in the test environment.
• The user interface has not significantly changed since the acceptance tests were first written.
• An intermittant network outage did not occur.

But when they fail, they tell us very little. They make such ambitious claims about the state of the software that failures could indicate a large number of disparate underlying issues.

Unit tests, on the other hand, claim very little. If a unit test fails, it is immediately obvious that there is a problem with a very specific section of code.

In general, the easier it is for a test to fail, the less it tells us when it does. Failures from tests that intermittently break for no reason at all aren't very informative. But if there's a little red dot next to that test that "couldn't possibly fail" then you've just discovered something startlingly new about your system.

Relying on acceptance tests makes sense if the code-base is relatively static, because failures will be relatively rare. But software that must change to remain valuable (i.e. almost all software) also needs fine-grained unit tests to give specific and actionable feedback on failures.

Eliot on projects without Continuous Integration

What are the roots that clutch, what branches grow
Out of this stony rubbish? Son of man,
You cannot say, or guess, for you know only
A heap of broken images, where the sun beats,
And the dead tree gives no shelter, the cricket no relief,
And the dry stone no sound of water.

- T. S. Eliot, The Waste Land

Safe habits

When I was growing up, I found some of my parents' habits irritatingly conservative. Examples included:

• Always lock doors from the outside using the key
• Always turn on the cold tap before the hot tap

The idea was that following these habits guaranteed you could never burn yourself or lock yourself out. But I found these precautions frustrating because I knew that it was unlikely that I'd forget my keys or put my hand in the scalding water.

However, I was mistaking the most likely outcome for the entire distribution. In Life's Grandeur, Stephen Jay Gould calls this "reification" - fixating on the average case and ignoring variation and atypical outcomes.

On any given occasion, my cavalier attitude would probably suffice. But sooner or later, if I locked doors by setting the snib and pulling them shut, my keys would not be in my pocket.

My parents understood my fallibility better than I did. And they were in a better position to appreciate the myriad of door-locking scenarios that would confront me over my lifetime.

That's why I like to think that if my mother were a programmer (and she'd make a good one) she would advocate TDD, which goes as follows:

1. Write a failing test
2. Write the minimum of code to pass the test
3. Refactor

If you make TDD a permanent habit then you are inevitably at most 5 or 10 minutes away from working, tested code. And you know that every bit of code you write has a corresponding test.

Be mindful of your development habits, and design them for the bad days, not the average days.

Descartes on Unit Testing

For he who attempts to view a multitude of objects with the one and the same glance, sees none of them distinctly; and similarly the man who is wont to attend to many things at the same time by a single act of thought is confused in mind.

- René Descartes, 'Rules for the direction of the mind' in Key Philosophical Writings