Idris is a functional programming language with first-class types, which means that properties can be stated and verified at compile time. It encourages interactive type-driven development, so that programming becomes a conversation with the machine. We have recently been implementing a new version, Idris 2, with a new core language based on Quantitative Type Theory (QTT). Idris 2 therefore supports linear types, allowing programmers to be precise not only about *what* a program can do, but also *when* it is allowed to do it.
In this talk I will cover recent developments in Idris 2. In particular, I will describe how the quantities in the type system give a new level of expressivity, and show how these can be used to implement state machines, communicating systems, and verify their properties, interactively.
Watch the full talk below:
Edwin Brady is a Reader in Computer Science at the University of St Andrews, interested in making state of the art programming language techniques accessible to sofware developers and practitioners. This involves type theory, dependently typed functional programming, compilers and metaprogramming. He is currently working on a new implementation of Idris, a dependently typed functional programming language. When he’s not doing that, you might find him playing Go (he's about 2 kyu), walking up a hill, watching a game of cricket.
