Re: [Moderator Action (size limit exceeded)] Re: Static Typing in XQ Update Test Suite

> Hello Michael,
>
> OK, it seems I had a wrong or outdated conception of Static Typing.
> (In my defence, it is a feature I have a bit neglected as I deem it
>  not very useful in absence of Schema, since in that case it does not
>  prevent runtime type errors.)
>
> I would like to make just a few remarks (not only for my own sake):
> - I could not find any definition of Static Typing in plain English
>   in the specs, other than this section 5.2.3. In particular there is
> no
>   mention whatsoever of optimistic or pessimistic checking.
>   But perhaps all this it entirely obvious to adepts of Formal
> Semantics.
> - The term "static typing" is in itself too vague and therefore
> confusing.
> - All tests in XQTS related to ST can in fact be passed by an
>   implementation that does *not* support ST but works as stated
>   in section 5.2.3 ...
>
> Cheers
>
> Michael Rys wrote:
> > Hi Xavier
> >
> >  
> >
> > I am not clear I understand your comments. The static typing feature
> > assumes so called pessimistic checks. Which means that an
> > expression /a/b will always infer element(b)* unless a schema
> > guarantees that there is exactly one a containing one b. Also, if
> > the static analysis infers type node()* then a static typing
> > implementation would have to raise an error if there is at least the
> > possibility that it could lead to a runtime type error. The comment
> > you cite below in section 5.2.3 means that you can still do the same
> > static type inferencing in a dynamically typed system as if you
> > support the static typing feature, but you would have to use
> > “optimistic” checks which could lead to some type mismatches be
> > reported statically, but some will be reported dynamically.
> >
> >  
> >
> > So the static typing feature means that an implementation supporting
> > it is supposed to raise an error when the static analysis can
> > determine that an expression _may_ raise an error at runtime.
> >
> >  
> >
> > Best regards
> >
> > Michael
> >
> >  
> >
> > From: www-ql-request@... [mailto:www-ql-request@...] On Behalf
> > Of Xavier Franc
> > Sent: Monday, January 18, 2010 2:15 PM
> > To: www-ql@...
> > Subject: Static Typing in XQ Update Test Suite
> >
> >
> >  
> >
> > Andrew Eisenberg wrote:
> >
> >
> >
> > We are still looking for implementations that support the
> > Update Facility Static Typing Feature and implementations that support
> > XQueryX. We'd like to encourage implementors of these features to submit
> > their results to us, so that we can advance XQuery Update Facility to W3C
> > Recommendation.
> >
> >
> > Dear Andrew,
> >
> > contemplating the test group "Update Facility Static Typing
> > Feature",
> > I think there are some reasons why no implementations so far can
> > pass the related tests:
> > IMHO, there are no more than 10 tests in 27 that really belong to
> > this category and are correct.
> >
> > 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:
> >  [XQ 5.2.3 Static Typing Feature]
> >  If an implementation does not support the Static Typing Feature,
> > but can nevertheless determine during the static analysis phase that
> > an expression, if evaluated, will necessarily raise a type error at
> > run time, the implementation MAY raise that error during the static
> > analysis phase.
> > It is also stated [XQ 2.2.3.1 Static Analysis Phase]:
> >   [Definition: The static analysis phase depends on the expression
> > itself and on the static context. The static analysis phase does not
> > depend on input data (other than schemas).]    
> >
> > * tests of the kind "ST is too vague" are wrong IMO:
> >     a static type node()* can perfectly correspond to correct node
> > types at runtime.
> > * tests of the kind "ST of Target/Source has cardinality greater
> > than one"
> >     - either involve the knowledge of input data (through
> > $input-context),
> >     - or assume that the path-expression will always return several
> > nodes,
> >      which cannot be asserted during static analysis (and BTW it
> > returns exactly one node).
> > * 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.
> >
> > Best regards
> >
> >
>
>