多层次语言是广义的箭头
Multi-Level Languages are Generalized Arrows
摘要：
多级语言和Arrow都促进了元编程，即编写一个程序生成一个程序的行为。所有Arrows所需的转换函数将任意宿主语言表达式转换为客语言表达式;因此，只有当客语言是宿主语言的超集时，Arrows才可以用于元编程。这种限制也存在于提供无限跨级别持久性的多级语言中。<p>本文引入了广义箭头，并证明了广义箭头在以下意义上对Arrows的推广：程序设计语言中的每一个箭头都是由一个广义箭头产生的，该广义箭头以该语言的术语范畴作为其上域。广义箭头在客户语言和宿主语言之间没有强制包含关系;它们促进了异构元编程。以所有广义箭头为态射的范畴和以所有多层语言为态射的范畴是同构范畴。这在Coq中得到了形式化的证明，并证明了多级语言是广义箭头的说法。<p>结合宿主语言中存在的一种特殊的撤回，这个证明可以用来定义一个可逆的翻译从两个级别的条款参数化的广义箭头实例的一个级别的条款。这在人体工程学上很重要：它允许客户语言提供者编写通用箭头实例，而那些客户语言的用户编写多级术语。这是有益的，因为实现广义箭头实例比修改编译器更容易，而编写两级项比操作广义箭头项更容易。
英文摘要：
Multi-level languages and Arrows both facilitate metaprogramming, the act of writing a program which generates a program. The arr function required of all Arrows turns arbitrary host language expressions into guest language expressions; because of this, Arrows may be used for metaprogramming only when the guest language is a superset of the host language. This restriction is also present in multi-level languages which offer unlimited cross-level persistence. <p> This paper introduces generalized arrows and proves that they generalize Arrows in the following sense: every Arrow in a programming language arises from a generalized arrow with that language's term category as its codomain. Generalized arrows impose no containment relationship between the guest language and host language; they facilitate heterogeneous metaprogramming. The category having all generalized arrows as its morphisms and the category having all multi-level languages as its morphisms are isomorphic categories. This is proven formally in Coq, and the proof is offered as justification for the assertion that multi-level languages are generalized arrows. <p> Combined with the existence of a particular kind of retraction in the host language, this proof can be used to define an invertible translation from two-level terms to one-level terms parameterized by a generalized arrow instance. This is ergonomically significant: it lets guest language providers write generalized arrow instances while the users of those guest languages write multi-level terms. This is beneficial because implementing a generalized arrow instance is easier than modifying a compiler, whereas writing two-level terms is easier than manipulating generalized arrow terms.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
