Initial Algebra Semantics Is Enough!
Initial Algebra Semantics Is Enough!
复制标题
初始代数语义就足够了！
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Neil Ghani
中科院分区：
文献类型：
--
作者：
Patricia Johann;Neil Ghani
最初的代数语义是现代功能编程语言理论的基石。对于每种归纳数据类型，它提供了一个折叠组合器，将结构化的递归封装在该类型的数据，教堂编码的数据，构建该类型数据的构建组合器以及折叠/构建规则的构建组合中，该规则通过消除该模块化程序来优化模块化程序。类型。长期以来，人们一直认为，初始代数语义的表达不足，无法为使用嵌套类型的编程提供类似的基础。具体而言，这些褶皱被认为太弱了，无法捕获通常发生的递归模式，并且没有为嵌套类型提供教堂编码，构建组合或折叠/构建规则。本文通过解决所有这些问题来推翻这种传统的观点。
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.