Mapping Polymorphism

摘要

We examine schema mappings from a type-theoretic perspective and aim to facilitate and formalize the reuse of mappings. Starting with the mapping language of Clio, we present a type-checking algorithm such that typable mappings are necessarily satisfiable. We add type variables to the schema language and present a theory of polymorphism, including a sound and complete type inference algorithm and a semantic notion of a principal type of a mapping. Principal types, which intuitively correspond to the minimum amount of schema structure required by the mappings, have an important application for mapping reuse. Concretely, we show that mappings can be reused, with the same semantics, on any schemas as long as these schemas are expansions (i.e., subtypes) of the principal types.