Adjoint folds and unfolds—An extended study

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. However, most, if not all, programs require some tweaking to be given the form of an (un)fold. In this article, we remedy the situation by introducing adjoint (un)folds. We demonstrate that most programs are already of the required form and thus are directly amenable to formal manipulation. Central to the development is the categorical notion of an adjunction, which links adjoint (un)folds to standard (un)folds. We discuss a multitude of basic adjunctions and ways of combining adjunctions and show that they are directly relevant to programming. Furthermore, we develop the calculational properties of adjoint (un)folds, providing several fusion laws, which codify basic optimisation principles. We give a novel proof of type fusion based on adjoint folds and discuss several applications - type fusion states conditions for fusing a left adjoint with an initial algebra to form another initial algebra. The formal development is complemented by a series of examples in Haskell.