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 deï¬ne 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 ï¬rst 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"
Recent comments
12 weeks 1 day ago
12 weeks 1 day ago
12 weeks 1 day ago
34 weeks 2 days ago
38 weeks 4 days ago
40 weeks 2 days ago
40 weeks 2 days ago
42 weeks 6 days ago
47 weeks 4 days ago
47 weeks 4 days ago