Richard Bird and Ross Paterson. Formal Aspects of Computing, 11(2):200-222, September 1999.
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.
gzipped PostScript, gzipped DVI, BibTeX.
A preliminary exploration of the theory of nested (or non-regular) datatypes.
A cute application of nested types, motivating the generalized folds of the above paper.