Introduction to Type-Driven Development with Rust

Photo by Adam Birkett on Unsplash

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:

  1. Write the input and output types.
  2. Define the function, using the structure of the input types to guide the implementation.
  3. 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.

References

--

--

--

Software engineer

Love podcasts or audiobooks? Learn on the go with our new app.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Takanori Ishibashi

Takanori Ishibashi

Software engineer

More from Medium

Web Application Programming in PicoLisp: Prefix Classes

Fusion Powered Strings!

Rust: Bigger Building Blocks — Intro to Structs

Image by: Polina Kholodova, from pexels.com

Implementing Standard Algorithms in Rust: Merge Sort, Quick Sort