Semi-strict static typing: reporting implausible expressions

[michaelhkay]

Strict static typing, as originally defined for XQuery 1.0, was not a success, because it prohibits too many constructs that are perfectly reasonable to write. However, the alternative, pure dynamic typing, prevents a processor reporting many obvious errors at compile time. A compromise is optimistic static typing, where the processor is allowed to report a type error statically in the cases where it can be shown that evaluation of an expression is bound to fail at run-time.

Optimistic static typing has proved a reasonably successful compromise, but there are a number of cases where things that are obviously user mistakes cannot be reported as static errors. I propose that a processor should be allowed (not required) to treat some of these conditions as static errors.

The first of these conditions is exemplified by passing an argument whose static type is xs:integer* to a function where the declared parameter type is xs:string*. Under optimistic static typing this cannot be reported as a static error, because it is not bound to fail; if the actual value at run-time turns out to be an empty sequence, the call will succeed. So the proposal is that where the inferred supplied type and the required sequence types are both emptiable (that is, occurrence indicator is "?" or "*"), but their respective item types are disjoint, the processor should be allowed to report a static error.

The second condition is what I call a void path expression. Specifically, if we know statically that the result of $A/B, or $A!B, or $A?B will be an empty sequence for any possible value of $A (given its inferred type), this almost certainly means the user has made a mistake, and we should be allowed to report a static error. This extends to the unary or implicit forms of these operators, based on the inferred type of the context item. This is most likely to occur with schema-aware code, where it should be possible to report a path such as A/B/C/D as incorrect if the schema does not allow such a path. But it also arises for example for $A?B if the inferred type of $A is a non-extensible record type and B is not one of its known fields; and it arises for inappropriate combinations of axes such as @code/text().

Note that I'm not proposing (as XQuery 1.0 static typing did) that any expression whose result is bound to be empty is a static error; the rule is confined to a few specific operators.

Perhaps, for backwards compatibility and interoperability, we should require processors to provide an option to switch this kind of static error detection off. (For example, XSLT 1.0 code sometimes deliberately uses /.. to represent an empty sequence, and this construct would be flagged under these rules.)

[ChristianGruen]

So the proposal is that where the inferred supplied type and the required sequence types are both emptiable (that is, occurrence indicator is "?" or "*"), but their respective item types are disjoint, the processor should be allowed to report a static error.

To understand this correctly: I assume it’s already allowed to report a static error if the types are not emptiable?

The second condition is what I call a void path expression. Specifically, if we know statically that the result of $A/B, or $A!B, or $A?B will be an empty sequence for any possible value of $A (given its inferred type), this almost certainly means the user has made a mistake, and we should be allowed to report a static error. […] it arises for inappropriate combinations of axes such as @code/text().

I know cases in which UIs generate paths dynamically, based on steps (element names, node kinds) provided by the user input, and in which the generated path is dynamically evaluated by the processor. An error may be unexpected. But that’s subject to discussion (some developers would possibly welcome a stricter handling of such input).

You proposed anyway that the processor errors would be optional, not mandatory. I think that would be fine.

[michaelhkay]

To understand this correctly: I assume it’s already allowed to report a static error if the types are not emptiable?

Correct. §2.4.1:

If an implementation can determine during the [static analysis phase] that ... an expression, if evaluated, would necessarily raise a [type error], the implementation may ... report that error during the [static analysis phase].

The problem with emptiable sequence types (xs:integer* versus xs:string*) is that it won't necessarily fail.