Abstracting Extensible Recursive Functions
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866915403379245056 |
|---|---|
| author | Hubers, Alex Ingle, Apoorv Marmaduke, Andrew Morris, J. Garrett |
| author_facet | Hubers, Alex Ingle, Apoorv Marmaduke, Andrew Morris, J. Garrett |
| contents | 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 including record subtyping and 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 extensible histomorphisms, 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 row type theory with support for recursive terms and types. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_11742 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Abstracting Extensible Recursive Functions Hubers, Alex Ingle, Apoorv Marmaduke, Andrew Morris, J. Garrett Programming Languages 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 including record subtyping and 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 extensible histomorphisms, 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 row type theory with support for recursive terms and types. |
| title | Abstracting Extensible Recursive Functions |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2410.11742 |