“Type-Driven” is a pretty cool-sounding name, but I cannot take all the credit for it. In this post I discuss some of the history behind the name, and how it is related to our philosophy of writing software.
Background: Test-Driven Development (TDD)
Test-Driven Development (TDD) is a methodology for developing software in which writing tests comes before writing the implementation. This may seem counter-intuitive at first, but the idea is simple: code should be written for a purpose, and that purpose typically takes the form of some “business requirements” on the functionality; we can codify these requires as test cases for our code before the implementation is done, then we know once all the tests pass that the software is able to fulfil its purpose (as it has been specified up until that point).
Phrased another way, programming can be thought of the art of turning business requirements (typically specified in natural language) into something that is executable by a computer. In TDD the translation of requirements into code is direct (requirements become test cases) and happens immediately. This ensures the final product will in fact meet all its requirements. Moreover, all the code is already covered by tests, which means developers can have confidence in maintaining the correctness of the code in any future refactoring that is required.
An additional benefit of TDD is that the code is typically minimal, or as simple as possible, in some sense. This is because the developer has a clear goal in mind to write an implementation which makes the tests pass and nothing more (potentially avoiding issues of scope creep, unnecessary abstraction or premature optimization). Simpler code is often better because it reduces the development time and typically is easier to maintain in the future.
Of course, TDD in practice is not as easy as it sounds. Translating business requirements into adequate tests can be challenging. I say “adequate” here because there are many implicit assumptions that can go into a simply natural language specification. As a simple example, consider the business requirement “the user must be able to enter a phone number.” One could try to capture this as a test case where it simply checks that the input "1-800-867-5309" passes, but this would be inadequate. What should happen if the input is too short or too long to be a phone number? What is supposed to happen on input that includes letters? Is it an invalid phone number, or should we convert to numbers using a mapping like a, b, c go to 1; d, e, f go to 2; etc? These questions would need to be clarified and the test case would need to cover all these cases and more. In fact, this would be a good candidate for fuzzing, but that’s a topic for another time.
The point here is that the software produced by TDD is only as good as the tests which were derived from the business requirements and this can be done more or less well. But we can do better, we can have more than just tests, we can have types!
Type-Driven Development (TyDD)
Edwin Brady is a Reader in the department of Computer Science at the University of St Andrews in the UK. He coined the phrase Type-Driven Development (TyDD) as a riff on TDD. The core principle is still the same: we want to translate business requirements into some form of code. But in this case we want to turn the requirements into types instead of tests. Brady works on a programming language called Idris which is meant to encourage this programming methodology. Here is a quote from the front page of its website
In type-driven development, types are tools for constructing programs. We treat the type as the plan for a program, and use the compiler and type checker as our assistant, guiding us to a complete program that satisfies the type. The more expressive the type is that we give up front, the more confidence we can have that the resulting program will be correct.
Edwin Brady (https://www.idris-lang.org/ accessed 2022-08-31)
As with TDD, some find TyDD an unintuitive idea at first. How can types be used to plan out a program? Aren’t they just tags like String or Int to say what kind of data there is? But types can be so much more than that. Certainly primitives types like numbers or Boolean values are the starting point, but these can be combined to create more complex types like tuples (product types), enumerations (sum types), function types (A → B), and more. In fact, the Curry-Howard correspondence tells us that if we have a sufficiently expressive type system then any theorem of constructive logic can be written as a type, and a proof of that theorem is an implementation of a program satisfying that type. A type system like this can be used to capture business logic faithfully, hence the concept for TyDD.
This mathematical foundation for TyDD gives an additional benefit over TDD in that we have help in writing an implementation of our program once we have specified the types. The Curry-Howard correspondence says that types are theorems and programs are proofs. We have other software that is able to generate proofs of theorems (see, for example, Z3), therefore we can view our types as theorems, ask a theorem prover to generate a proof for us, and in turn view this as an implementation of our program. In this way, the computer is actually helping us write correct code. This may differ from the experience of some developers where they view the compiler as an antagonist that just yells at them when they do something wrong. Viewing the compiler as your assistant rather than your enemy makes for a more pleasant and more productive coding experience.
In general, types are better than tests for capturing requirements because they naturally must cover all edge cases, whereas tests only cover what is explicitly written down. Returning to the phone number example, we might define a PhoneNumber type and a function fn parse_phone_number(input: String) -> PhoneNumber. But a theorem prover would fail to find an implementation for such a function because of the ambiguities we mentioned earlier. Therefore we might refine the type to look something like fn parse_phone_number(input: String) -> Result<PhoneNumber, ParseError>, where ParseError is a new type we must define (and therefore codify what the error conditions are). A programming language like Idris allows us to be even more specific in our type definitions because it allows including information like exactly how many digits can be in each part of the phone number (e.g. 1 to 3 digits for the country code, followed by 10 digits for the number). As it says in the quote on the Idris website, the more detail we include in our type definitions, the more certainty we have that our program is correct, and the easier of a time a theorem prover will have writing our program for us. As the developer, we can continue to refine our types as we write the program based on the feedback from a theorem prover.
The phone number example is a silly one because in a real project you would use a library (or copy a regex from somewhere) to not have to worry about the edge cases yourself. But the purpose of this example is to illustrate the ideas of TDD and TyDD at an accessible level. As an exercise, think of a project you worked on recently, how could TyDD have been applied to lead to a better final product?
As with TDD, TyDD is not always easy in practice. It can still be challenging to capture complex business requirements sufficiently accurately using a given type system. But the more practice one has with this kind of translation, the easier it becomes. And it doesn’t hurt to hire an expert to help you *wink* *wink*.
Software Development at Type-Driven Consulting
At Type-Driven Consulting, we believe in TyDD, but still recognize that languages like Idris are not yet ready to appear in production codebases. We take a practical approach which is a hybrid of TDD and TyDD where we always strive to write as precise types as possible in the programming language we are working with, and backing up any holes in the type specification with tests. Rust is our preferred programming language because we believe it strikes a good balance between having a strong type system while being a practical systems programming language that is suitable for production environments.
We also recognize that code is read (and modified) much more often than it is written. Therefore we always strive for code that is clean, and maintainable. The TDD and TyDD methodologies lend themselves to making especially maintainable code because it tends to involve many small pieces (each of which is easy to read) that are composed together, and all backed by tests to ensure correctness.
All that said, I would love to see languages with dependent types (like Idris) move more into mainstream programming. My personal view is that programming is hard, humans are kind of bad at it, and computers (read math) can help us.
Get in touch with us with us today to have Type-Driven Consulting involved in your next software project, or to learn more about software development principles.
Pingback: Type-Driven Ethics – Type-Driven Consulting