Programming as Conversation: Type-Driven Development in Action

Lead Research Organisation: University of St Andrews
Department Name: Computer Science


This project aims to improve the program development process, using a process of "Type-driven Development". We believe that in order to enable the highest levels of productivity, programming should be a conversation between the programmer and the machine. In type-driven development, we begin by giving a type as a plan for a program. Then the machine, rather than being seen as an adversary which rejects incomplete or incorrect programs, is the programmer's assistant. A limited form of this idea exists in modern integrated development environments: when typing "x." into a text buffer, the environment will show with methods "x" implements. This project will take this idea several steps further. Not only can we give feedback on partial programs, we can also use types and their structure to generate significant parts of a program and direct the implementation of more complex components such as communication and security protocols.

During development, programs spend most of their time in an incomplete state, and the act of programming is as much about the steps required to achieve a complete program as it is about the end result. Accordingly, language implementations and tools must support the editing process as well as check and compile the end result. In this project, we will develop the necessary tooling to support interactive type-driven development, based on sound theoretical foundations. Furthermore, we will make the tooling itself programmable: the foundations will essentially give a language of programming "tactics", which will be composable intro sophisticated methods for automatic program construction, directed by the type. We will liaise with industry throughout to ensure that the techniques we develop are well-suited to commercially relevant problems.

Planned Impact

In the course of the project, we will make significant advances in the state of the art of dependently typed programming, improving the available tools and developing new libraries and programming idioms. As well as benefitting academic researchers in the field of software verification, it will benefit the wider community of application developers by providing tools to improve programmer productivity.

This project will itself contribute to a longer term vision of fully verified systems infrastructure, thus the public at large will benefit from techniques which enable the development of stable, robust software at reduced cost. We are collaborating with companies and research institutions who may make use of the results of this project, In particular, we will be working with PIK, the Potsdam Institute for Climate Impact Research, who have been using Idris for several years for formalising economic models related to climate change, and who will benefit from the increased productivity offered by this project. We are also working with developers at Facebook, who develop large scale systems in Haskell, another language with a sophisticated type system which will benefit from type-driven interactive programming techniques. Finally, our contacts at Galois, Inc, in Portland, Oregon, are using Haskell and domain specific language technology to build tools for guaranteed confidentiality including secure voting systems. By liasing with these companies, we will be able to direct the research towards supporting socially and commercially important problems. We will also liaise with Microsoft Research, where researchers are developing GHC (the de facto standard Haskell compiler), in order to make our techniques usable by Haskell programmers, as well as in our own Idris compiler.

The project will involve development of a new, self-hosted, version of the Idris programming language ( As with all code released as part of the Idris system so far, everything produced during the project will be released under an Open Source licence, and made available via GitHub ( and the project web site. Throughout the project we will hold a series of open "Idris Developer Meetings" (following an earlier series in 2013-2015) to allow project contributors and others to work closely with the project team.

To help make the results of the project accessible to a wider audience of application developers (the most likely primary users of the project's results) we will continue to present workshops and tutorials alongside developer conferences such as Strange Loop, Code Mesh, and others. These workshops will give developers a hands-on opportunity to try type-driven development tools, with close support from the project team. These workshops will be made more effective with the support of the recently published book "Type-driven Development with Idris", which sets out some of the ideas which are the foundation of this project.


10 25 50
Description We have implemented a new version of the Idris programming language, which supports interactive program development. We have developed several new methods for improving compiler performance, and for type-driven program synthesis, meaning that there is much improved interactivity and feedback from the machine to help programmers. We have used this to develop new techniques for automated theorem proving, which will give increased confidence in program correctness. We have papers in preparation/currently under review about the implementation and theorem proving techniques.
Exploitation Route The Idris system is open source, with an active community, and available for use by software practitioners. The tools and methods we develop will therefore be directly applicable in industry.
Sectors Digital/Communication/Information Technologies (including Software)

Title Idris 2 
Description A programming language designed to encourage Type-Driven Development. 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. In Idris, types are first-class constructs in the langauge. This means types can be passed as arguments to functions, and returned from functions just like any other value, such as numbers, strings, or lists. This is a small but powerful idea, enabling: relationships to be expressed between values, for example that two lists have the same length; assumptions to be made explicit and checked by the compiler, for example if you assume that a list is non-empty, Idris can ensure this assumption always holds before the program is run; if desired, properties of program behaviour to be formally stated and proven. Idris is actively developed as part of this project, including the core language itself, interactive development tools (including support for the Language Server Protocol) and libraries. We are currently using it to develop Frex, a library for automatic equational reasoning (paper under review). 
Type Of Technology Software 
Year Produced 2021 
Open Source License? Yes  
Impact Some commercial usage (notably by Statebox and ONAI as well as several industry conference talks and a book (, >6000 sales) 
Description Lambda Days 2021 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Industry/Business
Results and Impact Software industry conference talk
Year(s) Of Engagement Activity 2021
Description Rebase 2020 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Industry/Business
Results and Impact Conference talk crossing between academia and industry
Year(s) Of Engagement Activity 2020