Types + Properties = Software by Mark Seemann
Combine a strong type system with Property-Based Testing to specify software.
When Kent Beck rediscovered Test-Driven Development (TDD) some twenty years ago, the original context was SmallTalk programming. When the concept of TDD began to catch on, it seemed to me to proliferate particularly in dynamic language communities like Python and Ruby.
It makes sense that if you can't get fast feedback from a compilation step, you seek another way to get feedback on your work. Unit testing is such a fast feedback mechanism. Watching the NodeJS community from the side, it always seemed to me that TDD is an integral way of working with that stack. This makes sense.
This also explains why e.g. C# programmers were more reluctant to adopt TDD. That your code compiles gives a smidgen of confidence.
C# and Java programmers may joke that if it compiles, it works, but also realise that that's all it is: a joke. Automated testing adds another layer of safety on top of compilation. On the other hand, you may get by with writing fewer tests than in a dynamic language, because the static type system does provide some guarantees.
What if you had a stronger type system than what C# or Java provides? Then you'd have to write even fewer tests.
Type spectrum #
It can be useful to think about typing as a spectrum.
To the left, we have dynamically typed languages like JavaScript and Ruby. Python can be compiled, and Clojure is compiled, so we can think of them as being a little closer to the middle. Purists would want to point out that whether or not a language is compiled and how statically typed it is are two independent concerns, but the point of this spectrum is to illustrate the degree of confidence the type system gives you.
Java and C# are statically typed, compiled languages, but a lot of things can still go wrong at run-time. Just consider all the null pointer exceptions you've encountered over the years.
Further to the right are languages with Hindley–Milner type systems, such as F# and Haskell. These offer more safety from static typing alone. Such types are the subject of this and future articles.
I've put Haskell a bit to the right of F# because it has higher-order types. To the right of Haskell sits dependently-typed languages like Idris. To the far right, we have a hypothetical language with such a strong type system that, indeed, if it compiles, it works. As far as I'm aware, no such language exist.
Creating software with Hindley-Milner type systems #
It turns out that when you shift from a Java/C#-style type system to the stronger type system offered by F# or Haskell, you can further shift your design emphasis towards designing with types. You still need to cover behaviour with automated tests, but fewer are necessary.
With the algebraic data types available in F# or Haskell, you can design your types so that illegal states are unrepresentable. In other words, all values of a particular type are guaranteed to be valid within the domain they model. This makes it much easier to test the behaviour of your system with Property-Based Testing, because you can declaratively state that you want your Property-Based Testing framework (FsCheck, QuickCheck, etc.) to provide random values of a given type. The framework will give you random values, but it can only give you valid values.
In this series of articles, you'll see an example of this in F#:
- Types + Properties = Software: designing with types
- Types + Properties = Software: state transition properties
- Types + Properties = Software: properties for the advantage state
- Types + Properties = Software: properties for the Forties
- Types + Properties = Software: composition
- Types + Properties = Software: initial state
- Types + Properties = Software: finite state machine
- Types + Properties = Software: other properties
Summary #
The stronger a language's type system is, the more you can use static types to model your application's problem domain. With a sufficiently strong type system, you can make illegal states unrepresentable. While states are guaranteed to be legal, transitions between states need not be. You can often use Property-Based Testing to ensure that the state transitions are correct. The combination of types and properties give you a simple, but surprisingly powerful way of specifying the behaviour of the software you create.
