Abstract.
Nested datatypes generalise regular datatypes in much the same way that context-free languages generalise regular ones. Although the categorical semantics of nested types turns out to be similar to the regular case, the fold functions are more limited because they can only describe natural transformations. 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.
Similar content being viewed by others
Author information
Authors and Affiliations
Additional information
Received September 1998 / Accepted in revised form July 1999
Rights and permissions
About this article
Cite this article
Bird, R., Paterson, R. Generalised folds for nested datatypes. Formal Aspects of Computing 11, 200–222 (1999). https://doi.org/10.1007/s001650050047
Issue Date:
DOI: https://doi.org/10.1007/s001650050047