理论计算机科学电子札记148（2006）27-52www.elsevier.com/locate/entcsCα ml概述FrancoisPottier1INRIA摘要Cα ml是一个将所谓的“绑定规范”转换为Objective Caml编译单元的工具。绑定规范类似于代数数据类型声明，但也包括有关名称和绑定的信息。Cα ml旨在帮助解释器，编译器或其他程序的编写者以安全和简洁的方式处理α转换。本文概述了Cα ml关键词：元编程，变量绑定，α-转换1引言函数式编程语言，如ML和Haskell，旨在构建、检查和转换复杂的符号对象，如程序和证明。它们非常适合这项任务，因为这些对象通常表示为抽象语法树，其结构很容易通过代数数据类型声明在ML或Haskell中表达-或者是吗？事实上，抽象语法树包含可以绑定的名称。操纵这样的树涉及到许多尊重名称含义的操作，例如计算术语的自由名称集，或者在整个术语中用名称（或术语）代替名称而不捕获ML或Haskell不支持这些操作。因此，它们必须使用下面讨论的各种方法之一进行手工编码这种手工编码过程是乏味的，而且容易出错。显然，需要一个1Email：Francois. Pottier@inria. fr1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.11.03928F. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）27更声明性的、健壮的、自动化的方法来处理涉及名称和绑定的抽象语法。也许应该区分问题的三个方面。首先，需要一种规范语言，它提供了一种描述抽象语法树结构的声明性方法，包括绑定信息。第二，需要一种实现技术，也就是说，一个高效的运行时表示- tation的名称和绑定器。最后，应该有一个从规范到实现的自动化路线我们现在依次讨论这三点Specificationslanguages. 在文献中出现了许多特殊语言。Plotkin [25]定义了一个“绑定签名”的概念，它允许形式为（x 1，.，xn）t，其中名称x1，. .. Talcott[33] 引 入 了 Honsell 等 人 的 “ 名 义 代 数 ”[ 11 ] 和 Urban et al. ’s “nominalsignatures” [ Shinwell的Fresh Objective Caml [29，30，31]实现了名义签名的广义形式，其中名称的绑定出现可以占据任意结构的项，而不仅仅是元组（x 1，.，xn）的固定大小n。特别是，这允许绑定可变数量的名称的构造。尽管如此，我们仍然认为这些建议中没有一个是完全令人满意的：仍然存在无法用这些规范语言中的任何一种忠实地建模的真实世界的构造特别是，绑定变量名的构造，如ML实施例2.3和2.4提供了细节。本文的第一个贡献是提出了一种新的绑定规范语言，它具有足够的表达能力来处理这些结构和许多其他结构。这个提议的一个重要方面是一种表达性的模式语言。模式用于形成抽象。模式是术语，因此它们可以具有任意大小。特别是，模式可以绑定任意长度的名称列表模式可以包含名称（的绑定出现）、位于抽象范围内的子术语和位于抽象范围外一个关键点是，术语的词汇结构（即，绑定器的位置及其范围的范围）不必与其物理结构相一致实施技术。De BruijnF. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）2729非常流行的一种实现技术。它包括将名称（自由或绑定）编码为整数索引，可以将其解释为指向其绑定站点的（相对）指针。它的优点是α-等价与一阶等价一致，并且不需要“新鲜”名称生成器。它的主要缺点是它使得开放式术语的含义依赖于上下文，需要在Fresh Objective Caml [29，30，31]和Fresh-Lib [5]实现中使用的另一种技术包括将名称编码为原子-可以测试相等性的值，但否则没有意义。在这种方法中，当一个抽象被打开时，它绑定的原子必须被这里采用了这种技术自动化实施。在实践中，通过编写规范而不是代码来处理绑定问题是可取的。换句话说，需要能够直接处理绑定规范的工具。满足这一需求的一种方法是将这一特性结合到编程语言设计中。例如，Pitts和Gabbay因此，在FreshML中，alge数据类型定义具有足够的表达力，可以按照Urban等人的风格对名义签名进行编码。 [34]. 对抽象的模式匹配Fresh Objective Caml [29 ， 30 ， 31] 是 FreshML 的 继 任 者 Urban 和CheneyαProlog项被统一到α-等价。然而，与设计一种新的编程语言相反，也可以编写一个单独的工具，接受绑定规范并为现有的编程语言生成代码这就是本文件所遵循的方法它没有我们最直接的竞争对手Fresh Objective Caml那么雄心勃勃，但更简单简单性的一个实际好处是使一些有用的优化，如这种工具的实际设计是我们的第二个贡献。Cheney通过依赖Haskell对泛型编程的支持，避免了对单独代码生成工具的需求在本文中，我们描述了Cα ml（发音：（该工具可以很容易地适应其他编程语言，如Haskell。我们首先对绑定规范语言（的简化版本）的语法进行正式说明（§ 2）。 我们给30F. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）27s：：=内部|外部范围规范t：：=单位|t × t |t + t|原子|⟨u⟩Expression typesu：：=单位|u × u |u + u|原子|st模式类型e：：=（）|（e、e）|因吉埃|一|中文（简体）p：：=（）|（p，p）|因吉伊普|一|se模式Fig. 1. 类型和术语通过对约束规范所产生的α等价关系提供形式定义，对这种语言赋予意义（§3）。然后是对Cα ml接受的具体绑定规范（§4）和生成的代码（§5）的非正式描述在与相关工作进行更全面的比较后（§6），我们总结了我们的贡献并讨论了未来工作的方向（§7）。2结合规范在本节和下一节中，我们采用了类型和术语的结构化观点这与更常见的方法相反，后者要求首先给出签名（或规格）。签名通常指定一组（命名的）类型构造函数，每个构造函数都配备了一个排序，从而产生一个类型代数;以及一组（命名的）项构造函数，每个构造函数都配备了一个元数，从而产生一个项代数在实践中，为类型和术语构造函数分配名称是有用和可取的，实际上，我们的工具是由程序员提供的规范驱动的（§4）。在这个理论上的阐述，但是这种程度的细节比较分散注意力，所以我们干脆就省略了。因此，我们的类型和术语的语法是固定的，如图1所示。类型被划分为表达式类型（写为t）和模式类型（写为u）。类似地，术语被划分为表达式（写作e）和模式（写作p）。我们让一个范围在一个可数无限原子集A上。我们将原子（p）写为出现在模式p内（在任何深度）的所有原子的（有限）集合，而不管它们出现(free绑定或绑定）。表达式和模式可以呈现任意结构。实际上，表达式和模式类型都包括单元类型和二进制乘积F. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）2731ba（（））=ba（s e）=ba（（p1，p2））=ba（p1）ba（p2）ba（injip）=ba（p）ba（a）={a}图二. 原子被一种模式和 总 和 。 因 此 ， 表 达 式 和 模 式 都 包 括 单 位 项 written （ ） 、 pairs 和injection，写为inji·，其中i的范围超过{1， 2}。表达式和模式类型都包含原子类型。因此，表达式和模式都包括原子a。表达式和模式之间的区别在于解释这些原子的方式。在表述中，原子的出现被理解为是指该原子在结合位置中的某个较早在模式中，原子的出现被理解为该原子的结合位点例如，当我们在我们的框架中对λ演算的项进行编码时（例2.1），我们将看到a在项（λa.a）a中（的编码）最左边的出现位于模式中，而其他两个位于表达式中。表达式包括抽象p，其中p是一个模式。相反，抽象包括一个抽象结束构造s e，其中e是一个表达式，作用域规范s是内部和外部之一。很自然地，表达式类型和模式类型包含类似的结构u和s t。模式p可以被认为是一棵树，其中每个叶子都携带一个原子或一个用作用域指定符装饰的子表达式。出现在前一种叶子上的所有原子的集合，写作ba（p），被称为被p束缚的原子的集合。后一种叶子对它没有贡献，它的正式定义见图2。抽象的含义现在可以非正式地解释如下。当一个抽象p形成时，被p束缚的原子就被束缚在p的子表达式中，这些子表达式被inner修饰。但是，在用outer修饰的子表达式中，它们不会被绑定。因此，内规范和外规范用于区分位于抽象范围内的子表达式，以及碰巧物理上附着在树p的叶子上但不位于抽象范围内的子表达式。表达式和表达式类型之间以及模式和模式类型之间的对应关系非常简单。我们省略它的定义。值得指出的是，图1中的类型定义可以而且应该被视为共归纳的，从而产生了递归类型。这是必要的，因为无限大小的数据结构家族，如列表和抽象语法树，只有递归类型。表达的定义32F. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）27另一方面，应将表达式和模式视为归纳的：也就是说，表达式和模式是有限的术语。我们不想对无限项的α等价进行推理，因为这个微妙的概念到目前为止还没有什么实际应用。下面的两个例子说明了我们的抽象和抽象结束构造的预期含义，以及内部和外部作用域规范之间的区别。例2.1纯λ-演算的项由文法M：= a|MM| λ a.M条件是，在λ-抽象λa.M中，原子a束缚在λ-项M内。在我们的框架中，这些项被编码为类型t的表达式，其中t是以下方程的唯一解：t=atom+（t×t）+atom ×innert(For为了可读性，我们的例子在必要时使用了n元乘积和和λ-项λa.a的编码是类型t注射3（a，内注射1a）根据上面的非正式解释，原子a被认为是束缚在这个抽象中的。事实上，它的最左边的出现使它成为由模式（a，内部）约束的原子的一部分。. ）.它的作用域是子表达式inj1a，用inner修饰。因此，整个表达式应被视为α等价于inj3（aJ， inner inj1aJ）其编码λ项λAJ.AJ。我们对α等价的定义（§3）确实与这些表达式有关。例2.2纯λ-演算经常被局部定义的letM：=...... | let a = M in M在局部定义中，设a=M1在M2中，原子a束缚在M2中。 在我们的框架中，λ项可以编码为t类型的表达式，其中t满足t=. + n原子×外部t ×内部t在a中的λ-项的编码让a=a是表达式注射4次（a，外注射1a，内注射1a）F. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）2733同样，原子a被约束在这个抽象中，它的作用域由仅内部子表达式-外部子表达式不位于其作用域中因此，该表达式应被视为α-等价于inj4（aJ，外inj1a，内inj1aJ）其对λ项进行编码，令aJ=ainaJ。前面的两个例子说明了inner和outer的用法。尽管如此，也许还不清楚为什么outer是有用的，为什么模式可以包含多个子表达式。相反，让我们暂时考虑一种受限制的语言，其中外部被抑制，每个抽象都包含一个单独的，独特的子表达式，隐含地用内部装饰。产生式p：：=s e被抑制，因此模式不再包含表达式，并且一元抽象构造p被替换为形式为pe的二元抽象构造，其中ba（p）中的原子被认为绑定在e内。在类型级别上也进行了类似的更改很明显，这种受限语言可以嵌入到完整的语言中。实际上，可以将pe编码为（p，inner e），将ut编码为u×innert。因此，后者至少和前者一样具有表现力。然而，相反的情况只在一定程度上是正确的。当然，这种受限制的语言是很有表现力的.它包含了名义代数[11]以及名义签名[34]，并对应于新鲜目标的一个片段Caml [29，31，30].特别是，它的表现力足以充分处理例2.1和2.2。实际上，例2.1的类型atom×inner t在受限语言中可以写成atomt。例2.2的类型atom×outert×innert可以写成t × atomt，如果人们愿意改变三个成分的排列顺序，并将外部t提升到抽象之外，它就变成了t。然而，在有些情况下，这种伎俩是无法施展的。这些通常涉及结合可变数量原子的模式我们主张，在这些情况下，我们更一般的语言具有更优越的可解释性。下面两个例子证实了这一说法。例2.3λ演算的现实扩展允许局部定义同时约束多个原子：M：：=. | let a = M and ... a=MinM在一个定义中，设a1= M1，且... 并且在M中，原子{a1，.，an}在M中是有界的。它们不受M1的约束，，Mn.在我们的框架中，这样的λ-项被编码为类型t的表达式，其中t和辅助模式34F. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）27型u满足方程t =. +u×内tu=单位+原子×（外部t）×u第二个方程将u定义为一个原子和一个外部表达式的配对列表的类型。因此，绑定列表a1= M1，.，an= Mn可以被编码为类型u的模式。第一个等式指出，let定义被编码为一个抽象，它由这样一个绑定列表和一个内部表达式，它编码最终λ项M。 根据定义（图2），由这种抽象所约束的原子是原子{a1，.，an}，它们的作用域是对M进行编码的内部表达式。 它们的范围不包括编码M1，. ，Mn，即使这些表达式物理上位于抽象内部，因为它们被标记为外部。在上面讨论的限制形式主义中，人们如何处理这种情况 项M1，. ，Mn必须位于抽象的范围之外，因此，在受限语言中，它们必须物理地位于抽象之外。结合的原子是1，...另一方面，an必须位于抽象的左侧。因此，必须维护两个单独的列表：表达式列表和原子列表。t =.+tJ×utJ=unit+t×tJu=单位+原子×u这种编码既笨拙又脆弱。事实上，它引入了垃圾：人们可能会意外地破坏两个列表具有相同长度的属性，并构造一个不编码有效λ-项的项。相比之下，在我们的新形式主义中，我们的模式可以有无限数量的子表达式，而不是只有一个，并且这些子表达式可以被标记为内部或外部，这一事实提供了足够的可扩展性来解决这个问题，Shinwell [29，pages 19-20]识别了这个问题，例2.4现在让我们用相互递归的局部定义来扩展λ演算：M：：=. | letrec a = M and ... a=MinM在定义函中c a1= M1， ... 和 an=Mn 在M中，原子{a1，.，an}被束缚在M1，.，Mn和M. 在我们的框架内，F. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）2735λ-项被编码为类型t的表达式，其中t和辅助模式类型u满足以下方程：t =. +u×内tu=单位+原子×（内部t）×u这个定义与例2.3的定义几乎相同。唯一的区别是，定义模式类型u的方程现在提到了内部t而不是外部t。因此，由模式约束的原子的作用域不仅包含λ项M（的编码），而且包含λ项M1，.，Mn的值。同样，我们在不将绑定列表拆分为两个单独列表的情况下实现了这一效果，而以前的方法似乎无法做到这一点。特别是，上面讨论的限制形式主义需要将原子列表分开1，. ，ann，其必须位于抽象的左手侧，以及编码M1，.，Mn，它必须位于抽象的右侧[29，第20页]。Cα ml中的抽象故意不能直接嵌套：当一个抽象被打开时，它必须在引入另一个抽象之前被关闭（通过内部或外部）。这种设计选择使得更容易定义和理解内部和外部的含义。Fresh Objective Caml [29，30，31]更自由，允许（二进制）抽象的左嵌套，目前在Cα ml中没有类似物。3α-等价的一个定义现在，我们通过正式定义两个项何时是α等价的，来给前一节中介绍的语言赋予精确的含义我们对α等价的定义是按照皮茨的风格[23]，但需要一些初步的定义，以便处理我们丰富的模式语言3.1更名定义3.1重命名是原子到原子的有限双射映射，即A的两个有限子集之间的双射。重命名隐含地被视为原子到原子的总体（但不一定是双射）映射，从模式到模式，从表达式到表达式。重命名被视为以最直接的方式将模式映射到模式，将表达式映射到表达式也就是说，36F. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）2712[a1/a2] ={（a2，a1）}[injip1/injip2]=[p1/p2][()/（）] =<$[（p1，pJ）/（p2，pJ）]=[p1/p2]<$[pJ/pJ]1 2 1 2[s e1/s e2]=如果此关系是重命名关系图三. 通过重命名一个词中的原子被重命名。无论此事件是绑定新名称还是引用现有名称，都将被忽略。没有采取任何预防措施α-等价的标准处理方法，如Pitts这样的重命名，通常写为[a1/a2]，将a2映射为a1。将它应用于表达式e，盲目地将e中出现的每个2替换为1。通常通过要求原子a1对于e来说是新鲜的来避免捕获。在本文中，我们需要构造更复杂的重命名，我们写[p1/p2]，其中p1和p2是共同类型的模式只有当p1和p2具有相同的“模式结构”时，这种重命名才被定义，也就是说，当它们只在（i）它们的结合原子的身份和（ii）它们的（内部或外部）子表达式中不同时定义3.2图3中定义的部分函数[·/·]将一种常见类型的模式对映射到重命名。也就是说，如果p1和p2是一个共同类型u的两个模式，那么[p1/p2]要么是未定义的，要么是重命名的。当它被定义时，它的定义域是ba（p2），它的值域是ba（p1）。图3中左上角的等式表明[a1/a2]是将a2映射到a1的单例重命名。下面的下一个等式说明空重命名将单元模式（）与其自身相关联。左下角的等式表明，在模式之间重命名如果他们不同意也没关系右上方的等式指出，当i和j时，[injip1/injj jp2]是未定义的。[1][2 ][3][4][5][6][7][8][9][10][11][12][13][14][15][16][17][18][19]也就是说，只有模式具有相同结构的基因可以是相关的。在结合可变数目的原子的构建体的情况下，例如实施例2.3和2.4中所示的那些，这特别意味着仅结合相同数目的原子的模式可以相关。最后一个等式指出，为了关联两个模式对（p1，pJ）和（p2，pJ），将问题分解成分量。也就是说，F. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）273712p=p1α2（）s=（）（p1，p2）s=（ps，ps）（s e）s=e1 2as=（）（injip）s=injips（sJe）s=（）ifs sJ见图4。 收集模式的内部或外部子表达式e1=αe2eJ=αeJe1=αe2（）=α（）（e1，eJ）=（e2，eJ）inj e1=inja=αae21α2iαi外部外部1α2[p/p1]p内部=[p/p2]p内部atoms（p）atoms（p1，p2）=p1图五. 表达式的α重命名[p1/p2]和[pJ/pJ]形成它们的集合论并集，得到1 2原子上的关系，并检查该关系是否是重命名。 此复选如果新的关系不是可应用的或不是单射的，则失败。例如，当试图为不同的原子x，y，z计算[（x，y）/（z，z）]或[（z，z）/（x，y）]时，会发生这种情况。另一方面，当评估[（（x，y），x）/（（z，x），z）]时，检查这产生了将z映射到x和将x映射到y的重命名。请注意，模式不一定是线性的：一个原子可以在一个模式中出现多次。我们的定义只要求所有事件都被一致地重命名。3.2α等价定义3.3如果p是一个模式，s是一个作用域指定符，那么ps表示一个表达式，如图4所示。这个转换将删除p中的所有原子，以及所有未标记为s的子表达式，用（）替换它们。简而言之，ps可以看作是p中标记为s的子表达式的集合。模式的结构（对，注入）被保留，但将是不相关的。定义3.4普通类型表达式上的α-等价由图5的规则定义。定义是通过表达式大小的归纳，而不是结构归纳，因为在最后一条规则中进行了修剪和重命名38F. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）27图5中的前四个规则是标准的全等规则。我们关注最后一条规则，它指定了两个抽象p1和p2何时是α等价的。第一个前提检查位于外部作用域的任何子表达式都是α等价的。辅助函数（·）外部擦除绑定位置的所有原子以及所有内部子表达式，以便它们不参与此检查。第二个前提要求[p/p1]和[p/p2]被定义为特定的模式p。这意味着p1和p2具有相同的结构（忽略它们的子表达式），并且只在它们结合的原子的一致重命名下才不同。为了克服这种差异，人们将它们映射到一个共同的模式p：也就是说，人们检查，在重命名[p/p1]下，和[p/p2]，p1和p2的内子表达式是α等价的.这些子表达式是使用辅助函数（·）inner收集的。最后一个前提要求p对于pi是新鲜的，其中i的范围超过{1， 2}。这允许将[p/pi]（域ba（pi）的双射）视为域原子（pi）的双射。这就防止了俘获，也就是说，在pi内部束缚原子和自由原子之间的混淆。当p1和p2具有类型atom×innert时，规则简化为[a/a1]e1=α[a/a2]e2a/∈atoms（a1，e1，a2，e2）（a1，innere1）直到符号上的差异，这正是α等价的定义，例如在Pitts皮茨定理3.5 = α是一个等价关系。4混凝土规格前几节已经简单地介绍了我们的类型语言和术语语言。Cα ml接受的结合特异性在几个方面更复杂图6以具体语法显示了一个无类型λ演算的绑定规范最明显的区别相对于理论presentation是实体命名。事实上，规范定义了一个命名类型的集合（表达式，lambda等）。在代数数据类型定义的传统中，每种类型都被定义为求和类型或乘积类型。F. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）2739排序变量类型表达式=| 原子变量的EVAR| lambda的Elambda<>| 表达式的EApp|表达式的表达式| EInjof[ int ] int表达式| ECaseofexpression分支列表| ELetRecof类型lambda绑定var=原子变量内部表达式类型分支=<条款>type子句绑定var=pattern内部表达式类型 letrecbindsvar =系结串列内表式类型绑定绑定var=模式变量内部表达式类型模式绑定var =|P通配符| 原子变化的PVar| 图案图案的PP空气| PInj， [ int ]数组模式| 模式的P和| 图案的POr见图6。 无类型λ-演算类型.每个求和类型都有一组命名的数据构造函数（EVar、ELAambda等）。在图6中，所有产品类型都是元组类型，其字段是匿名的。Cα ml也处理记录类型，其字段被命名。所有的定义都是相互递归的：它们的作用域是整个规范。简而言之，Cα ml o表示等递归类型，而为了简单起见，理论§2-3中的accountCα ml能够处理多种原子。在图6中，只声明了一个这样的排序（var）atom关键字的每一次出现后面都跟着一个排序。一个涉及多个排序的规范将在后面进一步展示在具体语法中，表达式类型和模式类型的区别在于后者（并且只有后者）带有绑定子句。这样的子句由binds关键字，后跟一个或多个排序组成。在图6中，子句在这种类型的定义中出现数据构造函数ELAambda和类型lambda的定义遵循例2 - 1。数据构造函数ELetRec以及类型letrec和binding的定义遵循例2.4。此外，示例规范包括二进制积和和（EPair，EInj），案例结构（ECase）和丰富的模式语言（pattern）。模式在case构造和let rec定义中都有使用。（binding和clause的类型的定义恰好相同。我们把它们分开是为了清楚起见。）分支被定义为一对模式和一个内部表达式的抽象。在那里，出现在左手图案中的每个原子都被认为是在右手表达式中被束缚的letrec定义被定义为一对绑定列表和一个内部表达式的抽象在那里，出现在某个束缚的左手模式中的每个原子都被认为是束缚在每个束缚的右手表达式中，而在右手表达式40F. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）27排序类型变量type类型=| 原子类型的Tvarvar| 类型箭头| ......这是什么？类型表达式=| .. .| ETType表达式类型的注释类型模式绑定var =| .. .| PT类型模式注释中性类型图7.第一次会议。类型化λ-演算的具体绑定规范（节选）let rec构造的表达式。这很好地说明了规范语言的可扩展性。还有一些特性值得讨论：集装箱。定义letrec时使用的类型构造函数列表来自Objective Caml默认情况下，它为Cα ml所知类型构造函数选项也是内置的。其他例如，如果Cαml不知道list，则可以声明如下：uses containerlistwithList.mapandList.线性。这里，对象语言包括连接和分离模式（PAn，POr）。人们可能想检查合取模式的两边是否有不相交的束缚原子集，而析取模式的两边是否有相同的束缚原子集Cα ml不需要知道（事实上，也不能被告知）这个良构条件。这是由用户来执行的。这是可以接受的，因为这个条件不会以任何方式与α目标Caml逃生舱口。注射的数据构造函数（EInj，PInj）带有一个整数参数，其类型为Objective Caml类型int。当用方括号括起来时，在规范中允许Arbitrary Objective Caml类型表达式。在方括号内，α-等价是恒等式。换句话说，Cα ml假装方括号内的值这是有用的，特别是当一个人希望附加可变信息的条款。可变记录字段或引用单元格在规范中不直接允许，但允许放在方括号内。多种原子。图7描述了如何使用可以出现在对象级表达式和模式中的类型注释来丰富图6的无类型λ演算类型变量由一种新的原子（typevar）表示，因此它们被认为与术语变量不同。类型包含sorttypevar的原子。表达式现在可以包含类型annota-F. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）2741类型表达式=| var的EVar| λ的λ| 表达式的EApp|表达式的表达式| EInjof（int）int表达式| ECaseofexpression子句列表| Letrec的ELetRecvar=身份证。不lambda =变量表达式见图8。 图6规范的原始版本（摘录）通过一个新的数据构造器ETypeAnnotation，表达式现在包含了var和typevar的原子。类似地，模式现在可以通过一个新的数据构造函数PTypeAnnotation包含类型注释，所以模式现在包含sortvar和typevar的原子，但只绑定前者。在PTypeAnnotation的定义中，第二个参数，其类型是typ，前面有关键字neutral，而根据我们到目前为止所说的，应该是inner或outer。实际上，在这种特定的情况下，内部和外部之间的区别变得毫无意义：pattern绑定了var类的原子，而typ从来没有引用过var，所以typ是在抽象的范围之内还是之外没有区别。为了避免用户在内部和外部之间做出任意决定，我们提供了关键字neutral。在inner和outer等效的情况下，允许并要求使用此关键字。这提供了一个有用的健全性检查。5从规范到代码在绑定规范之外，Cα ml生成Objective Caml类型定义和代码。在类型定义中，所有Cα ml特定的标记都被消除。其中一些，如内部、外部和中性关键字、绑定子句和方括号，只是被删除了。其他一些方面，包括atom关键字和抽象的出现，以两种不同的方式处理也就是说，Cα ml生成每个类型定义的两个版本，一个原始版本和一个内部版本。5.1“Raw” type图8显示了图6规范的原始版本的片段。在这个版本中，所有出现的atom都被向下转换为Objective Caml类型Identifier.t，默认情况下它与string同义。如果需要的话，可以提供Identi f ier的另一种定义;例如，identi f ier可以是一个字符串和一个被设置到某个源文件中的对象的对。抽象被抹去了。42F. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）27类型表达式=| var的EVar| ELambda of opaque lambda| 表达式的EApp|表达式的表达式| EInjof（int）int表达式| ECaseofexpression子句列表| ELetRec of opaque letrecvar=Var.Atom.tlambda =变量表达式不透明的Lambdavalcreate lambda：lambda→opaque lambdavalopen lambda：opaque lambda→lambda图9.第九条。图6规范的内部版本（摘录）原始版本仅用于文本形式之间的转换在原始形式和内部形式之间来回转换的函数由Cα ml自动生成在进入的过程中（从原始形式到内部形式），他们检查每个标识符是否正确绑定，并将标识符转换为原子的内部表示在离开的路上，它们将原子重新变成人类可读的标识符。事实上，解析器和漂亮的打印机只需要处理原始表单，这意味着它们可以以标准的风格编写，而不用担心名称和绑定。5.2“Internal” type图9显示了图6规范的内部版本的片段。在这个版本中，每种原子都被翻译成一个不同的抽象类型。更准确地说，类似地，模块Var和Typevar具有相同的签名，但定义了不同的ab-type类型，因此用户不会错误地混淆对象级别的type和term变量。每个抽象都产生两种类型，一种是抽象的，一种是透明的。例如，图6的lambda类型在图9中产生了抽象类型opaque lambda，其实际定义不公开，以及透明类型lambda，它是原子和表达式对的同义词抽象被向下转换为它们的抽象版本：例如，在图9中，数据构造函数ELAambda携带一个opaquelambda类型的参数。因为opaque lambda是一种抽象类型，所以这种类型的值不是di-F. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）2743正确使用。利用它的唯一方法是程序员显式调用函数open lambda，也是由Cα ml生成的，这将它变成一个透明的形式。无论何时调用它，open lambda都会产生一个新的原子a，并返回一个抽象的透明副本，其中绑定的原子一直被替换为a。该语义与Fresh Objective Caml的语义相同[32]。它自动执行Barendregt相反，为了将一对原子和一个表达式转换为opaque lambda类型的值，必须通过函数create lambda。5.3多个代码经验表明，在打开抽象时自动“刷新”绑定原子可以避免许多显式重命名操作的需要。然而，在有些情况下，必须明确处理姓名和改名问题。Cα ml自动生成代码，用于计算项的自由或束缚原子的集合，以及对项应用替换（原子替换原子）。Cα ml还生成遵循经典访问者设计模式的面向对象代码[4]，并帮助简洁地定义术语上的转换和遍历。生成的map类提供了一个方法集合（每个类型、数据构造函数或绑定规范中出现的记录字段一个）。这些方法中的每一个都返回其参数的深层副本，并通过对类的其他方法的自调用来实现这使得定义行为“几乎像”身份的变换特别容易例如，在图6中指定的语言的情况下，通过重写单个方法，即处理数据构造函数EVar的方法，实现了避免捕获的变量表达式替换。这需要不到10行用户编写的代码，无论规格的大小生成的类fold为定义遍历提供了类似的功能。5.4评论原子在内部表示为整数和标识符对整数单独代表原子原子的整数标识在需要时是原子集和原子上的映射表示为Patricia树[18]以提高性能。44F. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）27原子对原子的替换被急切地应用于所有节点，除了在抽象节点，在那里它们被挂起直到抽象被打开。这种惰性方法允许在抽象从未打开时保存工作更重要的是，它允许多个替换，包括打开抽象时所需的这有助于避免对单个术语连续应用多个替换特别是，遍历一个术语，在遇到抽象时打开相比之下，当前在Fresh Objective Caml [29，30，31]的急切方法导致二次时间复杂度。当然，暂停替换的想法并不新鲜：例如，参考Nadathur和Qi [16]或Shinwell [29，第162页]。全局整数计数器用于在需要时产生新原子。这是由生成的代码维护的唯一全局状态。可以预期，在任何时候，计数器的值都大于存在的任何自由原子的值。然而，如果计数器的值恰好小于一个束缚在一个项内的原子的值，那么它是完全好的。实际上，获取这样一个原子的唯一方法是打开封装它的抽象，但是这样做会导致它被一个新的原子替换，所以实际上没有办法观察到它。这句话有一个重要的实际后果：它意味着将输出值和输入值，Objective Caml的原始编组和解组操作，应用于一个没有自由原子的封闭项是好的Cα ml不支持处理未显式绑定的名称，例如Objective Caml中的记录标签和模块名称，或Java中的包和类名这些名称不受α转换的影响，因此唯一需要解决的问题是效率问题：例如，人们可能希望在内部将它们表示为整数这很容易使用全局状态（破坏了输出值和输入值的兼容性）或Garrigue风格的固定哈希方案进行手工编码[8]。6相关工作6.1规范语言在文献[25，11，34，29]中发现的许多特定语言的表达能力都不如本文中提出的语言特别是，它们要么根本不能处理，要么不能优雅地处理对象级别的结构，比如let和letrec，它们绑定了可变数量的名称。同样的限制存在于Talcott的“绑定结构”[ 33 ]中然而，塔尔科特F. Pottier/Electronic Notes in Theoretical Computer Science 148（2006）2745在某些方面比这里介绍的更有表现力。事实上，它的这会带来一些我们认为不必要的额外灵活性。在这里，内部编码的是完整的束缚原子集合，外部编码的是空集，没有其他集合可以表达。最新版本的Fresh Objective Caml [30] o编译器限制了抽象类型，其形式为：|s=t2，其中t1和t2是类型，s是排序。这个想法是，所有出现在左边成员内部的s类原子都被认为是束缚在右边成员内部因此，哪种原子被认为是束缚的是在t1被定义之后的后验相比之下，Cαml两
我的内容管理
展开
