Type-driven development

Type-Driven Development with Idris

Name:

The name “type-driven development” suggests an analogy to test-driven development. There’s a similarity, in that writing tests first helps establish a program’s purpose and whether it satisfies some basic requirements. The difference is that, unlike tests, which can usually only be used to show the presence of errors, types (used appropriately) can show the absence of errors. But although types reduce the need for tests, they rarely eliminate it entirely. …

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 overall process is to write the necessary data types, and then, for each function, do the following:

  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.

…

In type-driven development, instead of thinking of types in terms of checking, with the type checker criticizing you when you make a mistake, you can think of types as being a plan, with the type checker acting as your guide, leading you to a working, robust program. Starting with a type and an empty function body, you gradually add details to the definition until it’s complete, regularly using the compiler to check that the program so far satisfies the type. Idris, as you’ll soon see, strongly encourages this style of programming by allowing incomplete function definitions to be checked, and by providing an expressive language for describing types.

Types as models:

When you write a program, you’ll often have a conceptual model in your head (or, if you’re disciplined, even on paper) of how it’s supposed to work, how the components interact, and how the data is organized. This model is likely to be quite vague at first and will become more precise as the program evolves and your understanding of the concept develops.

Types allow you to make these models explicit in code and ensure that your implementation of a program matches the model in your head. Idris has an expressive type system that allows you to describe a model as precisely as you need, and to refine the model at the same time as developing the implementation.

The process of type-driven development:

You can characterize type-driven development as an iterative process of type, define, refine: writing a type, implementing a function to satisfy that type, and refining the type or definition as you learn more about the problem.

With matrix addition, for example, you do the following:

  • Type: Write a Matrix data type, and use it as the input and output types for an addition function.
  • Define: Write an addition function that satisfies its input and output types.
  • Refine: Notice that the input and output types for your addition function allow you to give invalid inputs with different dimensions, and then make the type more precise by including the dimensions of the matrices.

Incomplete definitions - working with holes:

Idris functions themselves can contain holes, and a function with a hole is incomplete. Only a value of an appropriate type will fit into the hole, just as a square shape will only fit into a square hole in the shape sorter. Here’s an incomplete implementation of the “Hello, Idris World!” program:

module Main
main : IO ()
main = putStrLn ?greeting

The syntax ?greeting introduces a hole, which is a part of the program yet to be written.

Tools

2025 © ak