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

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





------- Comment #7 from tim@cbcl.co.uk  2006-11-03 08:17 -------
"When I assert EXP treat as element(employee) I am asserting that EXP will
always return an employee. I want the system to tell me if EXP doesn't return
an employee, but I don't want it to reject my query because the system was able
to work out for itself that EXP was an employee without my telling it."

In your example above, the user has told the system explicitly that EXP will
always return an employee.  However, in some cases the system is able to
determine that not only would EXP return an employee, but it would return some
specific subtype of employee.  In doing so, the system is capable of _not_
rejecting some queries.  However, the current type rules are preventing use of
this information.  So there exist situations in which a user, in trying to add
extra type information, is actually forcing to the system to throw away more
specific type information and _causing_ a query to be rejected.


Consider:

Type S, type T where S is a subtype of T.
Function f($arg as S) as xs:boolean
Variable $s, proven to be of type S*.
Query: some $x as T in $s satisfies f($x)

With the current typing rules, $x is treated as if it had type T, so this
statement fails static typechecking because function f requires an argument of
type S.

With static type checking turned off, this query will succeed.

However, since the system already knows that $s is of type T*, it can infer
that:
1. each $x must be of type S
2. S is a subtype of T, therefore no dynamic typing errors will be raised.
3. f($x) is therefore type-checkable.

The current typing rules mean that it is forced to forget (1) above, because
the typing rule states that we must treat $x as being of type T.  This leads to
the unnecessary rejection of this query.

I'd argue that 

$s treat as T 

should have static type S if we know that type($s) = S and S is a subtype of T;
otherwise, it should have static type T.

Received on Friday, 3 November 2006 08:17:22 UTC