Functoriality of Enriched Data Types
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910035494305792 |
|---|---|
| author | Mulder, Lukas North, Paige Randall Péroux, Maximilien |
| author_facet | Mulder, Lukas North, Paige Randall Péroux, Maximilien |
| contents | In previous work, categories of algebras of endofunctors were shown to be enriched in categories of coalgebras of the same endofunctor, and the extra structure of that enrichment was used to define a generalization of inductive data types. These generalized inductive data types are parametrized by a coalgebra $C$, so we call them $C$-inductive data types; we call the morphisms induced by their universal property $C$-inductive functions. We extend that work by incorporating natural transformations into the theory: given a suitable natural transformation between endofunctors, we show that this induces enriched functors between their categories of algebras which preserve $C$-inductive data types and $C$-inductive functions. Such $C$-inductive data types are often finite versions of the corresponding inductive data type, and we show how our framework can extend classical initial algebra semantics to these types. For instance, we show that our theory naturally produces partially inductive functions on lists, changes in list element types, and tree pruning functions. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_06059 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Functoriality of Enriched Data Types Mulder, Lukas North, Paige Randall Péroux, Maximilien Category Theory Logic in Computer Science In previous work, categories of algebras of endofunctors were shown to be enriched in categories of coalgebras of the same endofunctor, and the extra structure of that enrichment was used to define a generalization of inductive data types. These generalized inductive data types are parametrized by a coalgebra $C$, so we call them $C$-inductive data types; we call the morphisms induced by their universal property $C$-inductive functions. We extend that work by incorporating natural transformations into the theory: given a suitable natural transformation between endofunctors, we show that this induces enriched functors between their categories of algebras which preserve $C$-inductive data types and $C$-inductive functions. Such $C$-inductive data types are often finite versions of the corresponding inductive data type, and we show how our framework can extend classical initial algebra semantics to these types. For instance, we show that our theory naturally produces partially inductive functions on lists, changes in list element types, and tree pruning functions. |
| title | Functoriality of Enriched Data Types |
| topic | Category Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2505.06059 |