We’ve been having lots of fun over the last couple of years investigating the possibilities and limitations of type-driven development in Idris. As we write larger programs, though, we’re finding the implementation of Idris is showing the strain - such is the nature of “research quality software” - and recently I decided the time was right to start again, and implement Idris 2 in Idris. In this talk, I’ll give an introduction to type-driven development (in Idris 2) and report on progress so far, showing off the most interesting features which the new design enables (notably, linear types and better type inference). I will show what is possible with modern type systems, and share what I’ve learned by implementing a larger system using type-driven development - including where it has worked well and where it has worked less well. I also aim to convince the audience that a modern sophisticated type system doesn’t have to be hard to use, and suggest ways in which people can contribute to the new implementation of Idris.

Lecturer in Computer Science at the University of St Andrews