Initial Algebra Semantics Is Enough!

ASU Author/Contributor (non-ASU co-authors, if there are any, appear on document)
Patricia Johann Ph.D, Professor (Creator)
Appalachian State University (ASU )
Web Site:

Abstract: 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.

Additional Information

Johann, P. and Ghani, N. (2007). Initial Algebra Semantics Is Enough! Proceedings, Typed Lambda Calculus and Applications 2007 (TLCA '07), pp. 207-222. NC Docks permission to re-print granted by author(s).
Language: English
Date: 2007
initial albegra semantics, programming languages, intermediate data, data, programming foundation, computer science, nested types

Email this document to