Skip to main content

Adjoint Folds and Unfolds‚ Or: Scything through the Thicket of Morphisms

Ralf Hinze

Abstract

Folds and unfolds are at the heart of the algebra of programming. They allow the cognoscenti to derive and manipulate programs rigorously and effectively. Fundamental laws such as fusion codify basic optimisation principles. However, most, if not all, programs require some tweaking to be given the form of an (un-) fold, and thus make them amenable to formal manipulation. In this paper, we remedy the situation by introducing adjoint folds and unfolds. We demonstrate that most programs are already of the required form and thus are directly amenable to manipulation. Central to the development is the categorical notion of an adjunction, which links adjoint (un-) folds to standard (un-) folds. We discuss a number of adjunctions and show that they are directly relevant to programming.

Affiliation
University of Oxford‚ Computing Laboratory‚ Wolfson Building‚ Parks Road‚ Oxford OX1 3QD‚ England
Book Title
10th International Conference on Mathematics of Program Construction (MPC '10)
Editor
Bolduc‚ Claude and Desharnais‚ Jules and Ktari‚ Béchir
Location
Manoir St−Castin‚ Québec‚ Canada
Pages
195−228
Publisher
Springer Berlin / Heidelberg
Series
Lecture Notes in Computer Science
Volume
6120
Year
2010