XML transformation languages, such as XQuery, take an XML document as input and produce another XML document as output. It is useful to know statically that such transformations always produce valid documents, for static debugging of the transformation program or for eliminating dynamic checks on the output documents. This gives rise to the XML type checking problem. Type- and automata-theoretic techniques have been proposed to address this type checking problem, exploiting XML's tree structure. However, existing approaches are not capable of reasoning about dimensional information of produced XML documents, such as that two locations in the output documents always have the same number of elements.
This paper presents a type-based analysis for XQuery to discover dimensional relationships in output documents from XQuery programs through refined type checking. For example, it can identify program fragments producing the same number of elements for all input documents. The novel aspects of our analysis are techniques to deal with the rich tree structure of XML types, whereas array analyses (e.g., bounds checking) for languages such as C deal with flat arrays. In this paper, we present our type system and give a sketch of its soundness.