14652 2011-11-01 11:10:26 +0000 [XPath 3.0] Definition of 'subtype' is incorrect/inconsistent 2013-06-19 08:42:14 +0000 1 1 1 Unclassified XPath / XQuery / XSLT XPath 3.0 Working drafts PC All CLOSED FIXED P2 normal --- 1 mike jonathan.robie public-qt-comments oldest_to_newest 59385 0 mike 2011-11-01 11:10:26 +0000 Is the union type Union(P, Q) a subtype of Union(P, Q, R)? According to the XSD rules, no. According to the detailed list of rules in 2.5.6.2, no. But according to the definition of 'subtype', yes. The definition of 'subtype' is: A sequence type A is a subtype of a sequence type B if and only if, for every value V, if V matches A according to the rules of SequenceType matching, then V also matches B. Since every value that matches Union(P, Q) matches either P or Q and therefore matches Union(P, Q, R), this definition would imply that Union(P, Q) is a subtype of Union(P, Q, R). Note also that the union type V = Union(P, Q) is unambiguously a subtype of Union(V, R). But if two union types V and W are both defined as Union(P, Q), then V is a subtype of Union(V, R) but W is not, although the definition of 'subtype' would suggest that it is. 60049 1 jonathan.robie 2011-11-15 15:25:34 +0000 Perhaps we should change the definition to this: [Definition: A sequence type A is a subtype of a sequence type B if subtype(A, B) is true.] That is the effective definition in the document, and it's hard to come up with a succinct intensional definition. 60050 2 mike 2011-11-15 16:34:08 +0000 >[Definition: A sequence type A is a subtype of a sequence type B if subtype(A, B) is true.] Seems OK to me. One could add the rider: When subtype(A, B) is true, it is always the case that for any value V, (V instance of A) implies (V instance of B). Note: the converse is not necessarily true: for example every instance of union(P, Q) is also an instance of union(P, Q, R), but there is no subtype relationship between these two types. 60052 3 jonathan.robie 2011-11-15 17:10:45 +0000 We agreed to resolve this using the following definition: [Definition: A sequence type A is a subtype of a sequence type B if the judgement subtype(A, B) is true.]