Custom Representations of Inductive Families

TL;DR

This paper introduces a language with dependent types and customizable inductive family representations that optimize runtime performance and enable reasoning about data representations, improving upon default linked-tree approaches.

Contribution

It presents a novel approach to inductive family representations with guarantees of no runtime traces, supporting optimizations and reasoning through a dependently typed language.

Findings

Representation guarantees no runtime traces

Supports optimization techniques like GMP-style big integers

Enables reasoning about data representations with dependent types

Abstract

Inductive families provide a convenient way of programming with dependent types. Yet, when it comes to compilation, their default linked-tree runtime representations, as well as the need to convert between different indexed views of the same data, can lead to unsatisfactory runtime performance. In this paper, we introduce a language with dependent types, and inductive families with customisable representations. Representations are a version of Wadler's views, refined to inductive families like in Epigram, but with compilation guarantees: a represented inductive family will not leave any runtime traces behind, without relying on heuristics such as deforestation. This way, we can build a library of convenient inductive families based on a minimal set of primitives, whose re-indexing and conversion functions are erased during compilation. We show how we can express optimisation techniques such as representing Nat-like types as GMP-style big integers, without special casing in the compiler. With dependent types, reasoning about data representations is also possible through a provided modality. This yields computationally irrelevant isomorphisms between the original and represented data.