1655 2005-07-16 00:41:34 +0000 [FS] need examples of when to raise a type error 2005-07-26 15:34:52 +0000 1 1 1 Unclassified XPath / XQuery / XSLT Formal Semantics 1.0 Last Call drafts PC Windows 2000 CLOSED FIXED P2 normal --- 1 fred.zemke simeon public-qt-comments oldest_to_newest 4739 0 fred.zemke 2005-07-16 00:41:35 +0000 4. Expressions Under "Static type analysis", the discussion of when to raise a type error is difficult to understand. It would help to work through the example in more detail. Consider x/title, where $x is statically known to have no children. I have not been able to figure out how the rules in the rest of Formal Semantics would actually analyze this, but there seem to be two possibilities: 1. There are rules that infer statEnv |- $x/title : empty. But in that case, there are static type rules that apply to the expression $x/title, by hypothesis. The principle that "the absence of an applicable static rule indicates an error" does not seem to apply. Instead, it looks like you want the following inference: statEnv |- Expr : empty not (Expr is empty sequence expression () or ... ) -------------------------------------------------- statEnv |- Expr raises typeError 2. The other possibility is that the other rules in Formal Semantics are unable to draw any inference of the form statEnv |- $x/title : Type. Now the principle "the absence of an applicable static rule indicates an error" does apply. However, the inference now seems irrelevant because there is no way to reach the first hypothesis, statEnv |- $x/title : Type. Scenario 1 is certainly possible (though I don't know if $x/title is an instance of it). For example, the expressions ((), ()) if $a = $b then () else () let $i := () return $i all have applicable static type rules whose ultimate conclusion is that the type is empty. I don't know if Scenario 2 is possible or not; perhaps $x/title is an example. I think it would help to revise this section to consider these scenarios explicitly, including worked examples, and possibly replace the inference with the one suggested above. If Scenario 2 is not possible, then a statement that (for all Expr) (there exists Type) [statEnv |- Expr : Type] would be very helpful. 5199 1 fred.zemke 2005-07-25 19:38:37 +0000 See comment #1605, additional comment #1, list item 3, in which it is stated that there are indeed expressions for which no type can be deduced. I conclude that there are two scenarios for static type errors: 1. an expression for which no formal type can be deduced 2. an expression for which "statEnv |- Expr : empty" can be deduced, and Expr is not one of the three permitted kinds of expressions of empty type. Note that these two scenarios cannot be reduced to each other. Accordingly, the fix for section 4 "Expressions" is to describe both of these scenarios separately. For scenario 1, there is no inference to state, since the formal language of inferences is not powerful enough to express the concept, "statEnv | not (for all Type) [Expr : Type]". And even if the language was extended to include this kind of judgment, you would have to add the whole machinery necessary to draw conclusions of that sort. Rather, this case is handled through the definition of the inference engine, which should say that the objective is to either conclude "statEnv |- Expr : Type" for some particular Type, given the user's Expr and initial statEnv, or else to conclude that there is no such Type. For scenario 2, it is possible to state an inference, but it is not the one shown in the specification. The correct inference is statEnv |- Expr : empty not (Expr is empty sequence expression () or ... ) -------------------------------------------------- statEnv |- Expr raises typeError 5212 2 simeon 2005-07-26 15:06:30 +0000 Fred, We have had a separate suggestion from Michael Dyck to use the second alternative you suggest, so I think we should use that one. Thanks, - Jerome 5218 3 mrys 2005-07-26 15:34:17 +0000 The working group decided to accept your additional comment 1 (correction to Jerome's comment). 5219 4 mrys 2005-07-26 15:34:52 +0000 We close the bug since we accepted the proposal.