License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2021.9
URN: urn:nbn:de:0030-drops-140527
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14052/
Go to the corresponding LIPIcs Volume Portal

Brady, Edwin

Idris 2: Quantitative Type Theory in Practice

pdf-format:
LIPIcs-ECOOP-2021-9.pdf (0.9 MB)

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.

BibTeX - Entry

@InProceedings{brady:LIPIcs.ECOOP.2021.9,
  author =	{Brady, Edwin},
  title =	{{Idris 2: Quantitative Type Theory in Practice}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{9:1--9:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14052},
  URN =		{urn:nbn:de:0030-drops-140527},
  doi =		{10.4230/LIPIcs.ECOOP.2021.9},
  annote =	{Keywords: Dependent types, linear types, concurrency}
}

Keywords: Dependent types, linear types, concurrency
Collection: 35th European Conference on Object-Oriented Programming (ECOOP 2021)
Issue Date: 2021
Date of publication: 06.07.2021
Supplementary Material: Software (ECOOP 2021 Artifact Evaluation approved artifact): https://doi.org/10.4230/DARTS.7.2.10

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI