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

[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,
>=20
> 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=20
>  not very useful in absence of Schema, since in that case it does not=20
>  prevent runtime type errors.)
>=20
> 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=20
>   in the specs, other than this section 5.2.3. In particular there is
> no
>   mention whatsoever of optimistic or pessimistic checking.=20
>   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=20
>   implementation that does *not* support ST but works as stated=20
>   in section 5.2.3 ...
>=20
> Cheers
>=20
> Michael Rys wrote:=20
> > Hi Xavier
> >=20
> > =20
> >=20
> > 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
> > =E2=80=9Coptimistic=E2=80=9D checks which could lead to some type misma=
tches be
> > reported statically, but some will be reported dynamically.
> >=20
> > =20
> >=20
> > 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.
> >=20
> > =20
> >=20
> > Best regards
> >=20
> > Michael=20
> >=20
> > =20
> >=20
> > From: [email protected] [mailto:[email protected]] On Behalf
> > Of Xavier Franc
> > Sent: Monday, January 18, 2010 2:15 PM
> > To: [email protected]
> > Subject: Static Typing in XQ Update Test Suite
> >=20
> >=20
> > =20
> >=20
> > Andrew Eisenberg wrote:
> >=20
> >=20
> >=20
> > We are still looking for implementations that support the=20
> > Update Facility Static Typing Feature and implementations that support=
=20
> > XQueryX. We'd like to encourage implementors of these features to submi=
t=20
> > their results to us, so that we can advance XQuery Update Facility to W=
3C=20
> > Recommendation.
> >=20
> >=20
> > Dear Andrew,
> >=20
> > 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.
> >=20
> > 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).]    =20
> >=20
> > * 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,=20
> >      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=20
> >    far too complex, and looks more like "formal proof of program"
> > than=20
> >    like what a compiler can achieve.
> >=20
> > Best regards
> >=20
> >=20
>=20
>=20

--=20
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