Expressive types, not oppressive types

Uncle Bob wrote a recent post in which he warns programmers against the "dark path" some modern languages have taken - that is to "double down" on static typing. He cites Swift and Kotlin as examples, though his argument is meant to be interpreted more generally.

I share many points of view in common with Uncle Bob. I find the dynamically typed Clojure programming language beautiful and expressive - most of my personal projects are written in Clojure. I think that TDD (test-driven design) is a valuable and important discipline - I work for an agile consulting company where most of our projects include helping clients to get better at testing.

But I disagree strongly with the way Uncle Bob frames this discussion on static types.

Uncle Bob looks at advanced type systems and sees them as more oppressive rather than more expressive. Being able to describe whether or not a function can return null is an opportunity, not a constraint. Being able to use types to describe your code's intent is an opportunity, not a constraint. Being able to reason about the behaviour of a function based on its type signature is an opportunity, not a constraint.

The kicker is that this is almost exactly the fallacy about TDD that we have railed against for years. We call it "test-driven design" because we know that evolving code in response to examples is a great way to inform a design. Folks who have not learnt to listen to their unit tests see them as nagging constraints that prevents them from writing code in the way they'd like. A master of TDD uses tests as feedback for their design.

Anyone who sees unit test as mere "checks" that make changing code needlessly difficult isn't getting the most out of test-driven design. Anyone who sees static types as mere "checks" that make changing code needlessly difficult isn't getting the most out of type-driven design.

Based on his post Uncle Bob falls into the latter category. He sees types as ad hoc antidotes for specific mistakes rather than tools for thought - "Every time there’s a new kind of bug, we add a language feature to prevent that kind of bug."

If that's Uncle Bob's experience of Swift and Kotlin, he should try Elm. Or F#. Or Haskell. If his experience is anything like mine, he would find that more sophisticated types lead to less ad hockery, not more.

In a follow-up post, Uncle Bob is explicit about what he wants in a programming language - "There is a balance point after which every step down The Dark Path increases the cost over the benefit. I think Java and C# have done a reasonable job at hovering near the balance point."

I couldn't disagree more. Java and C# have two of the most onerous and least beneficial type systems. Their complexity and absence of type inference force excessive bookkeeping on the programmer. They lack of basic features like sum types, which denies the programmer an important expressive idiom.

Java and C# represent the nadir of the type system trade-off, not the zenith. Type systems are tools. Better tools help us write better code. We should welcome each and every advance in the tools we use to do our job, because frankly we could do a lot better than what we have now.

To argue that employing more expressive types is a "dark path" that leads developers away from personal responsibility isn't accurate or helpful.

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.