Measuring data types
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911885064929280 |
|---|---|
| author | Mulder, Lukas North, Paige Randall Péroux, Maximilien |
| author_facet | Mulder, Lukas North, Paige Randall Péroux, Maximilien |
| contents | In this article, we combine Sweedler's classic theory of measuring coalgebras -- by which $k$-algebras are enriched in $k$-coalgebras for $k$ a field -- with the theory of W-types -- by which the categorical semantics of inductive data types in functional programming languages are understood. In our main theorem, we find that under some hypotheses, algebras of an endofunctor are enriched in coalgebras of the same endofunctor, and we find polynomial endofunctors provide many interesting examples of this phenomenon. We then generalize the notion of initial algebra of an endofunctor using this enrichment, thus generalizing the notion of W-type. This article is an extended version of arXiv:2303.16793, it adds expository introductions to the original theories of measuring coalgebras and W-types along with some improvements to the main theory and many explicitly worked examples. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_14678 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Measuring data types Mulder, Lukas North, Paige Randall Péroux, Maximilien Category Theory Logic in Computer Science Algebraic Topology Primary: 18C50, 68Q25, 16T15. Secondary: 18D20, 03B70 In this article, we combine Sweedler's classic theory of measuring coalgebras -- by which $k$-algebras are enriched in $k$-coalgebras for $k$ a field -- with the theory of W-types -- by which the categorical semantics of inductive data types in functional programming languages are understood. In our main theorem, we find that under some hypotheses, algebras of an endofunctor are enriched in coalgebras of the same endofunctor, and we find polynomial endofunctors provide many interesting examples of this phenomenon. We then generalize the notion of initial algebra of an endofunctor using this enrichment, thus generalizing the notion of W-type. This article is an extended version of arXiv:2303.16793, it adds expository introductions to the original theories of measuring coalgebras and W-types along with some improvements to the main theory and many explicitly worked examples. |
| title | Measuring data types |
| topic | Category Theory Logic in Computer Science Algebraic Topology Primary: 18C50, 68Q25, 16T15. Secondary: 18D20, 03B70 |
| url | https://arxiv.org/abs/2405.14678 |