Parametric polymorphism for XML
Parametric polymorphism for XML
复制标题
DOI：
10.1145/1040305.1040310
复制
发表时间：
2005-01
期刊：
影响因子：
--
通讯作者：
H. Hosoya;Alain Frisch;Giuseppe Castagna
中科院分区：
文献类型：
--
作者：
H. Hosoya;Alain Frisch;Giuseppe Castagna
尽管最近对XML的静态类型进行了广泛的研究，但参数多态很少被处理。这种良好的类型化规程在XML处理中也很有用，特别是对于涉及“参数模式”的程序，即在其他模式(例如，SOAP)上参数化的模式。处理XML多态的困难在于如何扩展主流(单态)XML类型系统中使用的“语义”方法。一个简单的扩展是对类型变量的所有替换进行“语义”量化。然而，这种方法归结为一个NEXPTIME完全问题，对于这个问题，还没有一个实用的算法。在本文中，我们提出了一种不同的方法，它平滑地扩展了语义方法，但在算法上更容易。在这种情况下，我们设计了一种新颖而简单的标记技术，其中我们将多态类型解释为一组带有注释的值，这些值的子部分被参数化。我们在多态类型系统的每个组成部分中都使用了这种解释，如子类型、类型参数的推断等。因此，我们实现了一个合理的系统，它直接表示多态类型系统的常见预期行为-“变量类型的值永远不会重新构造”-这让人想起雷诺德的参数理论。对于单纯系统，我们通过对已有的算法进行局部修改，得到了一套实用的类型检测算法。
Despite the extensiveness of recent investigations on static typing for XML, parametric polymorphism has rarely been treated. This well-established typing discipline can also be useful in XML processing in particular for programs involving "parametric schemas," i.e., schemas parameterized over other schemas (e.g., SOAP). The difficulty in treating polymorphism for XML lies in how to extend the "semantic" approach used in the mainstream (monomorphic) XML type systems. A naive extension would be "semantic" quantification over all substitutions for type variables. However, this approach reduces to an NEXPTIME-complete problem for which no practical algorithm is known. In this paper, we propose a different method that smoothly extends the semantic approach yet is algorithmically easier. In this, we devise a novel and simple marking technique, where we interpret a polymorphic type as a set of values with annotations of which subparts are parameterized. We exploit this interpretation in every ingredient of our polymorphic type system such as subtyping, inference of type arguments, and so on. As a result, we achieve a sensible system that directly represents a usual expected behavior of polymorphic type systems---"values of variable types are never reconstructed"---in a reminiscence of Reynold's parametricity theory. Also, we obtain a set of practical algorithms for typechecking by local modifications to existing ones for a monomorphic system.