Builtin Types viewed as Inductive Families

TL;DR

This paper presents a method using Quantitative Type Theory to define data structures that combine runtime efficiency with compile-time invariants, enabling aggressive invariant erasure during compilation without sacrificing programming simplicity.

Contribution

It introduces a novel approach to defining invariant-rich data structures as inductive families that are efficiently erased at compile time, improving upon existing methods.

Findings

Predictable complexity of representations

Seamless programming with high-level structures

Effective invariant erasure during compilation

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.