Functoriality of Enriched Data Types

TL;DR

This paper extends the theory of enriched categories of algebras of endofunctors to include natural transformations, enabling the definition of generalized inductive data types and functions that preserve their structure.

Contribution

It introduces a framework incorporating natural transformations to produce enriched functors that preserve $C$-inductive data types and functions, extending initial algebra semantics.

Findings

Framework produces partially inductive functions on lists

Enables changes in list element types

Supports tree pruning functions

Abstract

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.