On Wed, Nov 29, 2006 at 08:40:59PM +0800, Wang Zhen (Selina) wrote:

As you said, your work "goes beyond the actual requirements in the W3C specs", is it because in some aspect, the requirements in the W3C specs is not enough? Or, is it because the implementation of W3C specs are difficult or cause some problems?

When the development of Pathfinder started, it had not yet been clear what kind of subtype relationship the XQuery language would use. For quite a while, the W3C drafts depended on /structural subtyping/, which (computationally) is much more expensive than the /named typing/ that you find now in the W3C documents.

The XML structure leads to tree-structured types. The structural subtype relationship is now decided by looking at the full structure of both types and testing, whether each instance of the one type will always be an instance of the other type.

Example:

Consider the two types

t1 := element a { element b { item* } } t2 := element a { element b { item* }, element c { item* }? }

(that is, an element `a' with a single `b' child of arbitrary content, and an element `a' with a `b' and an optional `c' element in its content)

In this example, each instance of type t1 will always be an instance of type t2, thus t1 <: t2.

Testing this relationship can be quite expensive, which probably is why structural typing didn't make it into the current Candidate Recommendation of the specs. These specs now use named typing. Here, it is assumed that items are annotated with a type /name/ and that there is a hierarchy (the derivation hierarchy) between type names. To test a subtype relationship, one only has to look at the two names now, but /not/ at their full structure.

The Pathfinder compiler includes a full implementation of a structural subtype algorithm (we use the one described in [1,2]). In some occasions, this allows the inference of a more precise type information. Our system does not yet include validation support, but we expect that the structural type information can help to avoid an expensive validation if we can statically derive that validation will succeed.

Besides, do you provide a formal document, or any tutorials about the actual static typing you have achieved?

Sorry, but we haven't. You find the subtype algorithm we use in the references below. Our inference rules more or less follow the W3C specs, though the implementation needs quite some work.

Regards,

Jens

[1] Martin Kempa, Volker Linnemann. Type Checking in XOBE. BTW 2003.

[2] Martin Kempa. Programmierung von XML-basierten Anwendungen unter Berücksichtigung der Sprachbeschreibung. PhD thesis, U Lübeck, Germany, 2003.