论文部分内容阅读
XML是一种半结构化数据交换的标准格式，它已被广泛应用到Web服务、数据库以及形式化研究等等。为了更好的XML处理编程，近年来，在XML处理上出现了不少静态类型化函数式语言，比如XDuce、XQuery、CDuce、XJ、XTatic、XACT、XHaskell以及OCamlDuce等等，但大多数语言都缺少参数多态化或者对多态化仅提供有限的支持。然而，XML处理需要多态化功能，并且目前不少标准工作组，如RELAX NG和XQuery，已将多态化纳入讨论范畴。本文就如何为XML处理语言扩展参数多态化功能的问题进行研究。本文的解决方案分为两个部分:多态语义子类型关系的定义和多态演算的定义。
第一部分为具有递归类型、积类型、箭头类型和集合类型联结词（即交、并和否定类型）的类型系统定义和研究一个多态语义子类型关系。本文给类型变量分配类型解释域的子集，而不是将它们替换成基类型。这个语义赋值允许类型变量能够取值域的任意子集。因而，子类型关系可定义为在类型变量的所有可能赋值下所对应的集合的包含关系。为了确保子类型关系具有一致性的行为，本文提出了凸性的属性。利用集合论和凸性，本文还提出了子类型检测算法并证明它的可靠性、完备性和可终止性。简而言之，本文的子类型关系定义是基于语义的、直觉的和可判定的。
第二部分设计和研究一个显式高阶多态演算，并且该演算能够充分利用第一部分的子类型关系。多态演算的新颖之处在于给λ-抽象装饰上类型替换集合，并在规约的时候惰性地传递这些类型替换信息。本文演算也是一个具有交类型的显式类型化的λ-演算。在实际应用中，这些类型替换集合对程序员来说是透明的。为此，本文定义了显式演算对应的隐式演算并设计了一个替换推导系统。该推导系统能够推导出，在隐式表达式中哪里需要插入哪些类型替换，从而能够构造成良类型的显式表达式。本文还证明推导系统是可靠和完备的。最后，为了给多态演算提供一个运行模型，本文研究了从多态演算到单态演算（比如CDuce的变体）的编译。