无标记最终风格的模块化、可组合、类型化优化(2019年)

2020-09-28 23:53:17

毕竟,无标记最终嵌入式DSL的优化是可能的,它们是类型化的,并且是明显的类型保留。我们提出了基于求值归一化的优化框架,并证明了无标签最终优化也是模块化的、方便的和可组合的。我们将它们与作为数据类型的熟悉的深度DSL嵌入的优化进行了对比。本页提供的优化实质上是术语重写。后续课程基于计算而不是重写,以语义风格开发优化。

(领域特定的)语言(DSL)在宿主语言中的无标记最终嵌入以多个解释器为中心。一个解释器可以简单地计算DSL表达式,而另一个解释器可以打印或进行某种类型的静态分析。在这种方法的任何演示中都不可避免地被问到一个问题,那就是如何处理不被认为是解释器的操作,这些操作不能(容易)表示为叠加在DSL表达式上。典型的例子是优化,它以上下文敏感的方式重新组织代码。本文将不仅证明无标记最终DSL的上下文敏感转换是可能的--这样的优化是模块化的、方便的和可组合的。它们也是类型化的和类型保留的,这不仅对我们,而且对编译器都很清楚。当我们使用新的表达式形式(如一类函数、条件、异常等)扩展DSL时。我们仍然可以按原样使用以前编写的优化。许多优化,例如算术表达式简化,只处理语言的一个子集。无标记-最后的方法让我们简洁地表达它们,从语言中不相关的部分中抽象出来。优化不仅更加清晰,而且在语言扩展方面也很健壮,适用于任何扩展语言。与``深度嵌入相比,我们将清楚地看到无标记最终DSL嵌入的优势,即在宿主语言中将DSL表示为数据类型(AST)。可扩展性并不是唯一的优势。虽然优化是AST转换,但是每个优化都喜欢自己的AST形式。(抽象语法树可能有几个微妙的不同实现,我们稍后会看到。)。无标记最终框架允许每个优化使用其自己首选的ASTview。本文是作为无标记最终优化框架的教程编写的,并使用了一个非常简单的示例。该框架已成功地应用于编译和优化语言集成查询的复杂的实际应用中。虽然本教程使用OCaml,但也可以用Haskell表示。

OPTIMIZATION_Intro.ml[13K]本教程的完整OCaml代码-Haskell和OCaml中的最终系统优化:教程无标记-最终风格的优化教程的扩展版本-带有不同的运行示例:逻辑电路的DSL。该教程已在Haskell和OCaml中提供。最后,安全可扩展和高效的语言集成查询将该框架应用于实际项目中,如组合和可扩展的语言集成查询,将用户合成的查询表达式优化为生成高效SQL(不嵌套子查询)的形式。无标记-最终优化,代数上和语义上的后续教程,强调优化的语义、它们的正确性和计算,而不是重写。

本节简要介绍无标记最终方法,解释如何嵌入DSL并编写其解释器和转换器。示例DSL是最简单的,后面可以扩展,它只有整数和加法运算,它的抽象语法树可以用以下数据类型来表示:这个数据类型代表了DSL在OCaml中的深度嵌入,这不是我们要走的路。相反,到目前为止,我们介绍了我们语言的两种基本形式的签名:整数文本和加法操作:模块类型SYM=sig type';a repr val int:int->;int repr val add:int repr->;int repr->;int repr end。

这里,(目前,抽象的)类型代表某种语言表达式的表示形式,由表达式类型来索引。人们可能认为SYM将DSL语法指定为上下文无关的语法:只需将int repr读作“开始符号”,而val int和val add读作标记为int和add的两个结果即可。我们不需要知道什么是REPR来编写示例DSL表达式,例如:MODULE EX2(i:sym)=struct open I let res=add(add(Int1)(Int2))(add(Int3)(Int4))end。

(如上所述,名称i将用于通用解释器,即SYM的实例。)。为了计算该表达式,我们为它编写了一个解释器:模块Ru=struct type';a repr=';a let int x=x let add=(+)end。

T

NEG用另一个解释器(我们将只调用F)来解释DSL,从表面上看,NEG是解释器转换器。从双重意义上说,它也可以被视为表达式转换器:Ex2Neg具有与原始EX2相同的类型:给定一个解释器SYM,它在该SYM的域中计算其DSL表达式的表示法。也就是说,Ex2Neg是DSL表达式的无标记最终表示--即被否定的表达式。它可以用现有的Ru和Sh解释器解释,甚至可以用Neg解释器解释(即可以再次否定):设M.Res-10中的模块M=Ex2Neg(Ru);M.Res"中的let模块M=Ex2Neg(Sh);((-1+-2)+(-3+-4))";M.Res 10中的let模块M=Ex2NegNeg(Ru)中的let模块Ex2NegNeg(F:sym)=Ex2Neg(Neg(F。

(计算结果以缩进形式显示在每个表达式的下方。)。在接下来的文章中,我们将编写更多这样的DSL转换器--这些解释器不仅计算或打印表达式,而且通常以上下文相关、明显非组合的方式重写表达式。

在介绍优化框架之前,让我们使用部分求值的标准技术编写一个简单的独立优化。该优化方案虽然易于实现,但不易扩展,更难与其他方案相结合。我们稍后会在框架内重新实现它,看看缺陷是如何纠正的。样本优化很简单:应用加法x+0=0+x=x的代数定律来消除加法到零。为简单起见,我们假设所有整数文字都是非负的。对于读者来说,消除这一假设是一种练习。该优化被表示为在部分已知值域中的解释,跟踪和传播可用静态信息。在我们的例子中,此信息是该值是否静态已知为零。模块SuppressZeroPE(F:sym)=struct type';a repr={dynamic:';a F.repr;KNOWN_ZERO:BOOL}let int x={dynamic=F.int x;KNOWN_ZERO=(x=0)}让add e1 e2=Match(e1,e2)with(*add is not recursive!*)|({KNOWN_ZERO=TRUE},x)->;x|(x,{KNOWN_ZERO=TRUE})->;x|({dynamic=x},{dynamic=y})->;{dynamic=F.add x y;KNOWN_ZERO=FALSE}结束。

作为部分已知值的典型,REPR有两个组成部分,动态部分是源F解释器要解释的(转换后的)表达式。因为这个解释器在这一点上是抽象的,所以对F.repr一无所知。Repr的第二个分量告诉我们这个部分已知的值是否确实是完全已知的,即为零。我们在解释文字上已知的DSL整数文字时发现了这一点,加法的解释传播了这一知识,并以直接的方式应用了代数定律。让我们花点时间来说服自己,口译员的归纳结构使结构归纳证明变得简单明了。首先,我们需要一个引理,如果e是一个reprr类型的值,并且e.nowled零为真,则ere0表示零。证据是微不足道的。如果E是表达式的无标记最终编码,而I是么半群加法定律成立的解释器,则E(I).res和E(SuppressZeroPE(I)).res.dynamic具有相同的值,即E(I).res和E(SuppressZeroPE(I)).res.dynamic具有相同的值,即E(I)是表达式的无标记最终编码,而I是其中的么半群加法定律成立的解释器。我们还可以证明一个更强的性质:如果e是一个epr类型的值,则它表示零当且仅当e.KnowledZero为真。该定理对于基本情形int x明显成立,在归纳情形add e1 e2中,我们将归纳假设应用于e1和e2以及文字非负的假设。更强的属性要求优化的完备性:如果e是类型为repr的值,则e.dynamic表示没有加法为零的表达式。我们鼓励读者写出详细的校样,也许可以在他们最喜欢的校对助手的帮助下。以下示例将演示优化:MODULE EX3(i:sym)=struct open i let res=add(add(Int 3)(add(Int 5)(Int 0)(add(Int 1)(Int 0))end。

对其进行优化,然后让Sh解释器打印出M.Res-:int SuppressZeroPE(Sh).repr={SuppressZeroPE(Sh).dynamic=";((3+5)+1)";已知_ZeroPE(Sh)中的let模块M=Ex3NoZerosPE(Sh)中的let模块Ex3NoZerosPE(F:sym)=EX3(SuppressZeroPE(F))=EX3(SuppressZeroPE(F));";KNOWN_ZeroPE(Sh)=FALSE}。

优化起作用了:零个召唤消失了。OCamloutput还显示了问题:打印的是部分已知值。这些值在优化过程中使用;最后我们只想要最终结果。应该有一种方法来观察优化结果,并让用户省去优化器的内部细节。第二个问题是可扩展性:如果我们用一流的函数来扩展我们的DSL,我们同样必须扩展SuppressZeroPE来解释SuppressZeroPE(Sh).repr域中的新表达式形式(函数抽象和应用程序)。这个

让我们再次回想一下预热部分中的SuppressZeroPE优化器:SuppressZeroPE(F)将DSL表达式解释为包含F.repr的数据类型的值,即某个F解释器中的表达式解释(计算优化的表达式)。此外,reprr还包含优化过程中使用的额外数据。零消除优化计算DSL表达式,因此构建一个自下而上的repr。动态部分为优化的F解释,最后提取动态部分。以下捕获了两个表达式表示的模式,其中一个包含用于优化的额外数据:模块类型Trans=sig type';a from type';a term val fwd:';a from->;a from->;a term(*Reflation*)val bwd:';a term->;';a from(*reation*)end。

FROM类型是FROM解释器中DSL(子)表达式的表示形式;您可以将其视为到目前为止的优化结果。由于From解释器是抽象的,因此对From值一无所知,因此无法检查它们。类型';a项表示相同的DSL(SUB)表达式;它也是目前为止的优化结果。与FROM不同,术语的值是已知的,至少在一定程度上是已知的,并且可以检查。这些值包含优化的工作数据及其状态。优化过程自下而上地构建术语值,检查那些已经优化过的子表达式。接下来的两个部分显示了示例。通过操作fwd和bwd,这两个表示是相关的。后者特别用于从工作数据中提取优化结果的每一端。操作FWD构建工作数据。这两个运算通常不定义双射:通常fwd不是满射的,bwd也不是内射的。也就是说,虽然BWD的成分。Fwd应该是身份,fwd。BWD通常不是。人们可能会认为bwd是一个“抽象函数”:它丢弃了优化过程中内部使用的数据,即优化状态。则fwd是具体化函数,其将OptimizationState初始化为某个缺省的空值。这篇作文是fwd。BWD不是身份,因为丢弃的优化状态通常比缺省状态更丰富。这两种类型及其相互关系使人联想到评价化(NBE)。在NBE中,形式将被称为不透明对象表示;然后术语将是元语言表示,这是(非标准)评估的领域。那么函数fwd就是反射,而bwd就是物化。为了完成框架,我们定义了一个默认的泛型优化器:给定Trans的一个特定实例(我们为此类实例保留了名称X),优化器将构建一个自下而上的术语,从中可以提取或观察到From值。模块SYMT(X:TRANS)(F:SYMOBS with type';a repr=';a X.from)=struct open X type';a repr=';a Term type';a OBS=';a F.obs let int x=fwd(F.int x)let add x y=fwd(F.add(BWD X)(BWD Y))let Observate x=F.Watch(BWD X)end。

读者可能已经注意到,这个优化器就是愚蠢的身份转换器:由fwd初始化的优化状态没有任何用途,稍后被bwd丢弃。因此,SYMT优化的EX2与原始EX2相同:准确地说,M.观察M.Res中的模块M=EX2(SYMT(X)(I))对于任何X和解释器I都将始终与M.Res中的模块M=EX2(I)相同。具体的优化器被构建为SYMT的增量,覆盖某些DSL形式的解释并实际使用优化状态。与优化无关的其他形式的解释仍然是同态的。下面是示例。

Peter Dybjer和Andrzej Filinski:规范化和部分评估,G.Barthe等人。(编):应用语义学,LNCS 2395,第137-192页,2002年。

为了展示优化框架,我们从预热部分重新实现了优化,将添加部分消除为零。在框架内定义优化过程意味着指定两件事。首先是优化状态,即控制优化的数据。它们是通过编写Trans.Next的实例来定义的。接下来,我们需要说明如何使用这种优化状态并实际执行优化。它被指定为“部分解释器”:仅用于那些受优化影响的DSL形式的解释器。我们将把这第二部分称为iDelta。将这两个部分放在一个函数器中很方便,因为它们都是由from解释器参数化的,该解释器解释优化的表达式。在零添加消除的情况下,优化过程如下所示。模块SuppressZeroPass(F:Sym)=struct模块X=struct type';a from=';a F.repr type';a Term=|Unk:';a From->;';a Term|Zero:Int