On the Semantics of Nested Datatypes

Abstract

Nested (or non-regular or non-uniform) datatypes are recursively defined parameterised datatypes in which the parameter of the datatype changes in the recursive call. The standard semantic definition of recursively defined datatypes is as initial algebras in the category \mathitSet of sets and total functions. Bird and Meertens have shown that this theory is inadequate to describe nested datatypes. Instead, one solution proposed there was to define them as initial algebras in the functor category \mathitNat(\mathitSet), with objects all endofunctors on \mathitSet and arrows all natural transformations between them. We show here that initial algebras are not guaranteed to exist in the functor category itself, but that they do exist in one of its subcategories: the category of all cocontinuous endofunctors and natural transformations. This category is then a suitable semantic domain for nested datatypes, both first order and higher-order.