Idris 2: Quantitative Type Theory in Action

Resource | v1 | created by jjones |
Type Paper
Created 2020-02-27
Identifier arXiv:2104.00480


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; ...


about Idris

Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and...

referenced in A Crash Course in Idris 2

This is a crash course in Idris 2 (sort of a tutorial, but rather less gentle I’m afraid!). It provid...

Edit details Edit relations Attach new author Attach new topic Attach new resource
0.0 /10
useless alright awesome
from 0 reviews
Write comment Rate resource Tip: Rating is anonymous unless you also write a comment.
Resource level 0.0 /10
beginner intermediate advanced
Resource clarity 0.0 /10
hardly clear sometimes unclear perfectly clear
Reviewer's background 0.0 /10
none basics intermediate advanced expert
Comments 0
Currently, there aren't any comments.