Re: Re: Static Typing in XQ Update Test Suite

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

Re: Re: Static Typing in XQ Update Test Suite

Liam R. E. Quin
[these messages got stuck in the moderation queue because they are
large, or rather because the content-length says they are large...]

On Tue, 2010-01-19 at 02:41 +0000, Xavier Franc wrote:

> 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: [hidden email] [mailto:[hidden email]] On Behalf
> > Of Xavier Franc
> > Sent: Monday, January 18, 2010 2:15 PM
> > To: [hidden email]
> > 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
> >
> >
>
>

--
Liam Quin - XML Activity Lead, W3C, http://www.w3.org/People/Quin/
Pictures from old books: http://fromoldbooks.org/
Ankh: irc.sorcery.net irc.gnome.org www.advogato.org


Reply | Threaded
Open this post in threaded view
|

Re: Static Typing in XQ Update Test Suite

Michael Dyck
On Tue, 2010-01-19 at 02:41 +0000, Xavier Franc wrote:
>
> 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.

Section 2.2.3.1 says:
     Each expression is then assigned a static type (step SQ6).
     [Definition: The *static type* of an expression is a type such that,
     when the expression is evaluated, the resulting value will always
     conform to the static type.] If the Static Typing Feature is
     supported, the static types of various expressions are inferred
     according to the rules described in [XQuery 1.0 and XPath 2.0 Formal
     Semantics]. If the Static Typing Feature is not supported, the static
     types that are assigned are implementation-dependent.

     During the static analysis phase, if the Static Typing Feature is in
     effect and an operand of an expression is found to have a static type
     that is not appropriate for that operand, a type error is raised
     [err:XPTY0004]. If static type checking raises no errors and assigns
     a static type T to an expression, then execution of the expression on
     valid input data is guaranteed either to produce a value of type T or
     to raise a dynamic error.

If you're looking for a definition in plain English, that seems about as
good as you could hope for.

> In particular there is no mention whatsoever of optimistic or
> pessimistic checking.

That's true, but I'm inclined to think the spec is better off not
bringing in those terms. It doesn't need to, and the possible benefit is,
in my opinion, more than offset by the possible harm. (Even within the
Working Group, there is some disagreement about exactly what the terms mean.)

>   But perhaps all this it entirely obvious to adepts of Formal
> Semantics.

Perhaps not *obvious*, but my guess is that it would be fairly clear to
someone who was setting out to implement the Static Typing Feature.

> - The term "static typing" is in itself too vague and therefore
> confusing.

Is there something vague or confusing about the paragraphs I quoted above?

> - 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 ...

Yes, that's a very regrettable situation. I tried to ensure that it
wouldn't happen in the Update Facility's test suite.

-Michael Dyck