Lambda the Ultimate

by Neil Ghani and Patricia Johann:

Initial algebra semantics is one of the cornerstones of the theory of modern programming languages. It provides support for fold combinators encapsulating structured recursion over data structures, thereby making it possible to both reason about and transform programs in principled ways. Recently, Ghani, Uustalu, and Vene extended the usual initial algebra semantics to support not only standard fold combinators for inductive types, but also Church encodings and build combinators for them. In addition to being theoretically useful in ensuring that build is seen as a fundamental part of the basic infrastructure for programming with inductive types, this development has practical merit: the fold and build combinators can be used to define fold/build rules which optimise modularly constructed programs by eliminating intermediate inductive data structures.

In this paper, we apply this extended initial algebra semantics to the theory and practice of programming with nested data types. In particular, we use it to simplify the theory of folds for nested types, as well as to provide the first Church encodings, build combinators, and fold/build fusion rules for them.

Code for "Folds, Church Encodings, Builds, and Short Cut Fusion for Nested Types: A Principled Approach"