Thu 01 April 2021

Filed under Posts

Tags idris

A new paper, to appear at ECOOP 2021. 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 examples of the benefits of QTT in practice including: expressing which data is erased at run time, at the type level; and, resource tracking in the type system leading to type-safe concurrent programming with session types.

I will post a revised version, updated with referee's suggestions (thanks to them!) soon.


Mon 25 May 2020

Filed under Posts

Tags idris

I've just released a new version of Idris 2, which is a significant release in that it's the first one which is able to compile itself. Thus, it's the first one where we can really see how the performance of Idris 2 improves on the performance of Idris 1.

A …

Read More

Thu 27 February 2020

Filed under Posts

Tags idris paper

A paper on Idris 2 and QTT

Read More

Fri 10 January 2020

Filed under Posts

Tags idris

A discussion on erasure and linearity in Idris 2

Read More

Thu 09 January 2020

Filed under Posts

Tags meta

I've moved here from wordpress, because I wanted a nice simple static site that lives on a domain that's under my control. Also, for uninteresting reasons, I can't log in to my old site anyway...

Read More

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