Idris 2 is a functional programming language with dependent types, based on Quantitative Type Theory. It is implemented in Idris 2, which means we can take advantage of the expressive type system to guarantee properties of aspects of the implementation. In this talk, I will describe some of the most valuable lessons learned from implementing a dependently typed language in itself, and report on progress on a new core language for Idris 2, Yaffle.

Reader in Computer Science at the University of St Andrews