Initial Algebra Semantics Is Enough!

Initial algebra semantics is a cornerstone of the theory of modern functional programming languages. For each inductive data type, it provides a fold combinator encapsulating structured recursion over data of that type, a Church encoding, a build combinator which constructs data of that type, and a fold/build rule which optimises modular programs by eliminating intermediate data of that type. It has long been thought that initial algebra semantics is not expressive enough to provide a similar foundation for programming with nested types. Specifically, the folds have been considered too weak to capture commonly occurring patterns of recursion, and no Church encodings, build combinators, or fold/build rules have been given for nested types. This paper overturns this conventional wisdom by solving all of these problems.

• Type: Conference
• Year: 2007
• Where: TLCA
• Authors: Patricia Johann, Neil Ghani
• Keywords: Inductive Data Type, Initial Algebra Semantics, Nested Types, Theoretical Computer Science, TLCA 2007