The Functorial Nature of Enriched Data Types

Abstract

In computer science, many popular data types can be modeled in a categorical framework. More specif- ically, they can be modeled as an initial algebra in the category of F-algebras for some endofunctor F : C → C. Examples include the booleans, the natural numbers, lists, trees and more generally al- gebraic data types, W -types and inductive data types. These initial algebras have the special property that algebra morphisms out of it to any other algebra always exist and are unique. This gives us tools to easily reason about functions defined on these data types. The downside to this approach is that we lose a lot of flexibly when defining maps, since they must respect the algebra structures completely. In a recent paper it has been shown that the category of F -algebras is enriched over the category of F-coalgebras, if the category C and functor F involved are sufficiently well-behaved. This gave a structured way to define so called measurings, which respect the algebra structure up to a certain point, granting more flexibility when defining morphisms. They also introduced the notion of a C-initial algebra for some F-coalgebra C, which shares the desirable properties of an initial algebra while accommodating the idea of a measuring. So far, the above has been applied to the example of natural numbers. First off, we will consider more examples, including the previously mentioned booleans, lists and trees. We will also expand on the existing theory, showing the construction of the enriched category of F -algebras is functorial in F . That is, given a natural transformation µ : F → G, we will construct enriched functors from the category of F-algebras to the category of G-algebras and vice versa. This gives rise to functors Endo(C) → EnrCat, where Endo(C) is the category of (sufficiently well-behaved) endomorphisms on C and natural transformations. The category EnrCat is the category of enriched categories and enriched functors, and will be defined in this thesis. Throughout the thesis, we will continue to pay attention to C-initial algebras, providing many examples and showing in which cases they are preserved between categories of algebras.