Disciplined, efficient, generalised folds for nested datatypes
Disciplined, efficient, generalised folds for nested datatypes
复制标题
嵌套数据类型的规范、高效、通用折叠
DOI：
--
复制
发表时间：
2004
影响因子：
1
通讯作者：
Ian Bayley
中科院分区：
文献类型：
--
作者：
Clare E. Martin;J. Gibbons;Ian Bayley
Abstract.Nested（或非统一或非常规）数据类型具有递归定义，其中类型参数会发生变化。由于类型限制，它们的折叠功率受到限制。 Bird 和 Paterson 引入了广义折叠来获得额外的功率，但代价是效率的损失：折叠可能需要比线性时间更长的时间来评估。 Hinze 引入了有效的广义折叠来应对这种低效率，但以务实的方式做到了这一点：他没有提供分类或等效的基础，因此没有获得操作折叠的相关通用属性。我们将 Hinze 的构造效率与 Bird 和 Paterson 的强大推理工具结合起来。
Abstract.Nested (or non-uniform, or non-regular) datatypes have recursive definitions in which the type parameter changes. Their folds are restricted in power due to type constraints. Bird and Paterson introduced generalised folds for extra power, but at the cost of a loss of efficiency: folds may take more than linear time to evaluate. Hinze introduced efficient generalised folds to counter this inefficiency, but did so in a pragmatic way: he did not provide categorical or equivalent underpinnings, so did not get the associated universal properties for manipulating folds. We combine the efficiency of Hinze’s construction with the powerful reasoning tools of Bird and Paterson’s.