[Bug 3818] Static typing of $input-context1/works[1]/employee[1]/empnum[1]

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

           Summary: Static typing of $input-
                    context1/works[1]/employee[1]/empnum[1]
           Product: XPath / XQuery / XSLT
           Version: Candidate Recommendation
          Platform: PC
        OS/Version: Windows XP
            Status: NEW
          Severity: normal
          Priority: P2
         Component: Formal Semantics
        AssignedTo: simeon@us.ibm.com
        ReportedBy: tim@cbcl.co.uk
         QAContact: public-qt-comments@w3.org


We've found that we can't statically type check:

(: insert-start :)
declare variable $input-context1 as document-node()? external;
(: insert-end :)

count(() is $input-context1/works[1]/employee[1]/empnum[1])

(XQTS test nodeexpression3).

The expression expands to:

count(op::is-same-node((), 
  fs:apply-ordering-mode(
    fs:distinct-doc-order-or-atomic-sequence(
      let $fs::seq as node()* := 
        fs:apply-ordering-mode(
          fs:distinct-doc-order-or-atomic-sequence(
            let $fs::seq as node()* := 
              fs:apply-ordering-mode(
                fs:distinct-doc-order-or-atomic-sequence(
                  let $fs::seq as node()* := $input-context1 return 
                  ( let $fs::last := count($fs::seq) return 
                    ( for $fs::dot at $fs::pos in $fs::seq return 
                      let $fs::seq := child::works return 
                      ( subsequence($fs::seq, 1, 1) ) 
                    )
                  )
                )
              ) return 
              ( let $fs::last := count($fs::seq) return
                ( for $:fs::dot at $fs::pos in $fs::seq return 
                  let $fs::seq := child:::employee return 
                  ( subsequence($fs::seq, 1, 1) )
                )
              )
            )
          ) return 
          ( let fs::last := count($:s::seq) return 
            ( for $:fs::dot at $:s::pos in $:fs::seq return 
              let :fs::seq := child:::empnum return 
              ( subsequence($fs::seq, 1, 1) )
             )
          )
        )
      )
    )
  )
}

The sxpressions works[1], employee[1] and empnum[1] can all be typed as
element()?, (under the rules of 7.2.13).  However the use of "let fs::seq as
node()*" means that fs:seq gets typed as node()*, rather than the more specific
type element()?.

By the end of this, we can only tell that:

$input-context1/works[1]/employee[1]/empnum[1]

is of type node()*, when it is obviously element()?.

In 4.8.3 Let Expression, the typing rule states that:

statEnv |-  Expr1 : Type1
Type0 = [ SequenceType ]sequencetype
statEnv  |-  Type1 <: Type0
statEnv  |-  VarName of var expands to Variable
statEnv + varType(Variable1 => Type0 )  |-  Expr2 : Type2
------------------------------------------------------------------------
statEnv |-  let $VarName1 as SequenceType := Expr1 return Expr2 : Type2

i.e. $VarName1 gets treated as having type Type0, not the more specific type
that Type1.  Shouldn't Variable1 have type Type1?

Received on Thursday, 12 October 2006 10:25:12 UTC