A Few Constructions on Constructors
A Few Constructions on Constructors
复制标题
关于构造函数的一些构造
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
James McKinna
中科院分区：
文献类型：
--
作者：
Conor McBride;H. Goguen;James McKinna
我们提出了可以为每种归纳数据类型生成的标准设备的四种结构：案例分析、结构递归、无混淆、非循环性。我们的构造遵循两级方法——它们比激发它们灵感的标准技术需要更少的工作[11,8]。此外，考虑到适当的异构概念，它们可以毫无困难地扩展到数据类型的归纳族。这些结构是从模式匹配风格 [7] 的依赖类型程序到归纳原理 [21] 表达的等效程序的翻译的重要组成部分，因此在警句 [25] 中发挥着至关重要的幕后作用。
We present four constructions for standard equipment which can be generated for every inductive datatype: case analysis, structural recursion, no confusion, acyclicity. Our constructions follow a two-level approach—they require less work than the standard techniques which inspired them [11,8]. Moreover, given a suitably heterogeneous notion of equality, they extend without difficulty to inductive families of datatypes. These constructions are vital components of the translation from dependently typed programs in pattern matching style [7] to the equivalent programs expressed in terms of induction principles [21] and as such play a crucial behind-the-scenes role in Epigram [25].