This is an archived snapshot of W3C's public bugzilla bug tracker, decommissioned in April 2019. Please see the home page for more details.
2.4.1 XML Schema and the [XPath/Xquery] type system Many possible formal type notations do not appear to have any defined semantics. For example, I have been trying to determine the semantics of "document{empty}", which presumably would describe a document node with no children, so that "dynEnv |- document {} : document { empty }" should be inferable, but I have not found any rules to make such an inference. Similarly, the semantics of document { element p:o? }, document { element p:o+ } and document {element p:o *} seem to be undefined. I saw the statement in section 2.4.2 "Item types" that "The semantics of sequence types is described in [3.5.4 Sequence Type Matching]". However, 3.5.4 does not provide any semantics for document{empty}. Re-examining the quoted sentence, I see that it only says that the semantics of sequence types is specified in section 3.5.4. Presumably "sequence type" is the same as "SequenceType". (As a lesser issue, this should also be clarified; the specification should not assume that similarly spelled terms mean the same thing.) Back to the main issue, the formal type notations are deliberately designed to be a superset of the sequence types, so it seems to be a deficiency, that the semantics of the formal type notations is only specified when a formal type notation is one that would have been derived by normalizing a sequence type. (The difference between this comment and #1615 is that #1615 questions whether you really mean to support document { Type }, whereas this comment questions whether formal types that are not sequence types have any specified semantics.)
The comment is touching on a pretty important aspect of what the formal semantics is doing. There is in fact several ways to define what you would more formally call a 'meaning' for the type. One way is to extend the notion of 'a value matching a type' to work on all types, not only sequence types. That used to be part of the spec (and of a separate paper by Phil Wadler and my self at POPL), but was removed since it is not actually used anywhere to define XQuery. Another way to define the semantics of types is to define a 'validation' judgment which tells which values can be validated against which types (and yield a new value). There is still some (incomplete) specification of this in Appendix E. But again, this is non-normative since the validation semantics is fully specified in XML Schema. What remains are two main judgments in the formal semantics: dynEnv |- Value matches SequenceType and statEnv |- Expr : Type The last judgment is the one that is important for the purpose of this specification. However, if you wanted to prove something like a soundness theorem for the type system, you would have to go through the whole exercise of defining matching, etc. The main issue here is that we are defining a standard, not trying to formally prove properties of the system. So the work is restricted to defining only what is necessary for static typing. I do not believe this is something that the group will be willing to change at this point, but I hope it makes some sense. Now more concretely about your question related to document types. There is in fact a judgement which infers the type for a document node. This is located in Section 4.7.3.3 Document Node Constructors. The static inference rule looks as follows: statEnv |- Expr : Type statEnv |- Type <: (element | text | processing-instruction | comment)* ------------------------------------------------------------------------ statEnv |- document { Expr } : document It gives precisely the constraints related to what type is acceptable inside a document node type. In the case of document { () } you will get the static type of document { empty }. Do you have specific changes in the document that you would think help? - Jerome & Michael
The WGs have decided to accept the following fix to the inference rule of document constructors as follows. statEnv |- Expr : Type statEnv |- Type <: (element | text | processing-instruction | comment)* ----------------------------------------------------------------------- statEnv |- document { Expr } : document to statEnv |- Expr : Type statEnv |- Type <: (element | text | processing-instruction | comment)* ----------------------------------------------------------------------- statEnv |- document { Expr } : document { Type } Which fixes the bug that the type of the expression was not reflected in the output type. We believe that along with the previous rationale posted for the semantics of types, this closes your comment. - Jerome Simeon On behalf of the XML Query and XSL WGs