Generic Zero-Cost Reuse for Dependent Types

TL;DR

This paper presents a zero-cost approach to code reuse in dependently typed languages by leveraging Curry-style type theory, enabling seamless reuse of data and programs without runtime overhead.

Contribution

It introduces a novel method for dependently typed reuse that exploits Curry-style type theory to achieve zero-cost, generic programming solutions.

Findings

Reuses data and programs at zero runtime cost

Internalizes reuse as identity function in Curry-style theory

Addresses code duplication in dependently typed languages

Abstract

Dependently typed languages are well known for having a problem with code reuse. Traditional non-indexed algebraic datatypes (e.g. lists) appear alongside a plethora of indexed variations (e.g. vectors). Functions are often rewritten for both non-indexed and indexed versions of essentially the same datatype, which is a source of code duplication. We work in a Curry-style dependent type theory, where the same untyped term may be classified as both the non-indexed and indexed versions of a datatype. Many solutions have been proposed for the problem of dependently typed reuse, but we exploit Curry-style type theory in our solution to not only reuse data and programs, but do so at zero-cost (without a runtime penalty). Our work is an exercise in dependently typed generic programming, and internalizes the process of zero-cost reuse as the identity function in a Curry-style theory.