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.
翻译:在先前的研究中,自函子的代数范畴被证明可富化于同一自函子的余代数范畴,且该富化结构的额外性质被用于定义归纳数据类型的广义化形式。这些广义归纳数据类型由余代数$C$参数化,因此我们称其为$C$-归纳数据类型;我们将其通过泛性质诱导的态射称为$C$-归纳函数。本文通过将自然变换纳入理论框架来扩展该工作:给定自函子间合适的自然变换,我们证明其可诱导代数范畴间的富化函子,且这些函子保持$C$-归纳数据类型与$C$-归纳函数。此类$C$-归纳数据类型常为对应归纳数据类型的有限版本,我们展示了该框架如何将经典的初始代数语义扩展至这些类型。例如,我们证明该理论可自然地产生列表上的部分归纳函数、列表元素类型的转换以及树剪枝函数。