A categorical approach to the theory of lists

Abstract

Many of the laws in Bird's ‘theory of lists’ [1, 2] are precisely the conditions for various constructions to be functors, natural transformations, adjunctions, and so on. In this paper, I explore this categorical background to the theory, and — by generalizing one law and adding another — establish a completeness result for part of the theory. In the final section of the paper, I indicate how a theory of expression trees could be compiled along similar lines.

None of the mathematical results in this paper are new; instead, its contribution is in showing how category theory can be used to organize a complete set of laws for program transformation. I hope, too, that the paper will provide a readable introduction to category theory for those already acquainted with functional programming.