About the Typing Rule for "Let Expression" in XQuery

To Who It May Concern,

I try to use an simple example to test the static typing of XQuery 
expression,
but find something strange.

I think the typing rule for Let Expression is not precise in some way.
statEnv |-  Expr1 : Type1
Type0 = [ SequenceType ]sequencetype
statEnv  |-  Type1 <: Type0
statEnv  |-  VarName1 of var expands to Variable1      statEnv + 
varType(Variable1 => Type0 )  |-  Expr2 : Type2
 --------------------------------------------------------------------------------
statEnv |-  let $VarName1 as SequenceType := Expr1 return Expr2 : Type2
I think the Type0 as above should be Type1.

For example, if we look at this expression: doc("Catalogue.xml")/catalogue
(The XML file and schema file is as attached.)
According to "XQuery 1.0 and XPath 2.0 Formal Semantics", it should be 
"normalized" into Core Grammar, as
fs:apply-ordering-mode (
fs:distinct-doc-order-or-atomic-sequence (
   let $fs:sequence as node()* :=doc("Catalogue.xml") return
   let $fs:last := fn:count($fs:sequence) return
   for $fs:dot at $fs:position in $fs:sequence return
     child::catalogueExpr
))

When we try to type the underlined part, we will first get that 
"doc("Catalogue.xml")" is of type "document{element catalogue of type 
Catalogue}"
And we using the typing rule for Let Expression, like this:

statEnv |- doc("Catalogue.xml") : Type1
Type1 = document{element catalogue of type Catalogue}
Type0 = [  node()* ]sequencetype=
((element * of type xs:anyType | attribute * of type xs:anySimpleType | 
text | document { (element * of type xs:anyType | text | comment | 
processing-instruction)* } | comment | processing-instruction))*
statEnv  |-  Type1 <: Type0
statEnv  |-  $fs:sequence of var expands to Variable1     
statEnv + varType(Variable1 => Type0 )  |-  for $fs:dot at $fs:position 
in $fs:sequence return child::catalogue : Type2
--------------------------------------------------------------------------------
statEnv |-  let $fs:sequence as node()* := doc("Catalogue.xml") return 
for $fs:dot at $fs:position in $fs:sequence return child::catalogue: Type2

Then we try to type "for $fs:dot at $fs:position in $fs:sequence return 
child::catalogue" using the typing rule for For Expression:
statEnv |-  Expr1 : Type1
statEnv |-  VarName1 of var expands to Variable1
statEnv |-  VarNamepos of var expands to Variablepos
statEnv + varType(Variable1 => prime(Type1);Variablepos => xs:integer)  
|-  Expr2 : Type2
--------------------------------------------------------------------------------
statEnv |-  for $VarName1 at $VarNamepos in Expr1 return Expr2 : Type2 · 
quantifier(Type1)
 
So, we will get
statEnv + varType(Variable1 => Type0 )|-  $fs:sequence : Type0
statEnv + varType(Variable1 => Type0 )|-  $fs:dot of var expands to 
Variable2
statEnv + varType(Variable1 => Type0 )|-  $fs:position of var expands to 
Variablepos
statEnv + varType(Variable1 => Type0 )+ varType(Variable2 => 
prime(Type0);Variablepos => xs:integer)  |-  child::catalogue: Type2
where Type0= ((element * of type xs:anyType | attribute * of type 
xs:anySimpleType | text | document { (element * of type xs:anyType | 
text | comment | processing-instruction)* } | comment | 
processing-instruction))*
prime(Type0)=
(element * of type xs:anyType | attribute * of type xs:anySimpleType | 
text | document { (element * of type xs:anyType | text | comment | 
processing-instruction)* } | comment | processing-instruction)
--------------------------------------------------------------------------------
statEnv + varType(Variable1 => Type0 )  |-  for $fs:dot at $fs:position 
in $fs:sequence return child::catalogue : Type2

Actually, we need to decide Type2:
statEnv + varType(Variable1 => Type0 )+ varType(Variable2 => 
prime(Type0);Variablepos => xs:integer)  |-  child::catalogue: Type2
Since $fs:dot is of type prime(Type0)= (element * of type xs:anyType | 
attribute * of type xs:anySimpleType | text | document { (element * of 
type xs:anyType | text | comment | processing-instruction)* } | comment 
| processing-instruction)
We can easily get Type2 to be something like (element catalogue of type 
xs:anyType)*
But it is not the case!
If what I mentioned at the beginning is right, Type0 should be 
"document{element catalogue of type Catalogue}".
Since $fs:dot is of type prime(Type0)= document{element catalogue of 
type Catalogue}, then Type2 is "element catalogue of type Catalogue"

I just would like to make sure whether it is correct about my thinking.
Thank you,
Selina

Received on Monday, 2 October 2006 11:31:53 UTC