Re: Static Typing in XQ Update Test Suite

Xavier Franc wrote:
> 
> As far as I understand the static typing feature, an implementation 
> supporting it is supposed to raise an error when the static analysis can 
> determine that an expression will *certainly* raise an error at runtime:

It must raise an error in such cases, but more generally it must raise a
type error if it *cannot* determine that an expression would certainly
*not* raise a type error at runtime. That is, if it cannot prove that the
expression is type-safe, it must raise a type error.


> * tests of the kind "ST is too vague" are wrong IMO:
>     a static type node()* can perfectly correspond to correct node types 
> at runtime.

Yes, but it can also "correspond to" nodes that have incorrect types, and
so it's not type-safe.

> * tests of the kind "ST of Target/Source has cardinality greater than one"
>     - either involve the knowledge of input data (through $input-context),

On the contrary, knowledge of the input data would tell you that the
runtime cardinality would be at most one.

>     - or assume that the path-expression will always return several nodes,
>      which cannot be asserted during static analysis

Static type analysis doesn't assume that the expression will *always*
return several nodes, but it recognizes the possibility that it might.
(More precisely, it is unable to prove that it won't.)

> (and BTW it returns exactly one node).

Yes, that is very much intended. That way, the test distinguishes between
an implementation that does static type analysis (and raises an error)
and one that doesn't do it (and doesn't raise an error, because the
runtime cardinality is fine).

> * Test "stf-insert-02: insert: ST of SourceExpr has non-attribute before 
> attribute.":
>    although this error can indeed be detected by static analysis, that 
>    seems far too complex, and looks more like "formal proof of program"
>    than like what a compiler can achieve.

Static type analysis *is* a formal proof. The XQuery/XPath Formal
Semantics document is chock full of inference rules that a compiler can
use to carry out the proof. In this particular case, I don't think the
proof is that complex.

-Michael Dyck

Received on Tuesday, 19 January 2010 02:33:38 UTC