Introduction to Type-Driven Development with Rust
The aim of this blog post is to examine type-driven development with Rust. Type-driven development is an approach to develop robust and verified software, using a type system. The first section gives a brief overview of a type system.
What is a type system?
A type system is defined in the “Types and Programming Languages” as follows.
A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.
It allows early detection of some programing errors and helps us to build robust software.
What is a Type-driven development?
Dr. Edwin Brady used the term ‘Type-driven development’ in the “Type-Driven Development with Idris”:
Type-driven development is a style of programming in which we write types first and use those types to guide the definition of functions.
The procedures of applying it are as follows:
- Write the input and output types.
- Define the function, using the structure of the input types to guide the implementation.
- Refine and edit the type and function definition as necessary.
I rewrote a part of the fourth chapter in the “Type-Driven Development with Idris” with Rust. Idris has a future of holes, functions started with ‘?’, but Rust doesn’t have it. Therefore I used todo!() , which stand for parts of programs that are yet to be written.
Here is an example program using an enumerated type:
We can express a direction in code by defining a Direction enumeration and listing the possible kinds a direction can be, North, East, South, and West.
Type
Write a function type with Direction as the input and output, and then create a skeleton definition:
Define
Define the function by the pattern matching a parameter, direction:
The Rust compiler checks exhaustiveness, so it demands that you have a match arm for every variant of the enum.
Refine
Fill in ToDo’s on the right sides:
This simple example shows that we’ll add new types and functions, guided by the Rust type system.
