This is an archived snapshot of W3C's public bugzilla bug tracker, decommissioned in April 2019. Please see the home page for more details.
(This bug is extracted from Bug 5915 comment #2, where it's secondary to that bug's main point.) Consider the query: let $x := if (1) then text{"42"} else 3.14 return -$x which normalizes to something like: let $x := if (1) then text{"42"} else 3.14 return fs:unary-minus( fs:convert-operand( fn:data($x), 1.0E0 ) ) We can infer the following static types: text{"42"} : text? 3.14 : xs:decimal if (1) then text{"42"} else 3.14 : text? | xs:decimal $x : text? | xs:decimal fn:data($x) : (xs:untypedAtomic | xs:decimal)? The last of these types becomes 'Type1' in the Static Type Analysis rules for fs:convert-operand (FS 7.1.1). Note that Type1 <: xs:untypedAtomic? does not hold (because of the presence of xs:decimal in Type1), and so only the first of the four rules applies: statEnv |- not(Type1 <: xs:untypedAtomic?) ------------------------------------------------------------ statEnv |- (FS-URI,"convert-operand")( Type1, Type2) : Type1 Thus the static type of the call to fs:convert-operand is also inferred to be: (xs:untypedAtomic | xs:decimal)? On the other hand, we know that dynamically: $x is bound to a text node, fn:data($x) yields "42" as an xs:untypedAtomic, and fs:convert-operand returns that value cast to xs:double. Since the value of the call does not belong to the static type for the call, this is a violation of type soundness. The rules for fs:convert-operand need to be changed to properly handle such cases.
I propose to replace the rules in 7.1.1 / STA with the following rules. (Note that the second through fifth are minor reworkings of the existing four rules.) statEnv |- Type0 <: xs:anyAtomicType? statEnv |- TypeE <: xs:anyAtomicType prime(Type0) = AtomicTypeName1 | ... | AtomicTypeNameN statEnv |- convert_operand AtomicTypeName1 against TypeE is AtomicTypeName1' ... statEnv |- convert_operand AtomicTypeNameN against TypeE is AtomicTypeNameN' AtomicTypeName1' | ... | AtomicTypeNameN' = TypeR ----------------------------------------------------- statEnv |- (FS-URI,"convert-operand")(Type0, TypeE) : TypeR . quantifier(Type0) statEnv |- not(AtomicTypeName <: xs:untypedAtomic) ------------------------------------------------------- statEnv |- convert_operand AtomicTypeName against TypeE is AtomicTypeName statEnv |- AtomicTypeName <: xs:untypedAtomic statEnv |- TypeE <: xs:untypedAtomic | xs:string ------------------------------------------------------- statEnv |- convert_operand AtomicTypeName against TypeE is xs:string statEnv |- AtomicTypeName <: xs:untypedAtomic statEnv |- TypeE <: fs:numeric ------------------------------------------------------- statEnv |- convert_operand AtomicTypeName against TypeE is xs:double statEnv |- AtomicTypeName <: xs:untypedAtomic statEnv |- not(TypeE <: xs:untypedAtomic | xs:string | fs:numeric) ------------------------------------------------------- statEnv |- convert_operand AtomicTypeName against TypeE is TypeE
While we agree that the new rules you have proposed are correct, recalling your comment from Bug 5915 "The new rules will probably change the static type of fs:convert-operand(data(()), 1) to 'empty'" they are not the most precise. Under your new rules, I think fs:convert-operand(data(()), 1) will come out as xs:double?, rather than the more precise type 'empty'. statEnv |- none <: xs:untypedAtomic statEnv |- xs:double <: fs:numeric ------------------------------------------------------- statEnv |- convert_operand none against xs:double is xs:double statEnv |- empty <: xs:anyAtomicType? statEnv |- xs:double<: xs:anyAtomicType prime(empty) = none statEnv |- convert_operand none against xs:double is AtomicTypeName1' ----------------------------------------------------- statEnv |- (FS-URI,"convert-operand")(empty, xs:double) : xs:double . quantifier(empty) = xs:dobule?
My proposed new rule has the premise prime(Type0) = AtomicTypeName1 | ... | AtomicTypeNameN and in your second inference above, when Type0 is bound to 'empty', you've used the fact (from FS 8.4) that prime(empty) = none to bind N to 1 and AtomicTypeName1 to 'none'. However, the thing to note is that 'none' isn't an AtomicTypeName, rather it's a concrete way of denoting "a choice with zero alternatives". So the proper way to use prime(empty) = none to satisfy the given premise is to bind N to 0. Whereupon: -- the "convert_operand against" premises disappear, -- TypeR is bound to 'none', and -- the type inferred for the convert-operand() call is none . quantifier(empty) = none . ? = empty
Good point. We hadn't spotted that. It might be worth a note in the erratum to avoid misinterpretation.
> It might be worth a note in the erratum to avoid misinterpretation. I'm thinking of adding a Note immediately after the definition of prime(), conveying something like the point of comment #3.
At its meeting on 2008-10-27, the XQuery WG accepted the proposal in comment #1. Consequently, I'm marking this bug resolved-fixed. If you agree with this resolution, please mark the bug closed.
Great, thanks.
This issue has been entered as FS erratum E057, and the proposed fixes have been committed to the source files for the next edition of the FS document. Actually, while working on the erratum, it occurred to me the that same problem can occur with the second argument's type, so I modified the fix to handle that too. Consequently, I'm marking this issue CLOSED.