c © 1999 BCS Generalised folds for nested datatypes

Abstract. Nested datatypes generalise regular datatypes in much the same way that context-free languages generalise regular ones. Although the categorical se-mantics of nested types turns out to be similar to the regular case, the fold functions are more limited because they can only describe natural transforma-tions. Practical considerations therefore dictate the introduction of a generalised fold function in which this limitation can be overcome. In the paper we show how to construct generalised folds systematically for each nested datatype, and show that they possess a uniqueness property analogous to that of ordinary folds. As a consequence, generalised folds satisfy fusion properties similar to those developed for regular datatypes. Such properties form the core of an effective calculational theory of inductive datatypes