Elaborator reflection: extending Idris in Idris
Elaborator reflection: extending Idris in Idris
复制标题
DOI：
10.1145/2951913.2951932
复制
发表时间：
2016-09
期刊：
影响因子：
--
通讯作者：
D. Christiansen;Edwin C. Brady
中科院分区：
文献类型：
--
作者：
D. Christiansen;Edwin C. Brady
许多编程语言和证明助手都是通过从具有大量隐含信息的高级语言到高度显式的核心语言的精化来定义的。在许多高级语言中，这些精化工具包含用于程序构建的强大工具，但这些工具很少被设计为可供用户重新利用。我们描述了Producator反射，这是一种元编程范例，其中的精化机制直接可用于元程序，以及在Idris中精化反射的具体实现，Idris是一种具有完全依赖类型的函数式语言。我们论证了Idris的反思精化框架对一些现实问题的适用性，我们讨论了其设计特定特征的动机，并探索了阐述者反思的更广泛的含义，因为它可以与其他语言相关。
Many programming languages and proof assistants are defined by elaboration from a high-level language with a great deal of implicit information to a highly explicit core language. In many advanced languages, these elaboration facilities contain powerful tools for program construction, but these tools are rarely designed to be repurposed by users. We describe elaborator reflection, a paradigm for metaprogramming in which the elaboration machinery is made directly available to metaprograms, as well as a concrete realization of elaborator reflection in Idris, a functional language with full dependent types. We demonstrate the applicability of Idris’s reflected elaboration framework to a number of realistic problems, we discuss the motivation for the specific features of its design, and we explore the broader meaning of elaborator reflection as it can relate to other languages.