Java类型导向程序设计：基于模式匹配的新机制与泛型集成

理论计算机科学电子笔记138（2005）117-136www.elsevier.com/locate/entcs一种Java类型导向程序设计Stephanie Weirich1梁黄美国宾夕法尼亚州费城宾夕法尼亚大学{sweirich,lhuang3}@cis.upenn.edu摘要类型导向程序设计是软件设计中一种重要且广泛使用的范例。通过这种形式的编程，应用程序可以分析类型信息以确定其行为。通过分析数据的结构，许多操作，如序列化，克隆，适配器和迭代器可以定义一次，用于所有类型的数据。 这样，随着程序的发展，这些操作就不需要更新它们将自动适应新的数据表单。否则，必须为每种类型的数据单独重新定义这些操作中的每一个，迫使程序员在程序的生命周期中多次重新访问相同的程序逻辑Java语言支持使用instanceof操作符和Java ReectionAPI进行类型导向编程。这些机制允许Java程序依赖于对象的运行时类的名称和结构。然而，Java的类型导向编程机制很难使用。它们也不能很好地与泛型集成，泛型是Java语言。在本文中，我们描述了几个表现力的新机制的设计类型导向编程在Java中，并表明，这些机制是健全的，当包括在一个类似于Featherweight Java的语言基本上，这些新机制模式匹配泛型代码的类型参数的名称和结构因此，它们自然地与泛型集成，并为程序正确性提供强有力的保证。由于这些机制基于模式匹配，因此它们自然而简洁地表达了许多依赖于类型信息的操作。最后，它们为程序员的抽象提供了某种程度的保护。 而instanceof和receivection可以确定对象的运行时类型，我们的机制允许提供任何超类型进行分析，隐藏它的精确结构。关键词：类型导向编程，面向对象编程，反射，泛型，多型1本工作由NSF基金CCF-0347289 CAREER：面向对象语言中的类型导向编程支持。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.09.014118S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）1171介绍软件的设计和结构是一项艰巨的任务。好的软件工程要求代码简洁、可重用和易于修改。因此，现代静态类型编程语言包括抽象机制，如子类型和参数多态性（后者也称为泛型），以允许程序员分解复杂的软件。虽然这些抽象机制是有用的，但它们并不覆盖所有情况。它们不适用于那些最自然地由数据结构定义的操作。这些操作需要一组不同的抽象机制，称为类型导向编程。对于类型导向编程，程序分析类型信息以确定其行为。这样，如果参数改变结构，操作会自动适应。如果没有这种机制，这些操作中的每一个都必须为每种类型的数据单独定义和更新，迫使程序员多次重新访问相同的程序逻辑这种冗余增加了出错的机会，降低了可维护性。它使得改变数据表示对程序员没有吸引力，因为许多代码行必须修改。类型导向编程的一个典型用途是用于序列化。串行化将任何数据对象转换成适当的形式以供显示、网络传输、复制或永久存储.为了让程序员可以定义自己的例程版本，如序列化，Java编程语言[16]包括运行时类型标识（使用关键字instanceof）和引用API [17]。图1展示了一个简单的Java中循环数据结构的序列化类Pickle包含方法pickle，该方法通过检查对象的类型结构将其转换为字符串对于递归数据结构，此操作使用哈希表来记录先前序列化的对象对于以前没有序列化的对象，它首先确定对象布尔值）。如果是，则使用其中一个基元操作将object到string。否则，pickle递归序列化对象的每个字段。以这种方式实现序列化的好处是它独立于类结构。如果没有这种机制，每个类都必须实现自己的序列化例程。程序逻辑在类中的这种分散意味着，随着应用程序的更新，序列化方法必须在许多地方不断定义和更新即使我们不介意这种混合的关注，定义和维护-S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）117119class Pickle {//哈希表用于循环检测protected HashMap;public String pickle（Object obj）{if（obj== null）return“null”;//检查是否//如果没有，则为该对象存储一个唯一的if（hashMap.containsKey（obj））return（String）hashMap.get（obj）;String id=“#”+String.toString（hashMap.size（）+1）;hashMap.put（obj，id）;//打开对象Class Object> objClass=obj.getClass（）;if（ obj instanceofObject） {int i=（int i）;return int.toString（i）;} elseif（ obj instanceof Boolean） { Booleanb =（Boolean）obj.booleanValue（）;return Boolean.toString（b）;如果...{//其他基本类型的情况或if数组} else try {//如果obj不是原始类型或数组，则//确定所有字段并递归地pickle//每个字段，用逗号分隔字符串结果=“[”+id+“：“+objClass.getName（）+““; Field[] f= objClass.getDeclaredFields（）;for（int i=0; i f.length; i++）{ f[i]. setIncreasible（true）;result+= f[i].getName（）+“=”+ pickle（f[i].get（obj））;if（i（f.length - 1））result+=“，";<}“]”;return result+} catch（Exception e）{ return“不可能”;}}// 构造函数-创建 一个 空哈希表Pickle（）{this.hashMap = new HashMap（）;}}120S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）117Fig. 1. Java中的类型定向序列化S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）117121使用这些分布式方法是乏味的，并且容易出错，特别是如果代码维护者不是原始作者的话。类型导向编程允许程序员在一个位置定义操作此外，与其他将操作与数据分离的设计模式（如访问者模式[15]）不同，类型导向编程不会出现可扩展性问题。当现有的类发生变化时，因为类型导向的操作是由类型结构定义的，所以它们不需要更新。Palsberg和Jay已经证明，使用反射实现访问者模式可以解决可扩展性问题[30]。类型导向编程在软件系统开发中起着关键作用。 许多基本操作都是在类型信息的结构上定义的。除了序列化之外，克隆（制作相同的数据深度副本），结构相等和迭代（对集合中的每个数据元素应用操作）可以通过类型结构来定义。类型导向编程在软件组件的边界也很重要。可扩展系统可以使用类型信息来确保系统的稳定性它们可以检查新加载的代码是否满足运行系统的要求，并在接受动态更新之前提供必要的接口[20]。此外，当接口在开发过程中是已知的时，类型定向代理可以用于使组件的接口适应特定的位置。例如，如果应用程序总是用相同的第一个参数调用特定类的每个方法，类型导向编程可以为自动提供该参数的类定义一个包装器[33]。此外，这样的代理可以用于记录，跟踪，分析或调试对特定组件的所有方法的函数调用[19]。最后，面向类型的编程在软件和用户之间的边界也很有用它允许功能在添加到系统时自动返回给用户。例如，使用JavaBean [23]，系统可以检查新组件的接口，以直接提供复选框，选择列表，按钮等形式的组件的用户界面控制Java中现有机制的问题尽管Java的类型导向编程机制促进了程序的模块化（图1中的序列化例程可以应用于任何对象），但与其他语言中的类型导向编程相比，序列化也展示了instanceof例如，在Java中使用instanceof或review几乎总是需要122S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）117运行时类型转换，导致冗余检查和潜在的动态故障。在这个例子中，当obj是一个String时，它必须在转换为字符串之前转换为String类此外，如果obj不是表示基元类型的类之一，则必须安装IllegalException每次现场访问都可能引发但是，由于唯一访问的字段是由getDeclaredFields提供的字段，因此永远不会引发此异常当反射被正确使用时，运行时强制转换是多余的。但是，由于可能会错误地使用检测，因此程序员必须考虑运行时检测失败的情况，并且必须编写代码来处理ClassCastException或IllegalException等异常。 这些运行时强制转换必须包含在正确的代码中这一事实是一个征兆事实上，反射是一种相对低级的定义类型定向操作的机制此外，反射打破了Java中用户定义的抽象。getDeclaredFields方法生成一个数据结构，其中包含对象的所有字段，包括声明为protected或private的字段。因此，程序员不能依赖私有字段来隐藏信息或强制程序模块化。调用setfunctionsable（true）可以防止在访问私有和受保护字段时引发IllegalException。为了防止对私有字段的访问，整个程序可以使用安全管理器来运行，该安全管理器会导致setupsible命令失败。然而，这种粗略控制达不到所提供的可编程访问控制在其他领域。1.1Java的新机制在本文中，我们提出了新的机制，在Java中的类型导向的编程，可以用来代替instanceof或recruitment。这些新机制基于Java的第一类泛型扩展--其中，将参数实例化为泛型方法的类型并且类在运行时可用。Java中泛型的当前实现（基于GJ [5]）在程序运行之前擦除这些类型，而NextGen [ 8，3 ]等扩展则在运行时有效地提供了这种类型信息。一级泛型已经为Java编程语言提供了许多好处[2]。我们的新机制直接分析第一类类型信息，而不是检查对象的运行时类这种方法有几• 我们的新机制可以提供更强的正确性保证只是S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）117123由于泛型的引入允许从Java程序中消除一些强制转换，因此这种机制也可以消除潜在的故障点。• 我们的新机制更容易使用。我们提出的机制提供了复杂的类型匹配功能，为用户提供了一种方便的方式来编程的类型信息。特别是，这些机制可以更自然地编码类型导向算法的结构。• 我们的新机制与泛型很好地结合在一起。由于泛型的类型擦除实现，当前的JavaRecrection和instanceof实现没有提供关于泛型的准确信息类和方法。虽然可以扩展instanceof和Java引用[32]泛型，我们认为我们的机制是一个更自然的集成。• 我们的新机制在保护抽象方面是有表现力的反射和实例分析对象的最具体类型。然而，描述对象类型的运行时类型信息不需要完整的要通过分析确定的对象的结构可以向类型导向操作提供对象类型的缩写版本在下一节中，我们将非正式地描述分析类型参数的名称和结构的机制，并展示它们的表达能力。在第3节中，我们在类似于Featherweight Generic Java[21]的核心演算中形式化了它们的语义本文的主要结果是，我们表明，这些新的机制是类型安全的。最后，我们讨论了相关的工作和未来可能的扩展。2分析类型参数我们可以粗略地将类型导向机制分为两类：一类是确定运行时类型的名称（类似于instanceof），另一类是确定其结构（类似于响应机制）。这两种机制都是必要的：回想一下序列化的实现。在下面的小节中，我们首先描述可以用来代替instanceof的运算符，然后在下一小节中讨论reference的替换。2.1标称分析考虑一种新的Java表达式形式，名为ifsubtypeof。 这个表达式形式是条件的-它根据类型变量T在运行时是否是特定类型的子类型来选择两个分支之一。如果条件124S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）117保持，类型检查器可以执行类型细化-提到T的变量的类型可以在分支中改变，消除冗余的类型转换[12]。例如，如果x的类型为T，那么在下面的例子中，我们知道T是xD的子类型，并且x在使用之前不需要转换为xDTx;public int findDuplicate（T）{//在这个分支中T = x，所以x的类型为x}此外，类型变量在类型之间创建等式确定单个类型变量的运行时标识可以细化许多对象的类列表T> x;public int findDuplicate（T）{//在这里我们知道T是一个子类型，//所以列表x中的所有元素都是整数。}通过分析类型参数，我们从程序.否则，当检查对instanceof对象的引用的运行时类时，由于别名，它们的类型可能会意外更改。一个包含类型修饰的instanceof版本将是不我们不能静态地消除下面这样的类型转换，因为我们不能保证x.field的运行时类型保持不变。if（x.field instanceof x.field）{ writeInt（（x.field）;}如果x.field的类型是Object，任何线程都可以在任何时候用任何类型的对象更新x.field。然而，如果x.field的类型是类型参数T，如果我们确定T是一个子类型，那么x.field必须包含一个对象，其类型是一个子类型。不需要强制转换，因为其他线程可能只会给x.field赋值。if（T，t）{ writeInt（x.field）;}然而，ifsubtypeof，像instanceof一样，在参数化类方面受到限制。它不能确定类型T是否是任何类型的列表。相反，它必须将T与List U>进行比较，其中U是一个特定类型。由于<类型参数的不变性，使用List Object>是不够的：List< Object>不是List Object>的子类型<。将名词性分析与模式匹配相结合，可以使名词性分析更有表现力。下面的表达式typematch推广了ifsubtypeof。该表达式将参数类型与许多类型模式（可能包含模式变量的类型）进行匹配。S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）117125getClassName T>类的名称作为字符串。getFieldName T，f>类T中字段f的名称，以字符串形式表示。getMethodName T，m> 类T中方法m的名称，以字符串形式表示。numFields T>字段数为整数。numMethods T>方法的数量，以整数表示。图二. 类型结构的简单操作Tx;类型匹配T，这里x是一个整数。List< U>：//这里x是U的列表。default：//这里我们对x一无所知。与if子类型一样，类型检查器可以细化静态类型信息，使其与表达式的分支相 如果模式不包含任何自由类型变量，则typematch的行为与ifsubtypeof相同。2.2结构分析表达式ifsubtypeof和typematch对应于（并泛化）instanceof等操作，当我们知道类一个对象可以是一组有限的类中的一个。然而，很多时候程序员并不知道一个对象的类，但仍然想确定该类的结构在Java中，引用API提供了这种功能。在这一小节中，我们提出了基于分析运行时类型信息结构的反射替代方案。对于类型参数，反射的某些功能很容易定义例如，图2列出了几个操作，这些操作决定了类的名称或方法或字段的数量。然而，更难的是定义确定关于场和方法的精确信息并提供安全访问它们的操作。我们的方法是添加新的表达式形式来迭代类的字段和方法。forfield表达式迭代类中的字段T，将类型参数X绑定到每个字段的类型和访问器变量f为每个字段的名称。访问器变量可用于从类型T的对象投影当前字段。我们可以如下使用forfield：126S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）117public T>String pickle（T obj）{if（obj ==null） return“null”;//检查我们是否看到了obj。如果没有，为它存储一个唯一的id。if（hashMap.containsKey（obj））return（String）hashMap.get（obj）;String id=“#”+String.toString（hashMap.size（）+1）;hashMap.put（obj，id）;//打开对象类型匹配T，String：return String.toString（obj）;Boolean：return Boolean.toString（obj）;... ：//其他基本类型X[]： //数组默认值：{String result=“[”+id+“：“+ getName T> +““; Int i=0;public int findDuplicate（intx）{i ++= getFieldName T，f> + pickle X>（obj.f）;if（i<， i）}“]”;return result+}}图三. 酸洗与结构类型分析Tobj;//遍历T的所有字段public int findDuplicate（intx）{//绑定类型参数X和访问器变量f。然后//优化T，使其包含一个X类型的字段“f”XfieldVal =obj.f;print X>（fieldVal）;//可以像其他类型}使用forfield，我们可以重写pickle方法，如图3所示。 在这个例子中，我们使用类型匹配来确定T是基类型还是数组类型。如果两者都不是，那么forfield将遍历对象中的字段，递归地调用序列化例程。如果使用其参数的运行时类型调用pickle操作，则结果将是S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）117127与之前的pickle版本相同。然而，这个版本的pickle不仅更短，没有类型转换，而且在类型抽象方面更灵活。pickle的调用者可以通过提供不同的类型参数来自由决定应该生成对象的什么为例如，如果存在调用方不希望打印的运行时类型的组件，则调用方可以提供不包括该组件的超类型，如下面的示例所示class NotSecret {intanynumber = 54321;}{ int mysecretnumber= 12345; } Secrety = new Secret（）;System.out.println（Pickle.pickle Secret>（y））;System.out.println（Pickle.pickle NotSecret>（y））;pickle的两个调用都是有效的，但只有第二个调用打印了y的两个字段。forfield表达式形式的语义并不像它看起来那么简单。在forfield的主体中，类型T的恒等式应该被定义为一个类型，该类型包括一个称为f的X类型的场。然而，包含单个字段f的类型可能不存在。因为Java定义的类，很可能不会有一个具有正确结构的类，我们可以将T细化到。因此，如下一节所述，我们将向Java添加一种非常有限的结构化对象类型。考虑到我们正在验证对象类型的结构分析，这种添加并不奇怪但是，与其他结构类型系统不同，对程序员来说是令人困惑的，这个扩展是相当良性的。本质上，唯一的为了反映类型导向程序中常见的习惯用法，我们将类型模式匹配与forfield相结合。每个字段的类型由类型模式表示。在上面的例子中，这个模式总是一个单一的变量。然而，可以使用任何图案例如，模式可以是文字类型，在这种情况下，主体会为每个具有该类型的字段T obj =.;public int findDuplicate（）{//递增obj中所有整数值字段obj.f= obj.f+ 1}其他类型模式可以选择类中所有的数组字段（无论它们包含什么类型的元素）或类中的所有静态字段与forfield类似，formethod表达式迭代类中的方法。类型模式对于这个迭代非常重要。为128S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）117类型S，T，U：：=X| N非变量类型N、P、Q：：=C T>类声明CL：：=类C Xa N>a N{ Tf=v;M}方法声明M：：= T m（T x）{ return e;}方法类型Mt：：=（T）→T表达式e：：=X|e.F|e.m T>（e）||||新T（e）| (T)etypematch S withT： e default：eJfieldfoldi（x=e;S fx∈T） eJ方法i（x= e;MT mx∈T） eJ值v：：=新C（v）类型上下文Δ：：=∅ |Δ，X<：S| Δ, S <<: T|Δ，S：{ T fx}| Δ,T<<:{MTmx}术语上下文Γ：：=∅ |r，x：S类型替换Σ：：=∅ |X→ T见图4。 TDJ系列例如，假设我们想要挑选出一个类中所有不带参数、返回void且名称以“test”开头的方法。我们可以用以下代码来实现：public static.startsWith（“test”））{x.m（）;}}}迭代域和迭代方法之间的区别在于，由于方法类型参数和多参数方法，不可能编写足够通用的模式来匹配类中的每个方法。模式必须指定方法的类S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）117129型参数和项参数的数量。更复杂的模式语言可能会产生更多的表达能力。例如，我们可以添加一个然而，这将是有限的使用，因为我们不能调用方法，而不能确定它需要的类型和术语参数的数量。3语义为了更全面地描述我们新的类型分析操作符的语义，并保证它们在Java的上下文中是可靠的，130S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）117编程语言，我们接下来形式化一个小型的Java类语言扩展这些结构。像轻量级泛型Java（FGJ）[21]，我们的新语言，称为TDJ类型导向的Java，是一个面向对象的语言与名义子类型的功能核心。除了类型分析操作符，这种语言只包括顶级类定义，对象实例化，字段访问，方法调用和类型转换。我们省略了许多与我们的研究正交的Java特性，例如突变、并发、异常和接口。像NextGen [8]一样，TDJ有一个类型传递语义。我们在泛型Java不允许的地方例如，类型参数可以用于运行时类型转换和对象实例化。为了支持这个模型中的抽象对象创建，所有类都必须声明实例ini-适用于所有领域。在一个新的X（e）表达式中，因为类是抽象的，类型检查器不知道必须提供多少参数给建筑师。然而，如果新表达式没有提供足够的值，那么初始化器的值可以用于缺失的字段。为了简化语言的语义，我们要求初始化器是类声明中的语法值。TDJ的抽象语法如图4所示。我们使用元变量C和D来引用类名，x和y来引用表达式变量，X，Y和Z来引用类型变量。和FGJ一样，我们也严重滥用了序列，例如，使用Tf来指代T0f1，. ，T0fn. 符号|不|是序列的长度。名称序列（例如对于类型、变量、字段和方法）必须不包含重复项。此外，这不应该是字段或变量的名称。这个演算的核心的语义与FGJ非常相似。由于篇幅原因，打字的规则和辅助功能出现在配套的技术报告中[36]。为了使我们的模型更接近Java，我们给它一个小的步骤调用值的语义，而不是一般的约简规则。这种演算和FGJ的类型系统有一些显著的区别。许多规则要求找到类型的最小不变上限在FGJ中，变量可能不受其他变量的约束，但在TDJ中，我们不保留此不变量。因此，我们定义T的上界在Δ中，递归地写出界限Δ（T）。与FGJ不同的其他打字规则包括T-C类，在那里我们检查场的初始化器是否正确formed和T-NEW，其中，由于场初始化器的存在，可以向新表达式提供比场更少的参数。S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）117131计算：matches（N，X）=X›→N匹配（C S>，C T>）=等于（C S>，C T>）CT（C）= classC< XaN>aN{. 个文件夹T不是C T>matches（C S>，T）=matches（[X<$→S]N，T）equals（N，X）=X›→Nequals（S，T）=一致equals（C S>，C T>）=matches（N，T）= 0typematchNwithT：eT：e default：e›→（e）J[R-M[ATCH]matches（N，T）没有定义typematchNwithT：eT：e default：eJ [R-NO匹配]›→typematchNwithT：e default：eJ类型匹配N，默认值：e›→ e静态语义：JJ[R-D故障]ΔT okdom（Δ）=FV（T）米诺克<$X∈dom（Δ），Δ（X）=Object[M-MINOK]S：T∈Δ界限Δ（S）=N界限Δ（T）=N[B-REFINE]S：T∈Δ[S-REFINE]ΔΔS：TΔTokΔU okΔ;Γe∈U：UJ J（1 ≤i≤|不|） ΔiTiminokΔ， Δ，T：T;我我我我JΔ;ΓtypematchTwith T：e default：e∈U[T-R埃菲内]3.1名义分析表达式形式typematch T with T：edefault：e允许程序员模式匹配运行时类型信息的名称。这个表达式的语义如图5所示。这种表达式形式的动态语义依赖于产生替换函数matches（T，U）（如果如果存在，则T=T（U）。 （（·）notatesasi multaneoussub s.）在类型匹配的第一个计算规则，模式匹配的参数必须是封闭类型N。如果该类型匹配第一个模式，则将替换分支中的模式变量。如果第一个模式不匹配--如果我们不能导出匹配判断--那么语义将丢弃第一个模式并检查剩余的模式。因为每个匹配表达式都必须以默认分支结束，所以将采用某些分支。对于一个简单的、确定性的语义，图五. 名义型模式匹配132S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）117模式匹配分析的类型，选择第一个匹配。然而，对于类型匹配的操作来说，选择最精确的模式是可能的。匹配的定义在图5的顶部。由于参数化类的参数的不变性，我们必须确定的不仅仅是类型何时可以是模式的子类型（在一些替换之后）而且当它可以等于模式时（在一些替换之后）。因此，我们定义匹配（S，T）和等于（S，T）。第一条规则指出，我们总是可以将类型与模式变量相匹配。对于equals（S，T）也有类似的规则。要将不可变类型与模式匹配，我们必须将其与同一个类匹配，其中所有类型参数都是相等的，或者我们必须看到如果它的超类匹配模式。同样，要确定一个不可变类型是否等于一个模式，该模式必须是同一个类的，并且所有类型参数都必须相等。在模式匹配表达式中，每个分支都是在一个定义的上下文中检查的，该上下文中假设分析的类型是模式的子类型此上下文消除了类型强制转换的需要我们通过添加一个特殊的假设S：T。请注意，这个假设是在任意类型之间，而不是变量绑定。事实上，S和T的自由变量也应该(In规则T-REFINE判断ΔTminok确定一个上下文，该上下文恰好包括T的自由变量，最高界限为了保证语言的可靠性，我们在检查每个分支时不要引入任何额外的假设。通过上下文修正，我们可以得出结论：ΔS：T（参见S-REFINE规则）。这样的假设也决定了类型变量的边界。请注意，在某些情况下，某些变量可能有多个边界。我们可在上下文中加入的细化假设并无限制。如果他们不满意（例如，假设C：D时，C和D类之间没有关系），则类型匹配的分支这一假设永远不会成立省略对这些分支的检查是合理的。此外，为了简单起见，我们没有从类型匹配假设中得出任何“深入”的例如，从C X>：C Y>也可以得出类型X等于Y的结论。将这种扣除与平等假设结合起来是直截了当的，但要保持语言简单，我们还没有这样做，为这个微积分。3.2结构分析TDJ中的结构类型分析确定了类中存在哪些字段和方法，其表达形式为fieldfold和methfold。是--S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）117133计算：Je ›→efieldfoldi（x=e;T fx∈N）e0›→fieldfoldi（x=e;T fx∈N）e0J[E-FFCONG]flds（N）=Tf1≤i≤|F|fieldfoldi（x=v;T fx∈N）e <$→matches（Ti，T）=[E-FFM匹配]fieldfoldi+1（x= [x<$→v，fx <$→fi] n（e）;Tfx∈N）eflds（N）=Tf1≤i≤|F|fieldfoldi（x=v;T fx∈N）e <$→matches（Ti，T）没有定义fieldfoldi+1（x=v;T fx∈N）e[E-FFSKIP]fi=Tfi>|F|fieldfoldi（x=v;T fx∈N）e <$→v [E-FFBASE]静态语义：T：{Ufx} ∈Δ[RF-HYP]ΔU：{Tfx}ΔT：{Ufx}ΔS：{T fx}ΔS：U[RF-T范围]JJJΔΔT ok米诺克Ji> 0Δ; <：UΔ， Δ，T：{T f}; Γ，x：U∈U：UJJ J JXΔ; Γ-场折i（x=e;T fx∈T）e∈UJ J[T-F[IELDFOLD]Δ; Γε∈T0Δ; Γ εe. fx∈TΔΔT0：{T fx}[T-FIELDVAR]见图6。 野外折叠由于TDJ的功能性质，这些形式被设计为带有突变的语言可以将这些形式简化为迭代，如第2节中描述的forfield和formethod。表达式fieldfoldi（x=e;Sfx∈T）eJ的语义出现在图6. 这个表达式在T类型的域上迭代。变量x是一个累加器，初始化为e。表达式eJ对每个类型与模式S匹配的字段执行一次。变量fx是一个访问器变量，它替换为字段的当前名称。指数i是当前场的指数。在源程序中，它应该始终为1。fieldfold的操作语义由四条规则定义。 第一、 同余规则允许累加器被评估为一个值。在第二个规则中，索引引用类中的一个字段，并且该字段的类型与模式中的类型匹配。在这种情况下，fieldfold的主体成为新的累加器，在将当前累加器替换为x、将当前字段名替换为访问器变量以及由模式匹配生成的类型当当前字段的类型与模式不匹配时，使用下一个规则，跳过该字段。在最后一条规则中，索引为134S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）117超出范围，因此返回累加器fieldfold表达式的主体在定义的上下文中进行类型检查。一个精化假设S：{T fx}意味着任何类型S的表达式都可以投射一个类型T的场fx。这个假设在规则T-FIELDVAR中使用，当访问器是变量时，检查字段访问检查常量访问器的字段访问的规则没有改变。方法折叠的行为类似于字段折叠，所以我们省略了它的语义。（详见技术报告[36]）像fieldfold一样，操作语义遍历对象的方法，为每个匹配的方法类型执行fold的主体为了确定方法类型匹配，比如方法重写，我们需要方法的边界和参数的相等模式，但是我们允许返回类型是子类型。我们已经证明了这种语言是类型的声音，使用类似的证明FGJ [21]。这一证明的全部细节在其他地方出现[36]。4相关工作类型导向编程的最早例子是基于名义分析。许多语言，如Simula-67 [4]，CLU [28]，Cedar/Mesa [26]，Modula-2+和Modula-3 [7]，都有隐藏类型名称的机制。编译时（通过动态类型，称为any、REFANY或Object），并在运行时恢复类型名称（如INSPECT、instanceof或TYPECASE）。在某种程度上，对象语言中的动态分派是一种例外，名义分析的例子。Haskell类型类[34]通过使用类型参数在非OO语言中提供动态分派。结构类型分析对于具有复合类型的语言很重要Java（像许多其他语言，如Amber [6]，Cedar/Mesa [26]和C#）提供了一种将类型反射到数据结构中的机制。然而，即使程序员可以根据类型定义操作，这种机制也不能将操作类型与存储在数据结构中的反射类型因此，静态类型检查受到损害。类型定向操作依赖于运行时强制转换来保证其类型正确性。Crary等人[12]表明，通过使用依赖类型的形式，可以将类型信息反映到数据结构中，但允许静态类型检查本文所采用的方法非常类似于函数式编程语言中允许运行类型信息模式匹配的系统。例如，为了支持静态类型ML语言中的动态类型[29]，Abadi等人的Dynamictype[27][28][29][29]封装运行时类型信息，并提供特殊的消除form（称为typecase）来发现类型信息。S. 魏里希湖Huang/Electronic Notes in Theoretical Computer Science 138（2005）117135但是，对于Dynamic类型，只能分析存储在动态值中的类型信息。相反，内涵多态性[18]，外延多态性[13]和结构多态性[31]分析外显类型参数。这些框架要求语言语义-控制块在运行时传播类型信息，与值无关。The G’Caml [一个相关的研究方向，称为多型编程或泛型编程，模式匹配编译时类型信息以生成类型索引操作。这些机制定义了由参数化类型（也称为类型构造函数）定义的操作，如映射Charity [11]语言在编译时自动为数据库生成映射和折叠Functional ML [25]使用组合子来定义参数化类型，然后基于这些组合子定义类型导向操作。这个理论背后的思想被纳入了FiSH语言[24]。多型编程[22]扩展了Haskell，定义了类型导向的操作。泛型Haskell扩展了Haskell语言中的多型性，因此它可以处理相互递归，嵌套或多参数的数据库，以及包含函数的数据库[10]。这个框架与模式化匹配类型信息不同，类型导向操作是对微积分术语的解释。然而，Weirich [35]表明它可以与运行时类型分析相协调模式匹配运行时或编译时类型信息的系统与我们在这里提出的