Union Types for Semistructured Data
Union Types for Semistructured Data
复制标题
半结构化数据的联合类型
DOI：
10.1007/3-540-44543-9_12
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
B. Pierce
中科院分区：
文献类型：
--
作者：
P. Buneman;B. Pierce
半结构化数据库被视为动态类型：它们没有配备独立的模式或类型系统来约束数据。为半结构化数据设计的查询语言，即使与结构化数据一起使用，通常也会忽略可能存在的任何类型信息。这样做的后果是人们对使用具有复杂数据的动态类型系统所期望的：对应用程序正确性的保证较少。例如，在静态类型化查询语言中会导致类型错误的查询在应用于相同数据的半结构化表示时将返回空集。许多半结构化数据起源于结构化数据。当想要添加不符合原始类型的数据或想要联合收割机组合不同类型的数据源时，半结构化表示非常有用。然而，与指定类型的偏差通常是很小的，我们相信比丢弃所有类型信息更好的策略是尽可能多地保留它。我们描述了一个系统的untaggedunion typesthat可以容纳结构的变化，同时仍然允许一定程度的静态类型检查。这个系统的一个新奇在于它涉及类型之间的非平凡等价，这是由记录和联合的分布性定律引起的：一个值可以用一个类型引入（例如，包含联合的记录）并用于另一种类型（记录的联合）。我们描述了处理这些类型的编程和查询语言构造，证明了类型系统的可靠性，并开发了子类型和类型检查的算法。
Semistructured databases are treated as dynamically typed: they come equipped with no independent schema or type system to constrain the data. Query languages that are designed for semistructured data, even when used with structured data, typically ignore any type information that may be present. The consequences of this are what one would expect from using a dynamic type system with complex data: fewer guarantees on the correctness of applications. For example, a query that would cause a type error in a statically typed query language will return the empty set when applied to a semistructured representation of the same data. Much semistructured data originates in structured data. A semistructured representation is useful when one wants to add data that does not conform to the original type or when one wants to combine sources of different types. However, the deviations from the prescribed types are often minor, and we believe that a better strategy than throwing away all type information is to preserve as much of it as possible. We describe a system of untaggedunion typesthat can accommodate variations in structure while still allowing a degree of static type checking. A novelty of this system is that it involves non-trivial equivalences among types, arising from a law of distributivity for records and unions: a value may be introduced with one type (e.g., a record containing a union) and used at another type (a union of records). We describe programming and query language constructs for dealing with such types, prove the soundness of the type system, and develop algorithms for subtyping and typechecking.