基于论述，一个适合作为文件标题的20字中文标题可以是：“面向对象编程中的访问者模式及其在树状数据结构遍历中的应用”

理论计算机科学电子笔记155（2006）309-329www.elsevier.com/locate/entcs访问者模式彼得·布拉夫斯基1剑桥大学计算机实验室Cambridge CB3 0FD，英国Hayo Thielecke2伯明翰大学计算机科学学院伯明翰B15 2TT，英国摘要在面向对象的语言中，访问者模式可用于遍历树状数据结构：访问者对象包含一些操作，数据结构对象允许自己被接受访问者遍历。在多态lambda演算（系统F）中，树状数据结构可以被编码为多态高阶函数。 本文利用Java中的泛型技术，从多态编码中重构了访问者模式。我们概述了多态编码中的量化类型如何指导对一般访问者的推理。保留字：访问者模式，多态类型，面向对象编程，泛型Java1介绍树状数据结构，如抽象语法树或二叉树，以及它们的遍历（通常称为树遍历）在编程中无处不在。现代函数式语言，如ML和Haskell，以数据类型定义和模式匹配的形式提供结构来处理树1Email：Peter. ca m.a c. uk2电子邮件：H. cs.bham.ac.uk1571-0661© 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.11.061310P. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）以及更一般的递归数据库。然而，在面向对象的语言（如Java）中，情况要复杂得多。测试类成员资格和在其上分支被广泛认为是违反面向对象风格的。相反，访问者模式[6]被提出来定义树状归纳数据集上的操作。使用访问者的最简单的例子是A+B形式的求和类型。由于Java没有sum类型，所以Visitor模式实现了一个类，通过一种双重否定转换来完成sum类型的工作具体地说，类有一个接受访问者的方法;访问者本身有两个方法，一个接受类型A的参数，另一个接受类型B的参数。如果我们采取一种非常理想化的观点，将方法视为函数，将对象视为这些函数的元组，那么我们可以将上述内容视为多态λ-演算[8]中一个众所周知的同构的实例A+B = α（（A→α）×（B→α））→α这些同构在编程语言理论中有着坚实的基础。通过柯里-霍华德对应，它们也构成了高阶逻辑中逻辑连接词（如析取）的可定义性的一个更大图景的一部分本文旨在揭示这一类型论的游客观。具体地说，设计模式（如前面提到的访问者模式），就其本质而言，并不是一个明确的定义，而是各种相关的实例。因此，我们的目标是澄清访问者模式的变体如何与更理想化的类型理论图片相关我们将访问者分类为内部或外部，这取决于访问者本身或树是否指定了遍历。此外，这些可以是函数式的（通过返回值）或命令式的（具有void返回类型和副作用）。访问者模式的变体与alge编码的相似性将类型引入系统F可能是类型理论民间传说的一部分然而，精确地表达这一点似乎非常有用，因为一些技术可能从高度发展的多态lambda演算理论转移我们的观点不是将面向对象的语言翻译成函数式语言，或者相反。相反，我们可以看到，同样的概念在这两个非常不同的场景中都有表现。本文件的贡献包括：• 我们提出了一个程式化的多态λ-演算，使多态编码与访问者的关系更加清晰。• 我们在Featherweight Generic Java中展示了结果访问者的类型可靠性[9]。P. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）311• 我们勾勒出这种抽象的游客的看法可能是有用的推理游客。为了完整起见，附录（A部分）给出了Feath-erweight Generic Java的更多细节.这些细节对于理解这篇论文并不重要2背景我们简要回顾了两个相关背景领域，我们的目标是在这两个领域之间架起桥梁：设计模式文献[6]中提出的访问者和多态lambda演算[7]。我们发现给出一些面向对象的术语是有用的接口定义了一组方法，但没有给出它们的实体。这对应于ML签名。类这对应于ML结构。我们将在全文中考虑泛型Java [3]（Java扩展了类，接口和方法的类型参数）。简单地说，语法如下。类C<α>{...}形式的接口或类定义定义一个类C由类型变量α参数化。 类型C Int>实例化类C的类型参数为Int。本文给出了<α> Tm（...）{...} 定义了一个方法m，其中类型变量α是普遍量化的。形式为o.m< Int>（.）的方法m调用将α实例化为Int。访问者模式的目的是围绕数据类型上的操作而不是构造函数来组织程序访问者模式的典型例子由抽象语法树和编译器的各个阶段对它们的遍历组成;这种方法在SableCC [5]中使用。我们将考虑一个更简单的例子，基于整数叶的二叉树和求和叶的操作。二叉树的标准面向对象实现基于Composite模式[6]。数据类型签名（有时称为该接口包括方法头，该方法头指定对数据的所有操作的签名这迫使每个构造函数类提供一个方法来处理操作的适当情况。这种方法允许在不修改现有代码的情况下添加新的数据类型变体的缺点312P. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）添加新的操作是困难的，因为必须修改每个现有的类。访问者模式扭转了局面。添加新操作变得容易，但添加新变体变得困难访问者模式的使用方法如下。数据类型上的每个操作都被打包到一个具体的访问者类中。处理每个变量的case包含在一个通常名为visitCons的方法中，其中Cons是该变量的构造函数类每个具体的访问者实现一个访问者接口。这指定了访问方法的类型，必须存在于一个具体的访问者。它可以被看作是一个具体的游客签名。数据类型的构造函数类被修改为包含一个accept方法。它的作用是接受一个访问者，并为类实现的变量调用visit方法这本质上是一种对数据类型变量和访问方法的双重分派形式任何存储在类内部字段中的变量组件都必须传递给visit方法。还需要对accept方法和visitor接口进行参数化，因为我们无法预先知道任何具体的visitor类产生的类型。总而言之，访问者模式由以下类组成访问者它为每个Cons类声明名为visitCons的访问方法。ConcreteVisitor它实现了Visitor接口，并且必须为在那里声明的每个visit方法提供实现。数据/元素它声明了一个接受Visitor对象作为参数的accept方法。ConcreteData/ConcreteElement这对应于一个名为Cons的ML数据类型构造函数。它实现了在Visitor对象中调用visitCons的accept方法。访问者模式并没有规定访问者应该在哪里存储中间结果，或者应该如何将结果返回给调用者。我们将区分函数式访问者和命令式访问者，前者通过调用accept的结果返回中间结果，后者在访问者内部的某些字段中积累结果访问者模式的另一个方面是为复合对象选择遍历策略。我们可以把遍历代码放在数据类型中。为此，我们确保在任何组件对象上递归调用accept方法或者，我们可以将遍历代码放在访问者本身中。我们将分别将这些访问者称为P. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）313外部迭代器[6]。我们将使用多态lambda演算（System F）来编码数据类型。事实上，我们需要一个更强大的带有多态类型构造函数的System F扩展，称为Fω，因为它允许我们比单独使用System F更好地近似泛型和接口这个系统的大多数特性对于熟悉Haskell或ML等高级语言的人来说并不陌生：直观地说，Fω包含多态函数和多态类型构造器。图1给出了一个相当标准的Fω有限延拓生产管道 我们假设α∈/Γ是一个不属于自由变量的函数，在Γ中。我们把<$α：：<$.T表示为<$α.T，对Λα：：<$.T也是如此。空产品被写为1。 我们还将投影πit写成ti，对于λx，t为A × B。[a<$→π1x，b<$→π2x]t.3访问者和代数类型编码在本节中，我们回顾系统F [ 14 ]中代数类型的编码（sometimescalledtheBüohm-Berarducciencoding[2]）。其标准描述是用F-代数来表示的。然而，我们发现以稍微不同的风格来呈现它是有用的：虽然与通常的帐户同构，但它使与访问者模式的联系更加明确。3.1内部访客我们考虑代数类型的形式μ α。[α]i∈1.. n并且我们进一步限制注意力到作为递归类型变量α和类型常数的乘积的Fi因此，以这种方式定义的类型是各种形式的树，我们将看到游客是如何走树定义3.1我们将内部访问者定义为形式为A，a ii∈1.. n，其中A是一个类型（称为结果类型），并且a ii∈1. n是函数ai：Fi [A] →A的元组（称为访问方法）。在此条件下，我们可以定义F[X]=Σi∈1。nFi[X]. Vi算子本质上是F-代数，它们的访问方法给出了结构图.接下来，我们考虑代数类型的编码（也就是说初始化F-代数），但在弱初始访客方面改写314P. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）i∈1..n术语种类类型上下文类型t，s：：= x |λx：T.t |TT |Λ α：：K.t |t [T]|tin|πit K：：= π|KKT：：= α|T→T|中文（简体）|Λ α：：K.T|T [T]|i∈1.. nTir：：= 0|r，x：T|Γ，α：：K(Var)x：T∈Γrx：T(Abs)ΓT1：：Γ，x：T1t：T2Γλx：T1.t：T1→T2（应用程序）Γt：T1→T2 Γs：T1T2：T2Γ，α：：Kt：T（TABS） Γε Λα：：K.t：εα：：K.Tα∈/Γ（TApp）Γt：α：：K. T1ΓT2：：KΓt[T2]：[α<$→T2]T1i∈ 1.. nrti：TiI∈1.. nTi（元组） Γt ii∈1.. n：T（投影）Γππt：Tj金丁（TVar）α：：K∈ΓΓα：：K（KAb）Γ，α：：K1<$T：：K2T：：K1<$K2α∈/Γ（KApp）ΓT1：：K1K2ΓT2：：K1T1[T2]：：K2（卡罗）ΓT1：：ΓT2：：T1→T2：：TΓ，α：：KT：：（KAll）Γα：：K.T：：α∈/Γi∈ 1.. nΓTi：：减少（KTuple）i∈1.. nTi *电子邮件（λx：T.t）s~β[x<$→s]t（Λ α：：K.t）[T]~β[α <$→ T] tπj <$t i <$i∈1.. n~βtjJ我P. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）315（Λα：：K. T1）[T2] ~β[α<$→T2]T1316P. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）我我们定义一个对象T如下：T = α。（（Fi[α]→α））→αi∈1.. nT配备了访问方法：consi：Fi[T]→Tc〇nsi=λx：Fi[T]。Λα.λv：（Fj[α]→α）. vi（Fi[λt：T. t[α]v]x）j∈1.. n直觉上，我们认为consi是数据类型T的构造函数。则T具有n次consi∈1.. n在以下意义下是弱初始的。设A与A∈i： Fi [A]→A∈i∈1. n是任何访客。然后有一个从T到A的函数，定义为：λt：T .t [A]<$ai<$i∈1.. n这解释了T的定义：T的任何元素t都有能力接受任何结果为A且访问方法为visiti的访问者，并产生A的元素。T = α。（（Fi[α]→α））→αi∈1.. n`visit[α]x`Visitor[α]x更直观地说，T的元素可以被认为是树;它们使用visit方法递归地将自己折叠成A. 这是通过让访问者访问任何子树来实现的，从而将它们折叠成结果类型的元素，然后为最顶层的节点调用适当的访问方法。consi=λx：Fi [T].接待来访者λv：x（`Fj[α]→α）<$. vi遍历子树（Fi[λt：Tx`. t[α]v]x[α]）constru`ctoobrowsergxumentsj∈1..ncallvis`itmxethod见证T的初始化的访问者态射可以被看作是在T对象上调用accept并传递给它一个具体的访问者：具体访问者^a= λt：T . t[A]¸⟨ai⟩xi`∈1..ncall`acampaignxcept3.2外部访问者外部访问者由一对A，v ii∈1. 其中A是一个类型，vin是函数vi的 元 组 ：Fi [T] → A。注意这个位置的TP. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）317内部访问者会再次出现A。直觉上，外部访问者拥有与内部访问者一样的访问方法;不同之处在于这些方法可以接受类型T的树作为参数，而不是自动将树折叠成结果类型A的元素。我们定义了一个结构S，它以同样的方式接受外部访客，T接受内部的：S = αβ。（（Fi[T]→β））→βi∈1.. n此对象具有访问方法的结构pi ：Fi[S]→Spi= λx：Fi[S]. Λβ。λm：（Fj[T]→β）。mi（Fi[λs：S. s[T]{\displaystyle s[T]}{\displaystyle s [T}{\ n]x）j∈1.. nS上的访问者结构从弱初始访问者T导出一个函数。^p：T→S直观地说，这个映射采用一棵树，并对其进行模式匹配，以便外部访问者可以访问它。外部访问者可以自己使用这个映射来进行子树的进一步模式匹配，从而进行遍历。但是，如果不添加递归，外部访问者就不能遍历任意深度的树。由于整个树的遍历不再像内部访问者那样是内置的，外部访问者将不得不在自己的蒸汽下重复，这需要访问者中的定点组合子4分解编码本节对访客的总体看法如下。我们的目标是通过分解各种翻译，找出访问者模式和System F中的类型编码之间的联系我们提出了一个编码的代数类型到多态λ演算，是风格上接近面向对象的语言。演算是Fω的一个限制子集（带乘积），编码对应于系统F中代数类型的经典编码（直到某些约简和类型同构）。另一方面，因为我们的演算类似于面向对象的语言，所以有一个直接的嵌入到Featherweight Generic Java（它本身是Generic Java的一个子集）中;这让我们可以恢复318P. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）....ω我访客模式（按构成）。（ F）Alg. F型拜访O。R. . . ..，s.拉斯（O）JJGJ，，rFzGJ，，）λoo，ΔFωω我们需要一个演算来表示访问者，这样我们就可以为此，我们将“对象”近似另一个要素是一种参数化的let类型，我们将使用它来近似泛型的接口。我们定义：tα<β>beT1inT2β（Λα ：：β β）。T2）[Λβ. T1]在没有类型参数的地方，我们省略<>并定义：letαeT1inT2（Λα：：. T2）[T1]这个构造可以扩展为包括任意数量的参数在Fω的定义中加入一个元组类。我们定义了一些约定：我们写 “+” 表 示 “ 一 个 或 多 个 发 生 -“; β → 表 示 β1，.。 . ，βp;[S→]或[S1]。 . [Sp];和<$S→）对于<$S1），. . ，Sp）。我们的演算用于定义访问者类型，然后如下。定义4.1λoo的类型是Fω（带let）的良好类型，由下式给出：J在J：：=（letαβ>beOin）+α[S→]interfacedefinsO：：=i∈1.. nMi对象类型M：：=β→。（j∈1.. mSj）→Smethd类型S：：=α[S→]interfaceint at atiatia|int整型其中α，β∈TyVar，int是常量类型。请注意，此语法将所有类型变量限制为类型或类型。我们还坚持所有类型变量都是绑定的，并且所有绑定的变量都是不同的。使用定义4.1，我们可以将访问者重新表示为let类型。定义4.2如果T是一个构造函数类型为Fi[T]→T的数据类型，其访问者编码如下：T=let访客[β]令β γβ>bex`（Fi[β]→β）ini∈1.. n`visit[β]x接受δbeγ`[α]→α在δP. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）319ωj∈1..M很容易看出，这等价于通过Fω的一系列减少的系统F编码：不= 设γ<β>为（Fi[β]→β），设δ为α，γ[α]→αi∈1.. n=（Λ γ：：π π。（Λ δ.δ）[δα.γ [α] → α]）[Λ β.（Fi [β] → β）]i∈1.. n~β（Λ γ：：β）γ [α] → α）[Λ β.（Fi [β] → β）]i∈1.. n~βα。（Λ β.（Fi [β] →β））[α] → αi∈1.. n~βα。（（Fi[α]→α））→αi∈1.. n但是我们也可以在Generic Java中恢复访问者为了做到这一点，我们定义了一种翻译。定义4.3从λoo的类型到FGJ接口定义序列的转换如下：（为了使其更复杂，我们稍微使用了EBNF表示法。LHS上的重复出现与RHS上的重复出现相对应<$（letαβ>beOin）+α[S→]）=（interfaceeαβ>{<$O）}）+¢i∈1.. nMi）=（<$Mi））i∈1.. n<$β→。（j∈1.. mSj）→S）=<β→<$S）m（（<$Sj）xj））;<$α[S→]）=α<$S→）>int）=Int其中m和xj是新的。当考虑到FGJ的变换时，将有必要单独考虑Fi[β]的因子 我们将取Fi [β]为j∈1。r−1int ×k∈r.. nβ。320P. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）ω我们定义了以下缩写：Int→f= Intf1，. . . ，Intfr−1 （类似于Int→x）D→g= Dgr，. . ，Dgn （类似于β→g和S→y）Int→f;= Intf1;. . . ;Intfr−1;D→g;= Dgr;. . ;Dgn;（对于β→g;也是如此）。→f=→f;= this。f1=f1;. . . ;this.fr−1=fr−1;这个。→g=→g;=这个。gr=gr;. . . ;this. n=n;这是。→f= this。f1，. . . ，this. fr−1这是。→g.accept<α>（v）= this. gr.accept<α>（v），. . ，this. gn.acceptα>（v）将（）应用于访问者的let编码，令γ<β>为（Fi[β]→β），设δ是α，γ[α]→α，δ）i∈1.. n=界面γβ>{（βvisiti（Int→x，β→y）;）i∈1. n}界面δ{<α>α accept（γα>v）;}命题4.4从λoo到FGJ的转换是类型保持的。Proof（Sketch）证明是通过对类型结构的归纳，跟踪接口表生成的。Q我们已经证明了一系列Java接口可以被看作是系统Fω中的类型。如果接口类似于类型，那么实现接口的类应该对应于术语。这是事实：对于每个构造函数consi，都有一个类Consi。类似地，F ω中的“访问方法”元组有关这种对应关系的概述，请参见图2我们还希望确保接口和类定义都是良好类型的。命题4.5（内部访客格式良好）假设类表CT和接口表IT具有图2所示的类和接口定义，对于任何Δ，对于每个i∈ 1. n，(i) ΔUokP. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）321内部访客编码FGJ内部访客T=Yletγβ>be（Fi[β]→β），i∈ 1.. n设δ是<$α，γ[α]→α在δ中接口访客<β>{（βvisit（Int→x，β→y）;）i∈1. n我}接口D {a accept（Visitora> v）;}nsi：Fi[T]→Tconsi=λx：Fi[T].YΛα。λ v：（Fj [α] →α）。j∈ 1.. nv i（Fi[λt：T. t[α]v]x）Yclass Consi implementsD {在t→f;D→g;Consi（Int→f，D→g）{this. →f=→f;这个。→g=→g;}<α> α accept（Visitor<α>v）{returnv.visiti（this.→f，这个→g.accept<α>（v））;}}s：（Fi[U]→U）i∈ 1.. ns=fλx：Fi[U]. e ii∈1.. n类ConcVis实现访问者U>{（Uvisit（Int→x，U→y）{returnne;}）i∈1.n我我}图二. FGJ中类型编码和内部访问者之间的对应关系(ii) Δi→x：Int，→y：U，this：ConvVis∈i∈V和convV：U图2中的类和接口定义是格式良好的。校样（草图）使用FGJ的类型系统进行简单的类型检查作为一个工作的例子，我们考虑类型B的二叉树与整数在叶子上，由F[X] =Z+X×X的最小不动点给出。 这是编码为B=设γ为Λ β。（Z→β）×（（β×β）→β），设δ为α，γ[α]→α，它被转化为界面访问者β>{βint x（Int x）;intx，int y（x，y）;}接口BinTree {a accept（Visitora>v）;}数据类型构造函数是叶： Z →Bleaf（n）= Λα.λp，q：（Z→α）×（（α×α）→α）.pn节点数： （B×B）→B节点（l，r）= Λα.λ322P. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）对应的FGJ类Leaf和Node是类Leaf实现BinTree { Int n;Nil（Int n）{ this.n= n;}aaccept（Visitor v）{return v.visitLeaf（）;}}类Node实现BinTree { BinTreel;BinTreer;Cons（BinTreel， BinTreer） {this.l=l;this.r=r;}a accept（Visitora> v）{return v.visitNode（l.acceptα>（v），r.acceptα>（v））;}}二叉树的具体访问者的类型是设γ为（Z→Z）×（（Z×Z）→Z），一个求和树的叶子的操作可以定义如下：总和 ：B →Zsum=λt：T.t[Z]<$λx：Z.x，λ<$x，y<$：Z×Z.x+y<$这相当于在BinTree上调用accept，并使用以下具体访问者class SumVisitor implements VisitorInt>{ Int visitLeaf（Int x）{返回x;}Int visitNode（Int x，Int y）{returnx + y;}}生成的代码是有效的、类型良好的FGJ，带有接口代码。这意味着它也几乎是正确的泛型Java。实际上，在进行了一些小的修改（在方法定义中添加关键字public，丢弃类型参数实例化调用接受和添加一个主方法），它使用Sun Java 1.5编译器正确编译P. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）323接口访问者{int nums（int n）; intnums（int n）;}接口BinTree {void accept（v）;}int n; int n;public int findDuplicate（int []nums）{v.search（n）;}}Node类实现BinTree{ BinTreeleft; BinTree right;Node（BinTreeleft，BinTreeright） {this.left=left;这是正确的;}public void accept（v）{ left.accept（v）;right.accept（v）;}}类SumVisitor实现Visitor {int s;public int findDuplicate（intfindDuplicate）{public int findDuplicate（int n）{} public intfindDuplicate（int n）{}5从功能性到强制性的内部访问者图三. Java中的命令式内部访问器（无泛型）图2中的访问者是纯功能性的，并且依赖于泛型。图3中给出了一个更典型的使用内部状态的内部访问者的呈现（是否应该省略visitNode（）是有争议的，因为内部节点上没有信息在本节中，我们将讨论功能和命令324P. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）^^参观者，虽然在一个非常理想化的设置。考虑一个将二叉树的所有叶子相加的例子功能访问者将通过在所有内部节点上执行添加操作来实现这一点另一方面，访问者模式的一个更典型的强制性使用将使用访问者中的字段来累积总和。字段初始化为0，在每个叶子节点，它的值被添加到字段中;在内部节点，左子树和右子树被简单地一个接一个地遍历遍历后，字段保存结果。由于这种命令式访问器使用状态而不是结果值，因此其返回类型为void。我们将建模一个访问者，它通过函数S→S更新状态S，就像在命令式语言的语义学中，或者计算方法的一元视图中一样给定二叉树t（的函数内部访问者编码），我们将其定义为：^t= Λα.λc：Z →α→α. t[α→α]εc，εαε在这里，函数的组合被简化，◦α=λ<$f，g<$：（α→α）×（α→α）.λx：α.g（f x）与t相比，t更特殊：它只允许在叶子节点指定一个操作，需要转换类型为α的状态，而在内部节点的唯一操作是组合左子树和右子树的状态转换器;这种状态转换的组合对应于连续调用两个void返回方法为了将状态转换和功能访问者联系起来，我们希望表明状态转换访问者（初始状态为0）产生与函数访问者相同的^t[Z]（λn：Z.λs：Z. s+n） 0=t[Z]idZ，+我们使用关系参数性[13]，特别是Wadler开发的设t为内部访问者的二叉树，即t：α。（（Z→α）×（（α×α）→α））→αNowt[Z]（λn：Z.λs ：Z. s+n） =t[Z →Z]<$（λn ：Z.λs ：Z. s+n），则Z= 0.我们想展示哪里t[Z]idZ，+=t[Z→Z]addZ，Z0idZ =λn：Z.n：Z →Z加Z=λn：Z.λs：Z.s+n：Z→Z →ZP. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）325假设参数性[16]，对于所有关系R，<$t，t<$∈（（Z→R）×（（R×R）→R））→R我们定义了一个关系R：ZParticipate（Z→Z），f∈Ri <$f（x）=n+x，对所有x。然后我们有：如果Z是实数，则加Z<$∈Z →Rn+，nZn ∈（R×R）→R后者成立是因为如果∈R×R，则∈R。由于t将相关的参数映射到相关的结果，我们有∈R因此，根据R的定义，t[Z →Z]≠ dZ，则需要<$Z<$0=t[Z]≠ dZ+<$。注意，该证明利用了0是加法的中性元素，以及加法的结合性来建立fg之间的关系R。x+y：（f<$g）（z）=f（g（z））=f（z+y）=（z+y）+x=z+（x+y）上述通过结合性将功能访问者和命令访问者联系起来的论点也适用于更实质的情况。考虑抽象语法树的标准示例，并假设我们需要遍历树以将信息添加到符号表中就合成属性而言，最明显的规范本质上是功能性的，即在内部节点合并子树的符号表。命令式访问者可以用空的符号表来启动o表，并通过更新 在遍历期间可变的符号表。显示功能和命令版本的等价性应该类似于上面的参数性论证，空符号表是中性元素，符号表的合并是关联操作。6结论我们已经重建了内部的游客模式和外部变量的一个限制形式内的理想化类型理论的设置。要做到这一点，我们必须做一些简化的假设，而fit并不完美;这可能是不可避免的，因为Java并不是在lambda演算之上设计的，这与函数式语言不同。但是，如果人们同意这些理想化，就有可能比从冗长的Java代码或类图中更容易地收集访问者的基本特征我们总结了我们的抽象重建游客与326P. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）ω根据模式文献[6]中使用的术语映射模式文学理想化视图访客界面类型（确定函子F）具体访客Objetofvisitortype（f=F-al gebra）访问方法访问者结构图的组件数据（或弱初始访问者Accept方法证人姓名首字母具体数据由consi有大量关于访问者模式的文献，其中大部分都涉及克服它的一些不稳定性。这项工作可以追溯到雷诺兹[12]。在本文的上下文中，最相关的工作是Felleisen和FriedmanSetzer [15]还观察到访问者和函数式编程之间的如第5节所述，对于函数式（特别是内部）访问者，多态类型立即给出了一个推理原则，或应该有可能将这种参数的结构转移到更现实的命令式访问者，其中堆的部分上的逻辑关系将被用来代替函数式访问者的返回类型参数性代替访问者的结果类型，关系可以建立在一个结果系统上[10]（从函数式语言改编为面向对象语言[1]）。特别是，事件注释告诉我们，要遍历的数据结构释放了访问者的事件，但本身不会引起除了有效的系统，霍尔逻辑也适用于游客。具体来说，看看访问者的抽象谓词[11]是否可以类似于量化结果类型进行处理将是很有趣的System F中的访问者样式编码不能扩展到使用子类化的数据库在F： to中考虑类似的编码可能是值得的看看它是否更适合这种访客模式变体。确认我们感谢Alan Mycroft和匿名裁判的评论。P. 布拉夫斯基，H。Thielecke/Electronic Notes in Theoretical Computer Science 155（2006）327引用[1] 加文·比尔曼马修·帕金森和安德鲁·皮茨 MJ：一个命令 Java的核心演算和Java的结果。技术报告563，剑桥大学计算机实验室，2003年。[2] C. B？hmandC. Ber a rdu c ci. 一个更重要的是，这是一个关于大型企业的类型化计划。Theoretical Computer Science，39（2/3）：135[3] Gilad Bracha，Martin Odersky，David Stoutamire，and Philip Wadler. 让未来对过去更安全：为Java编程语言添加泛型。第13届ACM面向对象编程、系统、语言和应用会议（OOPSLA'98），温哥华，不列颠哥伦比亚省，1998年10月18-22日ACM Press，New York，1998.[4] Matthias Felleisen和Daniel P. Friedman。一点Java，一些模式。麻省理工学院出版社，马萨诸塞州剑桥，1998年。[5] Etienne M.作者声明：by Laurie J. SableCC，一个面向对象的编译器框架。面向对象语言和系统技术会议论文集，加利福尼亚州圣巴巴拉，1998年8月3IEEE计算机学会，华盛顿特区，1998年。[6] Erich Gamma，Richard Helm，Ralph Johnson，and John Vlissides. 设计模式：可重用面向对象软件的元素。1995年，马萨诸塞州波士顿，艾迪森-韦斯利[7] 我知道了。 Interr rr'etationfonctionnelleet'elimin ationdescoupuresdel' a r i t h m' et i que d 'r d re s u p' er i e u r. PhDth esis，Uiver siteParis7，1972.[8] Jean-Yves Girard，Paul Taylor，and Yves Lafont. 证明和类型。剑桥大学出版社，剑桥，1989年。[9] 五十岚敦，本杰明·皮尔斯，菲利普·瓦德勒。Featherweight Java：Java和GJ的最小核心演算。在Proceedings of the 14th ACM Conference on Object-Oriented Programming，Systems ，Languages，and Applications（OOPSLAACM Press，New York，1999.[10] John M. Lucassen和David K. 吉尔福德。多态效应系统。在Proceedings of the 15th ACMSymposium on Principles of Programming Languages（POPLACM Press，New York，1988.[11] 马修·帕金森和加文·比尔曼分离逻辑和抽象。 在Proceedings of the 31st ACM Symposium onPrinciples of Programming Languages（POPLACM Press，New York，2005.[12] John C.雷诺兹用户定义类型和过程数据结构作为数据抽象的补充方法。In S. A. Schuman，editor，New Directions in Embryonic Languages 1975，pages 157-168. 1976年，法国罗克库尔国际研究所[13] John C.雷诺兹类型、抽象和参数多态。 In R. E. A. Mason，editor，Information Processing83，pages 513-523. Elsevier Science Publishers B. V.（北荷兰），阿姆斯特丹，1983年。[14] John C. Reynolds和Gordon D.普洛特金关于多态类型lambda演算中可表达的函子。信息与计算，105：1[15] 安东·塞泽尔Java是一种函数式编程语言。In H. Geuvers和F. Wiedijk，editors，Types forProofs and Programs ： International Workshop ， TYPES 2002 ， Berg en Dal ， TheNetherlands，24施普林格，柏林，2003年。[16] 菲利普·瓦德勒免费的定理！第四届函数式编程和计算机体系结构国际会议（FPCA'89），伦敦，1989年9月11-13日ACM Press，New York，1989.328P. 布拉夫斯基，H。Thielecke/Electronic Notes