Adjoint folds and unfolds—An extended study

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 introd...

Full description

Saved in:
Bibliographic Details
Published in:Science of computer programming 2013-11, Vol.78 (11), p.2108-2159
Main Author: Hinze, Ralf
Format: Article
Language:English
Subjects:
Adjunction
Final coalgebra
Fold
Fusion
Haskell
Initial algebra
Kan extension
Unfold
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0167-6423
1872-7964
DOI:10.1016/j.scico.2012.07.011