构造函数演算中的多态命令和就地更新

理论计算机科学电子笔记91（2004）195-211www.elsevier.com/locate/entcs多态命令：就地更新C. B. 杰伊1H 。Y. 鲁二Q T.阮3澳大利亚悉尼科技大学信息技术学院摘要构造函数演算支持在任意数据类型（包括抽象数据类型）上定义的通用操作。本文扩展了基本的构造函数演算来处理构造位置。由此产生的演算能够定义一个通用的赋值操作，该操作在适当的时候就地执行，否则分配新的内存。这种方法可以消除许多与高阶多态语言相关的空间开销。结合现有的泛型编程技术，它可以表达一些非常强大的算法，如访问者模式。关键词：泛型函数，构造函数演算，命令式编程，就地更新，位置构造函数1介绍函数式编程最大的优点之一是它减轻了程序员管理内存的需要，这有助于使程序更短，更容易推理。代价是它们的编译器必须采取保守的内存分配方法，通常在堆中分配新空间，并在就地更新完全安全时垃圾收集旧空间。1电子邮件：cbj@it.uts.edu.au2电子邮件：helenlu@it.uts.edu.au3电子邮件：qtnguyen@it.uts.edu.au1571-0661 © 2004由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2003.12.013196C.B. Jay et al. / Electronic Notes in Theoretical Computer Science 91（2004）195-已作出重大改进以提高此过程的效率。例如，编译[11]中的类型使用类型信息来确保某些就地更新的安全性。这对于由简单类型构建的整数、浮点数和元组很有效，但不能处理递归类型，如列表，其中类型不确定其值的形状。 监测 列表长度等可以尝试使用大小类型[4]或其他依赖类型系统，例如[13]，目的是提取编译时信息。本文提供了一种赋值方法，该方法能够在运行时确定是否使用来自构造函数演算的现有技术就地赋值[5，6]。这是一个变种的的Aidda演算，支持强大的泛型编程[2，7]通过程序扩展的基础上模式匹配的构造器的任意类型。它能够为通常的二阶函数表达通用程序，如映射和折叠。它还可以很容易地扩展数字运算，如等式和加法，从原始数据类型（如原始整数或整数）到任意数据类型。这里使用相同的方法将位置上的原语操作扩展到构造位置上的泛型操作。当泛型赋值以这种方式定义时，就地更新是规范，基于位置的结构与其新值的结构的匹配。我们可以将原语赋值与泛型赋值结合起来，以获得两全其美的效果，尽可能实现完全的安全性和就地更新。三个例子被用来说明这种方法的一些好处insertionsort程序展示了如何使用高阶函数和模式匹配来编写空间效率程序该程序收敛显示了如何在有效利用空间的情况下对函数进行迭代。访问者程序将访问者模式[3]捕获为类型访客：name（X，Y）→（locY→）→locZ→其操作如下：访问者nfz遍历z的结构将f应用于由n命名的任何子结构。例如，n可以表征员工，f可以增加组织内员工的工资。本文其余部分的结构如下。第2节回顾了构造函数演算的关键方面。第3节将位置类型添加到基本演算中，并为它们的创建，读取和写入提供了一些原始操作。第4节介绍了施工地点和相应的操作。第5节提供了实例。第6节得出结论并考虑今后的工作。C.B. Jay et al. / Electronic Notes in Theoretical Computer Science 91（2004）195-1972构造函数演算（Constructor Calculus）在[5]中引入的构造函数演算是为了支持映射和折叠等通用函数的定义而创建的，其中参数和返回值的类型可以为各种数据库实例化。由此产生的定义允许这些函数能够作用于一大类数据集。在[6]中进一步发展了这项工作，它解释了本文中使用的任何未定义的符号。 后者还展示了如何用Hindley-Milner类型系统来证明关键思想，该系统的一个简单变体具有类型T和由下式给出的项t：T：：= X|D|1 |TT|T→ Tt：：= x|D|联合国|对|tt| λx.t|iftthentelse|设x=tint|fix.X是类型变量，D是类型常数，1是单位类型，T0<$T1是T0和T1的乘积，T0→T1是从T0到T1的函数的类型。在微积分中添加余积（或和）类型是一件小事，但是我们将看到它们可以通过允许数据类型定义来处理。术语形式分别表示变量、常数、单元类型的唯一值、配对、应用、抽象、条件、let声明和定点。构造函数演算是通过将条件替换为更强大的分支构造（称为扩展）而创建的。其语法c项下适用f，否则g其中c是构造函数，f和g是术语，称为专门化，默认函数。 扩展的重写规则是（undercnapplyfelseg）（cnt0. tn−1）> ft0. tn−1（undercnapplyfelseg）t > g tother其中cn表示接受n个参数的构造函数。从这些规则中可以清楚地看出，f可能有一个比g更特殊的类型，因为它只需要作用于构造函数c的参数。这是与条件句（或情况分析）的关键区别，条件句中的两个分支必须具有完全相同的类型。扩展的类型推导规则由下式给出：cn：1000c. T0→. . . →Tn Γg：T→TJn= U（Tn，T）n r nf：n（T0→. Tn−1→TJ）在cn下应用felseg：T→T J198C.B. Jay et al. / Electronic Notes in Theoretical Computer Science 91（2004）195-其中，Γ是术语上下文，U是最一般的单位符。这是很重要的一个类型的一个功能的 空 间 空 间 化 没 有 这 种 类 型 的 化 学 物 质。T0→. . . →Tn应为c的主型概型，即与生俱来的因为专门化函数必须能够作用于由C构造的任何项的子项。也就是说，专门化可以假设Tn和T的最一般的统一，但不能再多了。由于上述限制，我们将自己限制在构造器常数的有限集合上。基本的例子有un，pair和多态异常exn：X→Y其他示例将通过数据类型声明添加。能够将加法和等式等数值函数扩展到任意数据类型是很有用的。要做到这一点，需要与整数和整数匹配的模式。一种方法是将整数和浮点数视为由某种类型的原始整数和原始浮点数构造的值，例如比特元组。由于在编程语言中暴露这些是令人不愉快的，我们将采用不同的方法，即为每个原始数据类型引入新的术语形式，例如，对于浮动点数，可以有用类型推导规则under unusual applyfelsegT→TJ和评价规则=U（在非线性条件下应用felseg：T→TJ（under numeroat applyfelseg）n >fnifn is a numeroating pointnumber（在“applyfelseg”之下）t > g t，如果t不能是一个重复的点数。可以写under unusual applyf elseg对于under degenerate，适用felseg。类似的规则和约定也适用于整数类型int和其他数据类型。作为句法糖，我们也可以写将t1与t对于t t1，特别是当t由模式匹配给出时。C.B. Jay et al. / Electronic Notes in Theoretical Computer Science 91（2004）195-199我们可以使用模式匹配语法来表达扩展，其中模式| c x0... xn−1→t表示在c下应用λx0，. xn−1.telse同样地，| 振荡x → t表示在λx下应用λx，否则... . 模式匹配中的最终默认函数由异常常量exn给出。例如，这里有一个等式函数，它作用于任意的浮点数元组（tuple xiaoatequal：X→X→bool）=| y→ x = y）|float y → x = y)| un →λy。真| pair y 0 y 1 → tuple punchoatequal x 0 y 0 tuple punchoatequal x 1 y 1）在实践中，人们希望创建抽象数据类型并使用它们的punchc-|pair y0y1→tuplefloatequal x0y0&&tuplefloatequal x1y1) In practice, one wishes to createabstract data types and use their construc-tors，在定义泛型函数时也称为抽象器比如说，数据类型复合体=复合体和复合体引入复数作为一种新的抽象器，可用于定义新的操作。如果抽象器被视为原语，那么现有的泛型函数（如相等）必须扩展case以处理每个新的抽象器。相反，使用抽象器构建的术语被赋予一个具体的表示（反映其深层结构）作为参数元组（使用pair和un构建）。然后用一个名称（代表表面结构）标记它。类型的构造函数标记标签：X，Yname（X，Y）→X→Y其中name（X，Y）是一种名称类型。例如，complex可以解释为λx，y。标记复合体名称（对x y）其中，复合体名称：名称（复合体，复合体）。 任意抽象词的比较是通过对它们的名字进行模式匹配来实现的。准确地说，这需要一个额外的类型派生规则，即n：name（X，Y）g：T→TJn=U（name（X，Y），T）f：n（TJ）► undern applyf elseg：T→TJ因为名称常量必须具有常量类型，所以保持了类型安全。200C.B. Jay et al. / Electronic Notes in Theoretical Computer Science 91（2004）195-因此，数据类型的完全泛型相等由下式给出：（equal：X→X→bool）=| inty → primintequal x y）|int y → primintequal x y)|（xy → x y）|float y → primfloatequal x y)| un →λy。真| 对y 0 y 1 →等于x 0 y 0等于x 1 y 1）|pair y0y1→ equalx0y0&&equal x1y1)| tag m x → (| tag n y → (与...相配| m →等于x y|→false))|→ λy. 假例如，equal（complex 3. 三四。4）（复合体3. 三十五。（5）减少应用在复合名称下应用相等（对3. 三四。4）（对3. 三十五。5）else λy. 假复杂的名称，最终减少为假。同样的方法可以用来推广其他数值运算，例如添加到任意数据结构。如果需要，这些通用操作可以定制例如，复数的乘法可以给出它自己的情况。3位置本节以类似于ML [10]的风格向构造函数演算添加了一些命令式特性。在这种设置中，赋值可以被视为一个原子操作，它很容易描述，但空间很大命令的类型“命令”配备了两个常量skip：跳顺序：X→ X。命令skip没有效果。seqt0t1形式的项的求值执行命令t0，然后对项t1求值。我们可以写x; y对于seqx y。While循环和for循环可以通过定点构造来定义，以通常的方式。C.B. Jay et al. / Electronic Notes in Theoretical Computer Science 91（2004）195-201现在让我们考虑可分配的位置。每个类型T都有一个相关联的类型位置T存储类型T的值的位置。位置支持三个多态常量：primloc：X→locXprimval：locX→X初始符号：locX→X→ X。形式为primloct的项创建一个位置，其初始值为t.形式为primvalu的项表示存储在u处的值。形式为primassignu t的项用t的值更新位置u。需要垃圾收集来恢复冗余位置。一般来说，必须限制出现在位置类型中的类型变量的量化（参见[8，12]，但这并不限制本文中示例的多态性。图1中的评估规则采用了一个大步操作语义。值（元变量v）由抽象、扩展、构造函数、常量和形式为d v0.的项给出。其中d是没有显式求值规则的构造函数或常数。 这样的规则被总结为评估d d0的 规 则 。图中的n-1。存储（元变量）是从位置类型的术语变量到值的函数。这些term变量必须是location类型，并且将由元变量u表示。 一个求值上下文是一对（t，t） 其中项t的所有自由变量都在存储器的域中评价是用以下形式的判断来表示的其中（k，t）是评估上下文。大多数评价规则都是标准的。请注意，beta还原是急切的。例如，（t，primassignt0t1）的计算方法是首先计算t0。如果它的值是标识符u，则u的值在存储器中更新为计算t1的结果。然而，如果t0具有其他值，例如异常，则评估的结果是异常。定理3.1对于每个求值上下文（t，t），存在可以应用的求值规则。也就是说，评价永远不会停滞。证据 证明是通过归纳的结构t。Q评估规则没有给出存储操作将如何进行的指示202C.B. Jay et al. / Electronic Notes in Theoretical Computer Science 91（2004）195-切实贯彻人们期望像整数或浮点数这样的数据值的分配将就地执行，而函数的分配将通过分配新的内存来执行。微妙的情况是分配结构化数据，如列表。定义列表类型数据类型列表X = nil| X的缺点：列表X并采用通常的函数语法来表示它们，例如[1， 2， 3]表示cons1（cons2（cons3nil））。现在考虑这个例子让x=primloc[1]在[2];（1）primassignx [8，9].显然，第一个赋值可能已经到位，但是任何简单的primassign实现都将错过这个机会，因为它无法将这种情况与第二个形状变化的赋值区分开来。4位置构造函数当位置的结构与其新值的如果位置的构造方式与其值的构造方式相同，则可以通过比较构造函数来检查是否匹配本节介绍一个新的构造函数类，位置构造函数。它们可用于创建通用函数，用于基于其原始版本进行定位、赋值和赋值，就像equal基于数据相等一样。在此设置中，赋值可以被视为一个通用操作，如果可能，可以就地执行，否则创建一个新位置对于每个构造函数c：T0→. → Tn关联位置构造函数类型的连接conlocc：locT0→. →loc Tn.图2中给出了与位置构造函数相关的两个新的计算规则。 他们为已建地点创建标识符，并提供使用它们的扩展的专门化规则（默认规则不变）。注意，定理3.1仍然适用于这个增广系统。还要注意的是，如果c是一个抽象器，那么用于给c一个具体表示的技术必须适用于conlocc。通用函数loc为构造项创建构造位置，否则为例如函数、命令和位置创建C.B. Jay et al. / Electronic Notes in Theoretical Computer Science 91（2004）195-203（，t[v0/x]）（J，v）（λ，（λx.t）v0）<$（λJ，v）（，t（fixt））（J，v）（，fixt）（J，v）（n，t0）<$（nJ，v0）（nJ，t1[v0/x]）<$（nJJ，v1）（n，letx=t0int1）<$（nJJ，v1）（，t0v0. vn−1）<$（<$J，v）（c n下，应用t0elset1到（cnv0. vn−1））<$（<$J，v）（，t1v2）（J，v3）（n，undercnapplyt0elset1tov2）n（N，v3）（，exnt0t1）（，exnt0）（，v（exnt））（，exnt）（，d d0···dn−1）<$（，dn）d d0···dn−1=dn（，seq skipv）（，v）（，primlocv）（，u<$→v，u）ufresh（，primvalu）（，（u））（，primvalv）（，exnv）（，primassignu v）（，u<$→v，skip） （n，primassignv0v1）n（n，exnv0）（，v），v）（，t0）（J，v0）（J，t1）（JJ，v1）（jj，v0v1）（JJJ，v2）（，t0t1）（JJJ，v2）自己其定义为：Fig. 1.评估规则（loc：X→locX）=| un → conloc un| pair x 0 x 1 → conloc pair (loc x 0) (loc x 1)| tag m x 0 → conloc tag (primloc m) (loc x 0)| x → primloc x204C.B. Jay et al. / Electronic Notes in Theoretical Computer Science 91（2004）195-（，conlocc nu0. u n−1）<$（n，u<$→conlocc nu0. u n−1，u）ufresh（，t0u0. u n−1）<$（<$J，v）（c）n 应用t0elsettou）（J，v）（u）= conlocc nu0. n −11图二. 评价已建地点同样，通用估值函数为（val：locX→X）=| conloc un →un| conloc pair x 0 x 1 → pair (val x 0) (val x 1)| conloc tag m x 0 → tag (primval m) (val x 0)| x →原始x泛型赋值函数assign遵循与其他函数相同的基本模式，但接受两个参数。assign的定义可以是（assign：locX→X→X）=| un→ skip）|un →skip)| 对y 0 y 1 →赋值x 0 y 0;赋值x 1 y 1）|pair y 0 y 1 → assign x 0y 0; assign x 1 y 1)| conloc tag m x → (| 标签N Y →将原始m与| n →赋值x y|→ let u = conloc tag m x in primassign u (tag n y))| x → primassign x如果这个位置是由primloc创建的，那么将调用primassign。否则，assign将尝试将位置构造函数与新值的位置构造函数相匹配。匹配可能失败的唯一情况是当位置和术语被标记为不同的名称时，例如。中的指派设x=loc[1， 3， 5]，[2， 4， 6];C.B. Jay et al. / Electronic Notes in Theoretical Computer Science 91（2004）195-205将成功地就地更新整个结构，但是在赋值x[2， 4，6]时设x=loc[1，3];将首先将前两个列表条目的位置更新为2和4，但随后无法将nil name与cons name匹配。这里有一些糖语法是很方便的：let！x表示valx，x：=y表示assignxy。下面是我们前面的例子（1），它被修改为使用构造位置：letx=loc[1]inint [2];x：= [8，9]。现在，第一个赋值已经到位，第二个赋值也成功了。因此，赋值操作现在是一个通用函数，可以在合理的时候就地执行，否则分配新的内存。5示例本节使用三个例子来说明高阶函数和模式匹配如何与就地更新、用户控制的类属函数和泛型函数相结合，以生成简短、有表现力、高效的程序。5.1插入排序插入排序的工作原理是递归地将元素插入到排序列表中。下面是一个作为一对纯函数程序的实现。插入由（funinsertion：（X→X→bool）→X→listX→listX）g x=| nil →[x]| consh t →如果g × h然后consh（funinsertiong x t）else consx（consh t）206C.B. Jay et al. / Electronic Notes in Theoretical Computer Science 91（2004）195-然后递归地使用funinsertion在（funinsertionsort：（X→X→bool）→listX→listX）g=| 零→零| cons h t → funinsertion g h (funinsertionsort g t)该算法使用与列表长度的平方成比例的空间。下面的命令式算法insertionsort具有类似的结构，但仅使用恒定数量的新内存（当执行交换时）。（swap：locX→locX→loc）x y=让t =！xinx：=！y; y：= t（插入：（X→X→bool）→locX→loc listX→Bool）g x=| conloc nil →skip| conloc consh t →如果g！x的！H然后交换x h;插入g h t否则跳过（insertionsort：（X→X→bool）→loc listX→loc）g=| conloc nil →skip| conloc cons h t → insertionsort g t; insertion g h t这个程序的缺点是，当结构很大时，执行赋值可能很昂贵。解决方案是将多态插入排序实例化为位置的类型locY，以获得类型（locY→locY→bool）→loc list locY→Bool它可以很容易地被修改，insertionsort：（Y→Y→bool）→lock list lockY→lock这将使用更高效的交换。C.B. Jay et al. / Electronic Notes in Theoretical Computer Science 91（2004）195-2075.2收敛下面定义的函数收敛迭代函数f：X→X，直到结果稳定，即直到应用于旧值和新值的某个测试t：X→X→bool变为真。这反映了一种常见的情况，模拟某些系统向稳定状态的演化，例如Barnes- Hut算法[1]。（收敛：（X→X）→（X→X→bool）→X→X）ft x=让y=锁定xletz=loc（fx）inletb=loc false in whilenot（t！y！z）做b：=（不！b）;如果！B那么y：=（f！（z）否则z：=f！ydone;！y位置的使用允许程序员指出X类型需要两个位置，而不是一个无限的数字。此外，如果可能的话，分配将就地完成，只有在必要时才分配新的内存有许多例子表明，这将产生重大的好处。例如，通常使用由行为具有近似相等复杂性的区域构建的结构来表示复杂的动力系统。如果区域是安静的，则其表示保持其形状，并且就地更新成功。相反，如果一个地区是多事件的，那么它的代表的形状很可能会改变，并需要新鲜的记忆。5.3访问者访问者模式[3]描述了遍历（和更新）数据结构的过程。这可以在Java中通过从Walkabout类[9]中子类化来完成，Walkabout类使用反射来确定必要的结构。构造函数演算通过其强大的模式匹配方法支持单个泛型访问者与插入排序一样，我们将检查函数208C.B. Jay et al. / Electronic Notes in Theoretical Computer Science 91（2004）195-和命令式的算法（funvisitor：name（X，Y）→（Y→Y）→Z→Z）m f=| pair z0z1→ pair (funvisitor m f z0) (funvisitor m f z1)| tag n z0 →(与...相配| m → f (tag n z0)|→ tag n (funvisitor m f z0))| z → zfunvisitorn f z查找z的由n命名的子结构并将f应用于它们。它可以被看作是一种映射。与插入排序一样，该算法在空间使用上是二次的。相比之下，（命令式）访问者只需要恒定的空间。（visitor：name（X，Y）→（locY→）→locZ→）m f z=匹配z与| conloc pair z0z1→ visitor m f z0; visitor m f z1| conloc tag n z0 →(match（primvaln）with| m → f z|→ visitor m f z0)|→skip让我们考虑一个特殊的情况，更新一个组织中的员工的工资。给定一种工资数据类型salary=雇员的工资以及工资更新功能（改变工资：薪水→工资→工资）k=|工资y→工资（ky），我们可以定义（改变工资：最低工资→Z→Z）k=funvisitor工资名称（更改工资k）。C.B. Jay et al. / Electronic Notes in Theoretical Computer Science 91（2004）195-209例如，如果我们定义一种类型的大学，数据类型string=列表字符串datatypesta name=sta name of stringdatatypestaname=sta name of sta name andsalarydatatypedepartment=department of list staname数据类型university=university of listdepartment然后设部门1 =部门[员工（员工名“Barry”）（工资12. 0），海伦（Helen）（薪水13. 0），STA（STA名称“托尼”）（工资14。[2]工资变动。0部门 1计算结果为部门[职员（职员名“巴里”）（薪金24. 0），海伦（Helen）（薪水26. 0），28岁的托尼（Tony）（薪水28. 0）]。这种方法的优点是双重的。第一，不需要编写嵌套模式来表示部门等;第二，访问者可以在大学结构发生任何变化后重用，例如。或者是建立在完全不同的组织结构上。同样，如果我们定义（变更工资：最低工资→最低工资→最低工资）k=| conloc salary y → primassign y (k ∗ (primval y))然后（更新工资：最高工资→最低工资→最低工资）k=访客工资名称（更新工资k）将更新工资。6结论构造函数演算提供了一种强大的技术，可以用一些简单的210C.B. Jay et al. / Electronic Notes in Theoretical Computer Science 91（2004）195-原始人本文表明，同样的方法可以适用于imperative操作。也就是说，用于创建、读取和写入位置的原始操作可以支持这些操作的通用函数的定义。这种方法最显著的优点是，只要合理，泛型赋值操作就执行就地更新，否则就分配新的内存。据我们所知，这在其他多态语言中还没有实现。通过一些有代表性的例子来展示该方法的表达能力insertionsort程序展示了函数式编程风格及其模式匹配和递归如何收敛程序很好地说明了程序员和系统之间共享控制的价值：程序员指定需要多少数据结构，而系统确定何时需要新的存储visitor程序展示了泛型编程风格的强大功能如何与命令式特性自然结合，从而为大型数据结构提供灵活的编程。本文中的思想和例子表明，构造函数演算能够将函数式和命令式编程风格结合在一个简单的演算中。我们正在研究它与其他编程风格（如面向对象）的相关性。引用[1] 巴 恩 斯 ， J.E. 和 P. Hut ， A hierarchicalO （ NlogN ） force-calculation algorithm 。Nature，324（6270）：446[2] 巴克豪斯河和T. Sheard，editors，Workshop on Generic Programming ：Marstrand ，Sweden，18th June，1998. 查尔姆斯理工大学，1998年。[3] 伽马，E.，R.赫尔姆河Johnson和J.Vlissides，设计模式：可重用面向对象软件的元素。Addison-Wesley，1995年。[4] 休斯河J.M.，L. Pareto和A. Aiken，使用大小类型证明反应系统的正确性。程序设计语言原理研讨会。ACM Press，1996.[5] 杰伊角 B、 区分数据结构和函数：构造函数演算和函子类型。In S. Abramsky，编辑，Typed Lambda Calculi andApplications ： 5thInternationalConfereenceTLCA2001 ，Krako′w ， Polandd ， May2001Proceedings ， 计 算 机 科 学 讲 义 第 2044 卷 ， 第 217-239 页Springer，2001年。[6] 杰伊角B、 构造函数演算。www-staff.it.uts.edu.au/~cbj/Publications/constructors.ps网站，2002年。[7] Jeuring ， J. 编 者 ， Proceedings ： Workshop on Generic Programming （ WGP2000）：2000年7月。乌得勒支大学，UU-CS-2000-19，2000年。[8] 保尔森湖C.的方法，ML for the Working Programmer（工作程序员的ML）剑桥大学出版社，第2版，1996年。[9] Palsberg，Jens和C. 巴里·杰伊，《访客模式的本质》。在COMPSAC'98会议记录C.B. Jay et al. / Electronic Notes in Theoretical Computer Science 91（2004）195-211[10] NEWJERSEY的标准ML，cm.bell-labs.com/cm/cs/what www.example.com/smlnj/。[11] 第三届ACM SIGPLAN编译类型研讨会（TIC 2000），加拿大蒙特利尔，2000年9月21日。www.cs.cmu.eduwww.example.com/~crary/tic00/.[12] Wright，Andrew，Polymorphism for Imperative Languages Without Imperative Types.技术报告TR 93 -200，莱斯大学，1993年。[13] Xi，H.和F.通过依赖类型消除数组边界检查。 《程序设计语言设计与实现》（Proceedingsof Programming Language Design and Implementation，PLDI '98），蒙特利尔，1998年6月第214-227页， 1 9 9 8 年 。