[Bug 1655] New: [FS] need examples of when to raise a type error

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

           Summary: [FS] need examples of when to raise a type error
           Product: XPath / XQuery / XSLT
           Version: Last Call drafts
          Platform: PC
        OS/Version: Windows 2000
            Status: NEW
          Severity: normal
          Priority: P2
         Component: Formal Semantics
        AssignedTo: simeon@us.ibm.com
        ReportedBy: fred.zemke@oracle.com
         QAContact: public-qt-comments@w3.org


4. Expressions
Under "Static type analysis", the discussion of when to raise a
type error is difficult to understand.
It would help to work through the example in more detail.
Consider x/title, where
$x is statically known to have no children.  
I have not been able to figure out how the rules in the rest
of Formal Semantics would actually analyze this, but there
seem to be two possibilities:

1. There are rules that infer 
statEnv |- $x/title : empty.  But in that case, there are
static type rules that apply to the expression $x/title,
by hypothesis.  The principle that "the absence of an applicable 
static rule indicates an error" does not seem to apply.  
Instead, it looks like you want the following inference:

statEnv |- Expr : empty
not (Expr is empty sequence expression () or ... )
--------------------------------------------------
statEnv |- Expr raises typeError

2. The other possibility is that the other rules in Formal
Semantics are unable to draw any inference of the form
statEnv |- $x/title : Type.  Now the principle "the absence of an
applicable static rule indicates an error" does apply.  However,
the inference now seems irrelevant because there is no way to
reach the first hypothesis, statEnv |- $x/title : Type.

Scenario 1 is certainly possible (though I don't know if 
$x/title is an instance of it).  For example, the expressions

((), ())

if $a = $b then () else ()

let $i := () return $i

all have applicable static type rules whose ultimate conclusion is
that the type is empty.  I don't know if Scenario 2 is possible
or not; perhaps $x/title is an example.

I think it would help to revise this section to consider these
scenarios explicitly, including worked examples, and possibly 
replace the inference with the one suggested above.  If Scenario 
2 is not possible, then a statement that 
(for all Expr) (there exists Type) [statEnv |- Expr : Type]
would be very helpful.

Received on Saturday, 16 July 2005 00:41:37 UTC