[Bug 1728] [FS] stronger inference is possible in 7.2.13 "fn:subsequence"

http://www.w3.org/Bugs/Public/show_bug.cgi?id=1728


simeon@us.ibm.com changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|REOPENED                    |ASSIGNED




------- Additional Comments From simeon@us.ibm.com  2005-07-21 21:57 -------
Yes you are right. I got a closer look at where fn:subsequence is used in
normalization of predicates and we have at least three specific changes to make
it consistent:

 (1) Add a specific static typing rules for $fs:position, in [Section 7.2.13 The
fn:subsequence function], as follows:

statEnv |- Expr : Type      quantifier(Type) in { * }
------------------------------------------------------------
statEnv |- fn:subsequence(Expr, $fs:last, 1) : prime(Type) ?

 (2) Add a normalization rule for PrimaryExpr[last()] in [Section 4.3.2 Filter
Expressions]. I think this has just been overlooked.

 [| PrimaryExpr PredicateList [ last() ] |]Expr
  ==
 let $fs:sequence := [PrimaryExpr PredicateList]Expr return
 fn:subsequence($fs:sequence,last(),1)

 (3) Remove the second inference rule in [Section 7.2.13 The fn:subsequence
function]:

statEnv |- Expr : Type      quantifier(Type) in { 1, + }
---------------------------------------------------------
statEnv |- fn:subsequence(Expr, $fs:last, 1) : prime(Type)

I believe this rule will not be type safe, when the normalization result from 
something else than a predicate. For instance:

 $x//a/fn:subsequence(1,last(),1)

NOTE: this last problem is subtle and somewhat worrying. We may want to
reconsider the use of fn:subsequence for predicates, and instead use a
fs:subsequence function which will be introduced only for the normalization of
predicates (with will be dynamically equivalent to fn:subsequence, but with the
more precise typing rules), and use the simpler more general rule consistently
for fn:subsequence.

- Jerome

Received on Thursday, 21 July 2005 21:57:12 UTC