Builtin types viewed as inductive families

Guillaume Allais*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication32nd 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
EditorsThomas Wies
PublisherSpringer
Pages113–139
Number of pages32
ISBN (Electronic)9783031300448
ISBN (Print)9783031300431
DOIs
Publication statusPublished - 18 Apr 2023
Event32nd European Symposium on Programming, ESOP 2023 - Paris, France
Duration: 22 Apr 202327 Apr 2023
Conference number: 32
https://etaps.org/2023/cfp/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume13990
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference32nd European Symposium on Programming, ESOP 2023
Abbreviated titleESOP
Country/TerritoryFrance
CityParis
Period22/04/2327/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.

Cite this