Types As Specification

By Alex Beal
December 14, 2013

One illuminating way of looking at types is by seeing them as specifications. A function’s type, for example, is a declarative way of telling the type checker what you intend the function to do. You then supply the type checker with an implementation of the function, and the type checker ensures that the specification and the implementation match. This has clear advantages over comments or code conventions. The specification is enforced by the compiler, and therefore can never go out of date. The specification forces the programmer to think about the properties of the function at a higher level of abstraction, hopefully resulting in better design. Finally, the specification must be written in an unambiguous way, which is, of course, not the case with documentation written in English prose.¹ There are of course many other benefits to types in general, but I see these as their main benefits when used as documentation.

Seeing types as specification makes it clear why an expressive type system is so beneficial. The more precisely you can define your types, the more precise and unambiguous your specification is. This helps other programmers understand your intention, and also allows the type checker to give you stronger guarantees. In a language like Java, many abstractions which are easily and fluently expressed at the type level in other languages, can simply not be expressed. In a language like JavaScript, which can be thought of as a language where the type system enforces nothing, the type level specification for any function essentially says that this function could literally do anything. Imagine if you came across that in an API’s documentation.

Another opinion on specification sees the implementation as specification. This has been popularized by Jeff Atwood in his article Learn to Read the Source, Luke.² Although it’s certainly true that often times the documentation is out of date, and one must refer to the source to understand a program, this strikes me as a symptom of a disease–the disease of weak type systems–rather than something to be encouraged. The fact that he uses JavaScript–a language with no serious type system–as his example of this further strengthens this point. The reason this is so terrible is that it leads to tighter coupling. Consider Java interfaces, one of the nicer parts of Java, and how they decrease coupling. The idea here is to specify a generic API behind which one can hide an implementation. This, of course, decreases coupling because now implementations can be swapped in and out, but only if the implementations conform to the same API level contract. If an interface declares a sorting function, each implementation may use, e.g., mergesort or quicksort, but they must all sort the input. This seems like an obvious point, but notice that if the implementation becomes the specification, it’s no longer clear if the particular choice of sorting algorithm is part of the specification. Perhaps the interface was specifying different types of quicksorts (in place vs not in place), rather than sorting in general. This problem becomes much harder when the interfaces specify things more complex than sorting, such as hiding entire systems behind them. A type system can’t completely solve this problem, as some things are simply hard to express at the type level, but they can certainly help to alleviate the problem, and the help they can provide is proportional to their expressiveness.

Yet another school of thought sees tests as specification. Although I certainly see this as better than implementation as specification, it still suffers from several shortcomings. The first is that often times tests only specify contracts at a very shallow level. If I pass this concrete value to a function, then I expect this concrete value back. In contrast, the contract a type expresses is much more general, operating on classes of values rather than specific values. Properties based testing like QuickCheck³ can help to alleviate this, but it’s far from mainstream, and still doesn’t address the second shortcoming, that tests are imperative while types are declarative.⁴ When writing tests, I must describe to the computer how to generate a value, how to set up the test environment, how to call the function under test, and how to verify that the return is correct. This is not the case for types, where I can simply declare the property and let the type system produce a proof. This isn’t completely fair, though, as some properties are difficult to express at the type level, even in languages with expressive type systems, which is why I see these two types of specifications as complementing one another. What I can’t understand is choosing a language with no type system, and then having this burden fall on tests, coding conventions, and comments. Ultimately, I see this as one of my greatest frustrations with programming–the number of useful techniques and tools that are simply untapped.