Consider the following: () castable as xs:integer According to Formal Semantics (4.12.4), this expands out to: let $v := fn:data(()) as xs:anyAtomicType return $v castable as xs:integer This would mean that the expression would throw an XPTY0004 error, although this seems undesirable (and is not mentioned in the XQuery spec). Similarly (1,2) cast as xs:integer? throws an error, whereas XQuery seems to suggest that "false" should be returned.
See also bug #4873 (which doesn't address exactly the same point, but does point out that there are drafting problems with the spec of "castable as".)
To address the two cases in Comment #0, we could change the normalization rules in FS 4.12.4 so that the type of $v is xs:anyAtomicType*. At that point, I think the introduction of $v ceases to have any purpose, so we could "inline" its definition, and even collapse the two rules into one: [[ Expr castable as SingleType ]]_Expr == fn:data(( [[Expr]]_Expr )) castable as SingleType However, this would still have the problem (alluded to in Comment #1) that failure to atomize the value of Expr would raise FOTY0012 rather than cause the CastableExpr to yield false. (The latter being the correct behaviour, as indicated by Bug 4873 comment #1.) Therefore, I believe atomization needs to be pushed down into the core dynamic samantics of 'castable', rather than being exposed by normalization. So the normalization rule should be: [[ Expr castable as SingleType ]]_Expr == ( [[Expr]]_Expr ) castable as SingleType But I'm not yet sure what the dynamic evaluation rules should be. (Currently, the DE rules don't address the AtomicType? case, and the second DE rule has numerous bugs, so I'd want to propose rules that fix those problems too.)
For 4.12.4 Castable, I think the Dynamic Evaluation rules should be: dynEnv |- Expr => Value Value can be cast to SingleType ---------------------- dynEnv |- Expr castable as SingleType => true dynEnv |- Expr => Value not( Value can be cast to SingleType ) ---------------------- dynEnv |- Expr castable as SingleType => false where the auxiliary judgment "Value can be cast to SingleType" is defined by the following rules: -------------- () can be cast to AtomicType? Value can be cast to AtomicType -------------- Value can be cast to AtomicType? fn:data(Value) = AtomicValue1 AtomicValue1 cast value to type AtomicType => AtomicValue2 -------------- Value can be cast to AtomicType
At their meeting today, the WGs approved the proposed solution, so I am marking this issue resolved-fixed. If you agree with this resolution, please close the issue.
This issue has been entered as FS erratum E032, and its fix has been committed to the source files for the next edition of the FS document. Consequently, I'm marking this issue CLOSED.