Logo image
Back
Extensible Recursive Functions, Algebraically
Preprint   Open access

Extensible Recursive Functions, Algebraically

Alex Hubers, Apoorv Ingle, Andrew Marmaduke and J. Garrett Morris
ArXiv.org
Cornell University
10/15/2024
DOI: 10.48550/arxiv.2410.11742
url
https://doi.org/10.48550/arxiv.2410.11742View
Preprint (Author's original)This preprint has not been evaluated by subject experts through peer review. Preprints may undergo extensive changes and/or become peer-reviewed journal articles. Open Access

Abstract

We explore recursive programming with extensible data types. Row types make the structure of data types first class, and can express a variety of type system features from subtyping to modular combination of case branches. Our goal is the modular combination of recursive types and of recursive functions over them. The most significant challenge is in recursive function calls, which may need to account for new cases in a combined type. We introduce bounded algebras, Mendler-style descriptions of recursive functions in which recursive calls can happen at larger types, and show that they provide expressive recursion over extensible data types. We formalize our approach in Rωμ, a small extension of an existing row type theory with support for recursive terms and types, and mechanize the metatheory of Rωμ via an embedding in Agda.
 Computer Science - Programming Languages

Details

Metrics

13 Record Views
Logo image