Abstract

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.

Bio

Edwin is a Lecturer in Computer Science at the University of St Andrews in Scotland, interested in type-driven development, domain specific languages and reasoning about effectful programs. When he’s not doing that, he might be playing Go, watching cricket, or wandering around Scotland’s countryside.