[XQuery] Issue raised by formal definition of SequenceType Matching

The following issue was identified during formal definition of
SequenceType matching.  Resolution of this issue is necessary to
complete closure of Issue 559 (New Sequence Type needs to be fully
implemented in Formal Semantics).

(For W3c members, please see 9 Dec FS editors' draft at: 
  http://lists.w3.org/Archives/Member/w3c-archive/2003Dec/0022.html
In particular
 
http://lists.w3.org/Archives/Member/w3c-archive/2003Dec/0022.html#sec_type_matching
 
http://lists.w3.org/Archives/Member/w3c-archive/2003Dec/0022.html#jd_aux_derives_from
)

Background
==========
The subtype relation, which is the basis of static typing is defined
as follows:

  Type1 is a subtype of Type2

if-and-only-if

  for every Value such that 
    Value matches Type1
  then 
    Value matches Type2

Notice that _subtyping_ (the relation between two types) is defined in
terms of _matching_ (the relation between values and a type).
Therefore, for the definition of static typing to be self-contained in
the Formal Semantics, _matching_ must also be defined completely (and
preferably normatively) in the Formal Semantics.  It would be nice if
the Formal Semantics could refer to the normative definition of
sequence-type matching in the language book [Section 2.4.4
SequenceType matching], but this is not possible, because this section
only specifies matching rules for a _subset_ of XML Schema types
(i.e., those expressible as SequenceTypes), whereas the Formal
Semantics requires matching rules for all possible types.

We are _not_ asking that we revisit the issue of what is normative
text that began with this thread:
  
  Normativity statement in language book
 
http://lists.w3.org/Archives/Member/w3c-query-editors/2003Oct/0206.html

What we are asking is that the correspondence between the rules in
[Section 2.4.4 SequenceType matching] be more closely correlated by
(1) including cross-document links and (2) aligning the terminology
_exactly_.

Prolems with current definitions
================================

type-matches
------------

1. type-matches defines a relation on _type names_, not on the types
   that they denote. Also, "type-matches" is a poor name as it
   specifies the derivation relationship between two type names, not
   the sequence matching relation between a value and a type.
   
2. FS Section [7.2.1 Derives from] gives the formal definition of
   type-matches, which is called derives-from in the FS doc.

   The two sections should use the same terminology and provide
   equivalent definitions. 

3. The current definition of type-matches in the language book is not
   completely transitive, because the "one or more steps" clause
   should be applied to both rules (1) and (2).

   To illustrate, type-matches(Person,Student) should return true if:

     1. Student is a known type and is derived by one or more steps of
        restriction or extension from Person 
   and 
     2. UGrad is an unknown type, and an implementation-dependent
        mechanism is able to determine that UGrad is derived by
        restriction from Student. 

   The current definition does not adequately cover this case.

type matching
-------------

1. The text in the language book should point to Section [7.4.1
   Matches].

2. The two sentences in [2.4.4 Sequence Type Matching] starting as:
   "These rules are a subset of the static typing rules defined in FS,
   which compares ...." are not right. The relationship that should be
   established here is between values and types.

   See "Suggested changes" below for corrected text.

Based on the explanation above, here are :

Suggested changes to [Section 2.4.4 SequenceType Matching]:
===========================================================
[To editor: No changes to Definition or Note]

The rules for SequenceType matching compare the actual type of a value
with an expected type. These rules are a subset of the formal rules
that match a value with an expected type defined in <xspecref
spec="FS" ref="sec_type_matching"/>.  These rules are a subset of the
rules in the Formal Semantics, because the Formal Semantics must be
able to match a value with any XML Schema type, whereas the rules
below only match values against those types expressible by the
SequenceType syntax.

Some of the rules for SequenceType matching require determining
whether a given type name is the same as or derived from an expected
type name.  [ In rest of paragraph, replace all occurrences of "type"
by "type name". ]

We define the pseudo-function named derives-from(AT, ET), which takes
an an actual simple or complex type name AT and an expected simple or
complex type name ET, and either returns a boolean value or raises a
type error. [err:XP0004][err:XP0006] The pseudo-function "derives-from"
is
defined as follows and is defined formally in <xspecref spec="FS"
ref="jd_aux_derives_from"/>.

  * derives-from(AT, ET) returns true if:

    1. AT is a type name found in the in-scope schema definitions, and
       is the same as ET or is derived by restriction or extension
       from ET, or

    2. AT is a type name not found in the in-scope schema definitions,
       and an implementation-dependent mechanism is able to determine
       that AT is derived by restriction from ET, or

    3. There exists some type T_1 such that derives-from(AT, T_1) and
       derives-from(T_1, ET) are both true.

[To editor: the point of the last rule is that 1. and 2. are mutually
transitive.  This relationship is missing in the current rules.] 

  * derives-from(AT, ET) returns false if:

    1. AT is a type name found in the in-scope schema definitions, and
       AT is not the same as ET or is not derived by restriction or
       extension from ET, or

    2. AT is a type name not found in the in-scope schema definitions,
       an implementation-dependent mechanism is able to determine that
       AT is not derived by restriction from ET, or

    3. There does not exist any type name T_1 such that
       derives-from(AT, T_1) and derives-from(T_1, ET) are both true.

  * derives-from(AT, ET) raises a static error [err:XP0004][err:XP0006]
if:
    1. ET is a type name not found in the in-scope schema definitions,
or
    2. AT is a type name not found in the in-scope schema definitions,
       and the implementation is not able to determine whether AT is
       derived by restriction from ET.

Note:

  The derives-from pseudo-function can not be written as a real XQuery
  function, because type names are not valid function parameters.

[To editor: All other occurrences of type-matches(ET, AT) in the
remaining rules should be changed to derives-from(AT, ET).]
-- 
Mary Fernandez <mff@research.att.com>
AT&T Labs - Research

Received on Wednesday, 21 January 2004 14:13:14 UTC