This is an archived snapshot of W3C's public bugzilla bug tracker, decommissioned in April 2019. Please see the home page for more details.
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.
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
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
The working group decided to accept your additional comment 1 (correction to Jerome's comment).
We close the bug since we accepted the proposal.