[Bug 29586] [XQ31] 2.5.6.2 The judgement subtype-itemtype(Ai, Bi)

https://www.w3.org/Bugs/Public/show_bug.cgi?id=29586

--- Comment #15 from Tim Mills <tim@cbcl.co.uk> ---
ACTION A-643-04: JRobie and Tim to draw up a proposal to resolve bug
29586 (funciton item types).


In DM31 2.8.1 Functions, it is stated that a function has the property:

* signature (a FunctionTest of the form Annotation* TypedFunctionTest): The
TypedFunctionTestXP31 has one SequenceTypeXP31 for each parameter, and one
SequenceType for the function's result. [Definition: A function signature
represents the type of a function.] The presence of annotations is language
dependent; functions defined in languages, such as XPath, that have no
mechanism for defining annotations will create functions in the data model with
zero annotations.

This says that the signature is a FunctionTest, but doesn't say that the
SequenceType for parameter and return type have to match those written in the
function declaration.

As Kike Kay has pointed out, where the specification states that the result of
an expression is of type X, then it is acceptable for the implementation to
return a value of type Y, provided that subtype(Y, X) holds. i.e.
substitutability.

To make it clear that this principal applies to function items, I suggest we
look at the text of

* 3.1.5  Evaluating static and dynamic function calls
* 3.1.6  Named Function References
* 3.1.7  Inline Function Expressions


In 3.1.5.1 Evaluating Static and Dynamic Function Calls, there is a description
of how partial function application results in the creation of a function
item's signature. 

  signature: The signature of F, removing the parameter type at each of the
fixed positions.

As a result of partial function application, the processor might be able to
narrow the signature prescribed in the above text.  THus the signature is as
above or a subtype thereof.



In 3.1.6 Named Function References, there is no description of how the
signature of a named function reference is constructed.  Perhaps this is an
oversight, but it leaves plenty of wiggle room.  For example, an implementation
might want to return a value with signature function(item()*) as
xs:nonNegativeInteger for fn:count#1.


In 3.1.7 Inline Function Expressions, there is a description of how the
signature is constructed: 

  signature: A FunctionTest constructed from the Annotations and SequenceTypes
in the InlineFunctionExpr.

We should state that the signature must be as above or a subtype thereof, as
determined by (static?) analysis of the function's implementation (body?).


In 2.5.6.2 The judgement subtype-itemtype(Ai, Bi), add the rules

* Ai is map(K, V), and Bi is function(xs:anyAtomicType) as V?.
* Ai is array(X) and Bi is function(xs:integer) as X.


The text in 3.1.5.3 Function Coercion then needs to be addressed.

"The map $m has a function signature of function(xs:anyAtomicType) as item()*.
When the fn:filter() function is called, the following occurs to the function:"

 1. The map $m is treated as function ($f), equivalent to map:get($m,?)."

As we've said above, as a result of partial function application, an
implementation may be able to identify a more specific type.  Here, we can say
that the following static typing judgement holds.

statEnv |- $m <: map(K, V)
----------------------------
statEnv |- map:($m, ?) : V?

So the implementation is free to treat $m as matching
function(xs:anyAtomicType) as V?


In "2.5.5.8 Map Test", replace the text

"The function signature of the map, treated as a function, is always
function(xs:anyAtomicType) as item()*, regardless of the actual types of the
keys and values in the map. This means that a function item type with a more
specific return type, such as function(xs:anyAtomicType) as xs:integer, does
not match a map in the sense required to satisfy the instance of operator.
However, the rules for function coercion mean that any map can be supplied as a
value in a context where such a type is the required type, and a type error
will only occur if an actual call on the map (treated as a function) returns a
value that is not an instance of the required return type."

with

"The function signature of the map, treated as a function, is always a subtype
of function(xs:anyAtomicType) as item()*.  The rules for function coercion mean
that any map can be supplied as a value in a context where the required type
has a more specific return type, such as function(xs:anyAtomicType) as
xs:integer, even when the map does not match in the sense required to satisfy
the instance of operator. In such cases, a type error will only occur if an
actual call on the map (treated as a function) returns a value that is not an
instance of the required return type."

Similarly, in "2.5.5.9 Array Test", replace the text

"The function signature of the array, treated as a function, is always
function(xs:integer) as item()*, regardless of the actual member types in the
array. This means that a function item type with a more specific return type,
such as function(xs:integer) as xs:integer, does not match an array in the
sense required to satisfy the instance of operator. However, the rules for
function coercion mean that any array can be supplied as a value in a context
where such a type is the required type, and a type error will only occur if an
actual call on the array (treated as a function) returns a value that is not an
instance of the required return type."

with

"The function signature of the array, treated as a function, is always a
subtype of function(xs:integer) as item()*.  The rules for function coercion
mean that any array can be supplied as a value in a context where the required
type has a more specific return type, such as function(xs:integer) as
xs:integer, evnm when the array does not match in the sense required to satisfy
the instance of operator. In such cases, a type error will only occur if an
actual call on the array (treated as a function) returns a value that is not an
instance of the required return type."

-- 
You are receiving this mail because:
You are the QA Contact for the bug.

Received on Monday, 16 May 2016 09:14:11 UTC