ORA-FS-004-E: Formal Semantics comments, precise types

There are a number of places in the Formal Semantics spec where it
chooses a static type that is more general than the most specific type 
that is deducible.

While we understand that an implementation is free to extend static typing
to produce more specific types than the Formal Semantics spec says [1],
we think it is important for the spec to choose the most specific type 
possible.

Examples of places in the Formal Semantics where a more-specific type is 
desirable:

----------------------------------------------------

1. SECTION 4.8.2 for expression

431: for expression type

Under static type analysis, when a type declaration is present,
the static environment should be extended to typing VarRef1 with type 
Type1, NOT type0.

----------------------------------------------------

2. SECTION 4.8.3, let expression

432: let expression type
bug

The let expression variable has its declared type, instead of its actual 
type,
entered into the static environment.

Under static type analysis, when a type declaration is present,
the static environment should be extended to typing VarRef1 with type 
Type1, NOT type0.

----------------------------------------------------

3. SECTION 5.12, Function Declaration

454: function return type vs declared return type

Example:
declare function foo() as xdt:anyAtomicType {return 3;}
foo() + 4

When doing static type analysis on foo() +4, should foo()'s static
type be xdt:anyAtomicType or xs:integer ?

According to the current spec, foo()'s static type is xdt:anyAtomicType.
Then foo() +4 raises static type error.

foo()'s static type should be xs:integer so that foo() +4 does
NOT raise static type error.

----------------------------------------------------

4. SECTION 6.2.8, fn:reverse function

442: explain why factored type is used here
bug/editorial

It may not be obvious why the static Type analysis for fn:reverse()
function actually returns the factored type of the function's
input sequence.

For example, consider:
fn:reverse((1, 'abc')).

The input sequence type is (xs:integer, xs:string).
After applying fn:reverse(), its most precise type should be (xs:string, 
xs:integer).

If we compute the factored type, its type
is (xs:string|xs:integer)+ , which is NOT as precise as
(xs:string, xs:integer).

Suggest: either return the most precise type (preferred solution),
or add some text to explain why a factored type is used here.

----------------------------------------------------

[1] From the Formal Semantics spec:

3.6.7 Static Typing Extensions

For some expressions, the static typing rules defined in the Formal 
Semantics are not very precise (see, for instance, the type inference 
rules for the ancestor axes — parent, ancestor, and ancestor-or-self— 
and for the function fn:root function. Some implementations may wish to 
support more precise static typing rules.

A conforming implementation may provide a static typing extensionXQ, 
which is a type inference rule that infers a more precise static type 
than that inferred by the type inference rules in the Formal Semantics. 
Given an expression Expr, the type of Expr given by the extension must 
be a subtype of the type of Expr given by the Formal Semantics. "

Received on Friday, 16 April 2004 00:00:59 UTC