Builtin types viewed as inductive families

Guillaume Allais

doi:10.1007/978-3-031-30044-8_5

Builtin types viewed as inductive families

Guillaume Allais

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

1 Citation (Scopus)

47 Downloads (Pure)

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 as implemented in Idris 2, 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. ESOP 2023
Editors	Thomas Wies
Place of Publication	Cham, Switzerland
Publisher	Springer
Pages	113-139
Number of pages	27
Volume	13990
ISBN (Electronic)	9783031300448
ISBN (Print)	9783031300431
DOIs	https://doi.org/10.1007/978-3-031-30044-8_5
Publication status	Published - 17 Apr 2023
Event	European Symposium on Programming - Sorbonne Université, Paris, France Duration: 22 Apr 2023 → 27 Apr 2023 Conference number: 32

Publication series

Name	Lecture Notes in Computer Science
Volume	13990 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	European Symposium on Programming
Abbreviated title	ESOP 2023
Country/Territory	France
City	Paris
Period	22/04/23 → 27/04/23

Funding

This research was funded by the Engineering and Physical Sciences Research Council (grant number EP/T007265/1).

Keywords

quantitative type theory
indexed families
runtime representation
Idris 2

Access to Document

10.1007/978-3-031-30044-8_5Licence: CC BY 4.0

Allais-LNCS-2023-Builtin-types-viewed-as-inductiveFinal published version, 592 KBLicence: CC BY 4.0

European Symposium on Programming
Allais, G. (Speaker)
22 Apr 2023 → 27 Apr 2023
Activity: Presenting or Organising an Event › Participation in conference

Cite this

@inproceedings{4baa8b63714244adbb2675f4ec21e6cd,

title = "Builtin types viewed as inductive families",

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 as implemented in Idris 2, 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.",

keywords = "quantitative type theory, indexed families, runtime representation, Idris 2",

author = "Guillaume Allais",

year = "2023",

month = apr,

day = "17",

doi = "10.1007/978-3-031-30044-8\_5",

language = "English",

isbn = "9783031300431",

volume = "13990",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "113--139",

editor = "Thomas Wies",

booktitle = "Programming Languages and Systems. ESOP 2023",

address = "Switzerland",

note = "European Symposium on Programming, ESOP 2023 ; Conference date: 22-04-2023 Through 27-04-2023",

}

TY - GEN

T1 - Builtin types viewed as inductive families

AU - Allais, Guillaume

N1 - Conference code: 32

PY - 2023/4/17

Y1 - 2023/4/17

N2 - 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 as implemented in Idris 2, 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.

AB - 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 as implemented in Idris 2, 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.

KW - quantitative type theory

KW - indexed families

KW - runtime representation

KW - Idris 2

U2 - 10.1007/978-3-031-30044-8_5

DO - 10.1007/978-3-031-30044-8_5

M3 - Conference contribution book

SN - 9783031300431

VL - 13990

T3 - Lecture Notes in Computer Science

SP - 113

EP - 139

BT - Programming Languages and Systems. ESOP 2023

A2 - Wies, Thomas

PB - Springer

CY - Cham, Switzerland

T2 - European Symposium on Programming

Y2 - 22 April 2023 through 27 April 2023

ER -

Builtin types viewed as inductive families

Abstract

Publication series

Conference

Funding

Keywords

Access to Document

Fingerprint

Activities

European Symposium on Programming

Cite this