Generic Zero-Cost Reuse for Dependent Types

Larry Diehl, Denis Firsov, Aaron Stump
3/21/2018
cs.PL

Official code: larrytheliquid/generic-reuse (6 stars, MIT, last commit 2018-10-05).

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.

View on arXivView PDF

Code Implementations(1)

larrytheliquid/generic-reuseOfficial100%
MIT

Source code accompanying the draft paper "Generic Zero-Cost Reuse for Dependent Types"

60TeX, MakefileMar 23, 20188 years agoMIT

Similar Papers

Really Natural Linear Indexed Type Checking

78% match1 repo332015

A Machine-checked proof of Birkhoff's Variety Theorem in Martin-Löf Type Theory

77% match2 repos502021

Types for Grassroots Logic Programs

76% match2026

Order-Sorted Intensional Logic: Expressing Subtyping Polymorphism with Typing Assertions and Quantification over Concepts

76% match2025

Oxide: The Essence of Rust

76% match1 repo1362019

Type-Constrained Code Generation with Language Models

75% match1 repo1052025

Cite this paper

@article{diehl2018generic,
  title  = {Generic Zero-Cost Reuse for Dependent Types},
  author = {Larry Diehl and Denis Firsov and Aaron Stump},
  year   = {2018},
  eprint = {1803.08150},
  archivePrefix = {arXiv},
  url    = {https://arxiv.org/abs/1803.08150}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/1803.08150.svg)](https://codeofpaper.com/paper/1803.08150)

Discussion