This is an archived snapshot of W3C's public bugzilla bug tracker, decommissioned in April 2019. Please see the home page for more details.
7.1.3 The fs:convert-operand function The last three inferences under "Static type analysis" are inadequate because Type1 is not deterministic. What is wanted is that Type1 is the minimal type such that Expr1 <: Type1. For example, suppose Expr1 is 1.3. So Expr1 <: xs:decimal, but also Expr1 <: xs:decimal? and Expr1 <: xs:decimal+ and Expr1 <: xs:decimal*. And many other types could go on the right hand side. It wouldn't matter much except that quantifier(Type1) is required in the conclusion, and we don't know whether the correct quantifier is 1, ?, + or *. The solution might be to create a judgment that Type1 is the best static type of Expr1. Or the solution might be to create a judgment that Quantifier1 is the best quantifier of Expr1. I notice that many other subsections of 7.1 could use such judgments. This comment is related to two other comments: 1. #1612: We need to spell out the quantifiers in inferences (is it "for all Type1" or "there exists Type1"?) 2. #1605: We need to define the inference engine (how does the engine know when it has computed enough inferences? For example, "1.3 <: xs:decimal*" is correct, so can the inference engine stop when it finds that one, and never find the tighter inference that "1.3 <: xs:decimal"?
7.2.3 "fn:abs, etc." and 7.2.10 "fn:min, etc." are some other sections that would benefit from a judgment to find the "best" promotion.
This is one of the few cases, where the available formalism cannot be fully precise. Rather than change the whole approach, I would probably prefer adding some clarification in prose next to the rule, indicating that in cases several types can be inferred, the 'best' one is chosen. This could be done also using a 'semi formal' judgment like 'Type1 is most precise', which could be defined in prose. Would you be satisfied with that approach? - Jerome
I think this may be one of the places in the spec that logically depend on the execution model of the inference engine. See my proposed description of the inference engine in comment #1605 as an additional remark. If the inference engine is conceptually "firing" an inference whenever it detects that the premises of the inference are fulfilled, in a non-deterministic order, then you know when you have deduced that "|- Expr : Type" for some specific Expr and Type, but you never know whether you have found the "best" Type. In addition, you cannot have a judgment of the form "statEnv |- (for all Type1)[ if Expr : Type2 then Type1 <: Type2 ]" which is conceptually what is needed for the informal judgment, "statEnv |- Type1 is the best formal type for Expr". The reason is that the inference engine is not powerful enough to prove theorems about "for all" statements, it is only powerful enough to deduce single concrete judgments. You are right, we don't want to start over, so perhaps an English-language definition of a judgment "statEnv |- Type1 is the best type for Expr" is needed. But supplying a hand-wavy definition looks like a big conceptual hole that I would rather see filled. A bottom-up implementation would start at the leaves of the parse tree and recursively decide the best static type for each node of the tree. It is possible to model bottom-up implementations using an inference engine as described in my comment #1605. The thing is, don't bother to define "statEnv |- Expr : Type" via inferences. Instead, define "statEnv |- Type is the best formal type for Expr" for each kind of expression.
Huh? I don't get it. Surely "Expr <: Type" is just a typo for "Expr : Type". See Bug 1745, last comment.
regarding additional comment 4, you are right, my use of <: was a mistake; the correct symbol is : in judgments such as Expr : Type. regarding additional comment 5, I can accept a prose description of choosing the best type, especially if there is a judgment of the form "Type is the best formal type for Expr". As to the definition of "best", is it possible to define it as follows: "The best formal type for a [query/expression] Expr is that Type1 such that, for all formal types Type2, if 'statEnv |- Expr : Type2' is inferrable, then 'statEnv |- Type1 <: Type2' is inferrable"? This would define the best formal type as the minimal formal type. However, I don't know the Formal Semantics well enough to know if there always is a minimum formal type for an expression. Once you have a definition of the best type, then the best quantifier is presumably the OccurrenceIndicator of the best type.
Sorry, what I mean is: I don't understand why the concept of "best" type is needed here. I don't see how "Type1 is not deterministic". Is it possible to infer two distinct static types for an expression? If Expr1 is 1.3, then Expr1 : xs:decimal, but I don't think you can go from there to Expr1 : xs:decimal? etc.
If indeed every Expr has only one Type such that statEnv |- Expr : Type, then there is no problem. Perhaps we could add an informative note to this effect in some convenient place? By the way, I see that the incorrect usage, Expr <: Type, is found in some of the inferences in 7.1.3 "fs:convert-operand".
I think I take it back and that Michael is right. We don't really need the best type in this particular case. There are a few places where we need it (in type promotion for instance), but not there. We do need to fix all the Expr <: Type into Expr : Type though. - Jerome
The working group decides to fix the Expr <: Type issue as outlined. The informative note was discussed but the working group decided not to add it (the response to 1605 covers this). Please close the issue if you agree with the resolution or reopen the issue if you disagree.