RE: question about subtyping and type annotations

On Fri, 24 Feb 2006, Michael Kay wrote:

>
>> Section 3.12.5 Constructor Functions seems to be pretty clear
>> about it:
>
> That only says they are equivalent to casts. Are casts exempt from the
> general rule of substitutability, which says that any expression can return
> a value whose dynamic type is a subtype of the required type?
>

Could the following make sense?:

The substitutability is a (1) non-normative _property_ of a [good] 
language spec rather than a (2) normative statement in a language spec 
that uniformly tweaks definitions of all the language's constructs.

If so, XQuery casts do satisfy the substitutability property (1). 
(Implementing them differently, as Michael suggests, wouldn't violate (1), 
but would change the language semantics, since such implementation would 
contradict the rules in 3.12.3.)

Perhaps, some confusion can be avoided by changing the phrase in 
3.12.3.4.b

   "... the input value is mapped into the value space of the target type,
        unchanged except for its type. "

to highlight that the "type" here is _dynamic_, similar to the 
corresponding phrase in 3.12.3.4.d:

   "The resulting value is the same as the input value, but with a
    different dynamic type."

The intent is the same in both cases, isn't it?

Vladimir

Received on Friday, 24 February 2006 19:41:43 UTC