Abstract
State of the art optimisation passes for dependently typed languages can help
erase the redundant information typical of invariant-rich data structures and
programs. These automated processes do not dramatically change the structure of the data, even though more efficient representations could be available.
Using Quantitative Type Theory, we demonstrate how to define an invariant-rich,
typechecking time data structure packing an efficient runtime representation
together with runtime irrelevant invariants. The compiler can then aggressively
erase all such invariants during compilation.
Unlike other approaches, the complexity of the resulting representation is
entirely predictable, we do not require both representations to have the
same structure, and yet we are able to seamlessly program as if we were
using the high-level structure.
erase the redundant information typical of invariant-rich data structures and
programs. These automated processes do not dramatically change the structure of the data, even though more efficient representations could be available.
Using Quantitative Type Theory, we demonstrate how to define an invariant-rich,
typechecking time data structure packing an efficient runtime representation
together with runtime irrelevant invariants. The compiler can then aggressively
erase all such invariants during compilation.
Unlike other approaches, the complexity of the resulting representation is
entirely predictable, we do not require both representations to have the
same structure, and yet we are able to seamlessly program as if we were
using the high-level structure.
Original language | English |
---|---|
Title of host publication | Programming Languages and Systems |
Subtitle of host publication | 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings |
Editors | Thomas Wies |
Publisher | Springer |
Pages | 113–139 |
Number of pages | 32 |
ISBN (Electronic) | 9783031300448 |
ISBN (Print) | 9783031300431 |
DOIs | |
Publication status | Published - 18 Apr 2023 |
Event | 32nd European Symposium on Programming, ESOP 2023 - Paris, France Duration: 22 Apr 2023 → 27 Apr 2023 Conference number: 32 https://etaps.org/2023/cfp/ |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 13990 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 32nd European Symposium on Programming, ESOP 2023 |
---|---|
Abbreviated title | ESOP |
Country/Territory | France |
City | Paris |
Period | 22/04/23 → 27/04/23 |
Internet address |
Keywords
- Runtime representation
- Idris 2
- Quantitative Type Theory
- Indexed families
Fingerprint
Dive into the research topics of 'Builtin types viewed as inductive families'. Together they form a unique fingerprint.Datasets
-
Builtin Types viewed as Inductive Families (code)
Allais, G. (Creator), University of St Andrews, 24 May 2023
DOI: 10.17630/bd1085ce-a462-4a8b-ae81-9ededb4aea21
Dataset: Software
File