Builtin types viewed as inductive families

Allais, Guillaume; Wies, Thomas, ed. (2023) Builtin types viewed as inductive families. In: Programming Languages and Systems. ESOP 2023. Lecture Notes in Computer Science, 13990 . Springer, FRA, pp. 113-139. ISBN 9783031300448 (https://doi.org/10.1007/978-3-031-30044-8_5)

[thumbnail of Allais-LNCS-2023-Builtin-types-viewed-as-inductive]
Preview
 Text. Filename: Allais_LNCS_2023_Builtin_types_viewed_as_inductive.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (605kB)| Preview

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.

CORE (COnnecting REpositories)