Idris 2: Quantitative Type Theory in Action

Thu 27 February 2020

Filed under Posts

Tags idris paper

A new draft is available, describing the design of Idris 2 and some of the things you can do in a language based on Quantitative Type Theory (beyond the brief introduction I give here.)

Idris 2: Quantitative Type Theory in Action

Abstract: Dependent types allow us to express precisely what a function is intended to do. Recent work on Quantitative Type Theory (QTT) extends dependent type systems with linearity, also allowing precision in expressing when a function can run. This is promising, because it suggests the ability to design and reason about resource usage protocols, such as we might find in distributed and concurrent programming, where the state of a communication channel changes throughout program execution. As yet, however, there has not been a full-scale programming language with which to experiment with these ideas. Idris 2 is a new version of the dependently typed language Idris, with a new core language based on QTT, supporting linear and dependent types. In this paper, we introduce Idris 2, and describe how QTT has influenced its design. We give several examples of the benefits of QTT in practice including: clearly expressing which data is erased at run time, at the type level; improving interactive program development by reducing the search space for type-driven program synthesis; and, resource tracking in the type system leading to type-safe concurrent programming with session types.


Edwin Brady © Edwin Brady Powered by Pelican and Twitter Bootstrap. Icons by Font Awesome and Font Awesome More