question about subtyping and type annotations

[Per Bothner]

I'm unclear on the semantic model for type annotations, and I can't
find a clear answer in the specifications or in the test suite.

I gather (and Saxon agrees) that:
   100 instance of xs:byte ==> false
because 100 has "type annotation" xs:integer, which is not a sub-type
of xs:byte.

Using the cast xs:byte creates a value with type annotation xs:byte:
   xs:byte(100) instance of xs:byte ==> true

What about xs:integer(xs:byte(100))?  I would expect this to return
a value with type annotation xs:integer, but Saxon (b8-6-1) disagrees:
   xs:integer(xs:byte(100)) instance of xs:byte ==> true ????

This implies that if the argument already conforms to the casted-to-type
then it it returned changed.  That is certainly a possible behavior,
but another behavior is that casting to xs:integer returns a value
with annotation xs:integer.  That seems more consistent to me.

The formal semantics just refers to chapter 17 of Functions and
Operators, which mainly specifies which conversions are valid.
The formal semantics should probably specify the resulting "formal
values" after a cast.

Either way, this should be tested in the test suite.  I didn't
find it (using a quick grep).
--
        --Per Bothner
per@...   http://per.bothner.com/

[Michael Rys]

I agree with your assessment that xs:integer(xs:byte(100)) should have a
type annotation of xs:integer. Mike apparently disagrees. You should
file a Mozilla request to add this to the test suite.

Best regards
Michael

> -----Original Message-----
> From: www-ql-request@... [mailto:www-ql-request@...] On
> Behalf Of Per Bothner
> Sent: Thursday, February 23, 2006 7:30 PM
> To: www-ql@...
> Subject: question about subtyping and type annotations
>
>
> I'm unclear on the semantic model for type annotations, and I can't
> find a clear answer in the specifications or in the test suite.
>
> I gather (and Saxon agrees) that:
>    100 instance of xs:byte ==> false
> because 100 has "type annotation" xs:integer, which is not a sub-type
> of xs:byte.
>
> Using the cast xs:byte creates a value with type annotation xs:byte:
>    xs:byte(100) instance of xs:byte ==> true
>
> What about xs:integer(xs:byte(100))?  I would expect this to return
> a value with type annotation xs:integer, but Saxon (b8-6-1) disagrees:
>    xs:integer(xs:byte(100)) instance of xs:byte ==> true ????
>
> This implies that if the argument already conforms to the
> casted-to-type
> then it it returned changed.  That is certainly a possible behavior,
> but another behavior is that casting to xs:integer returns a value
> with annotation xs:integer.  That seems more consistent to me.
>
> The formal semantics just refers to chapter 17 of Functions and
> Operators, which mainly specifies which conversions are valid.
> The formal semantics should probably specify the resulting "formal
> values" after a cast.
>
> Either way, this should be tested in the test suite.  I didn't
> find it (using a quick grep).
> --
> --Per Bothner
> per@...   http://per.bothner.com/
>
>

[Michael Kay-3]

>
> What about xs:integer(xs:byte(100))?  I would expect this to return
> a value with type annotation xs:integer, but Saxon (b8-6-1) disagrees:
>    xs:integer(xs:byte(100)) instance of xs:byte ==> true ????
>
> This implies that if the argument already conforms to the
> casted-to-type
> then it it returned changed.  That is certainly a possible behavior,
> but another behavior is that casting to xs:integer returns a value
> with annotation xs:integer.  That seems more consistent to me.

There's some dispute about whether the Saxon behaviour here is acceptable.
The specification says that xs:integer(xs:byte(100)) returns an xs:integer.
My reading of the spec is that any expression that is defined to return an
xs:integer is also allowed to return a subtype of xs:integer: for example it
would be valid here for Saxon to return a value of type
saxon:seven-bit-integer, provided that the resulting value can be used
anywhere that an xs:integer can be used, and that (EXPR instance of
xs:integer) returns true. Logically this means that it is also acceptable to
return an xs:byte. This is one reason that we don't have a function that
tells you the actual type annotation on a value, the only thing you can do
is test whether a value is an instance of some candidate type.

Others have disagreed with this reading of the spec; in particular I have
heard it suggested that although the principle above applies to most kinds
of XQuery expression, cast and constructor expressions are an exception. But
I have also heard it suggested that it would be wrong say for the position()
function to return a value that is an xs:int as well as being an xs:integer.
I can't agree with that interpretation.

Michael Kay
http://www.saxonica.com/

[Michael Kay-3]

Given Michael Rys' intervention, I think the debate hinges on which of the
following statements takes precedence.

3.1.5: the value returned by a function retains its most specific type,
which may be derived from the declared return type of the function. For
example, a function that has a declared return type of xs:decimal may in
fact return a value of dynamic type xs:integer.

(Or more generally 2.2.3.2: The dynamic type of a value may be more specific
than the static type of the expression that computed it.)

3.12.3: cast is supported if the input type is a non-primitive atomic type
that is derived by restriction from the target type. In this case, the input
value is mapped into the value space of the target type, unchanged except
for its type. For example, if shoesize is derived by restriction from
xs:integer, a value of type shoesize can be cast into the schema type
xs:integer.

My reading is that 3.12.3 requires that the result is an instance of
xs:integer, but 3.1.5 allows that it might also be an instance of xs:byte.
The phrase "unchanged except for its type" does not disallow returning the
type unchanged.

The reason Saxon behaves this way is that the compiler often generates
unnecessary casts and then optimizes them away in a subsequent phase of
analysis. If I weren't allowed to optimize the cast away, I would have to
distinguish an cast created by the compiler from one that was written by the
user.

Michael Kay
http://www.saxonica.com/

[Jerome Simeon]

I agree with Michael Rys's reading.

I don't think that constructor functions should be considered as standard
function calls.

Section 3.12.5 Constructor Functions seems to be pretty clear about it:

[Definition: The constructor function for a given type is used to convert
instances of other atomic types into the given type. The semantics of the
constructor function T($arg) are defined to be equivalent to the
expression ($arg cast as T?).]

- Jerome

www-ql-request@... wrote on 02/24/2006 05:23:54 AM:

>
>
> Given Michael Rys' intervention, I think the debate hinges on which of
the
> following statements takes precedence.
>
> 3.1.5: the value returned by a function retains its most specific type,
> which may be derived from the declared return type of the function. For
> example, a function that has a declared return type of xs:decimal may in
> fact return a value of dynamic type xs:integer.
>
> (Or more generally 2.2.3.2: The dynamic type of a value may be more
specific
> than the static type of the expression that computed it.)
>
> 3.12.3: cast is supported if the input type is a non-primitive atomic
type
> that is derived by restriction from the target type. In this case, the
input
> value is mapped into the value space of the target type, unchanged
except
> for its type. For example, if shoesize is derived by restriction from
> xs:integer, a value of type shoesize can be cast into the schema type
> xs:integer.
>
> My reading is that 3.12.3 requires that the result is an instance of
> xs:integer, but 3.1.5 allows that it might also be an instance of
xs:byte.
> The phrase "unchanged except for its type" does not disallow returning
the
> type unchanged.
>
> The reason Saxon behaves this way is that the compiler often generates
> unnecessary casts and then optimizes them away in a subsequent phase of
> analysis. If I weren't allowed to optimize the cast away, I would have
to
> distinguish an cast created by the compiler from one that was written by
the
> user.
>
> Michael Kay
> http://www.saxonica.com/
>
>
>

[Michael Kay-3]

> 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?

Michael Kay
http://www.saxonica.com/

On Friday 24 February 2006 16:57, you 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?

Another question is what the negative impact, if any, is when returning say
xs:byte when xs:integer is the static type(apart from Per Bothner's confusion
when investigating these corner cases).


                Frans

[Michael Kay-3]

> Another question is what the negative impact, if any, is when
> returning say
> xs:byte when xs:integer is the static type(apart from Per
> Bothner's confusion
> when investigating these corner cases).

The only negative impact I can see is that some type errors won't be
detected, for example if the value is passed to a function that requires an
xs:byte. But that's true for any expression that returns a subtype of the
declared type, or for example if the result of 1+1 is delivered as an
xs:short - which to my mind is clearly allowed.

Michael Kay
http://www.saxonica.com/

[Vladimir Gapeyev]

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

[Michael Rys]

The main negative impact will be that type inspection will result in
different results in typeswitch and instance of statements.

That is obviously not conductive to interoperable semantics.

Best regards
Michael

> -----Original Message-----
> From: www-ql-request@... [mailto:www-ql-request@...] On Behalf
Of

> Frans Englich
> Sent: Friday, February 24, 2006 10:16 AM
> To: www-ql@...
> Subject: Re: question about subtyping and type annotations
>
>
> On Friday 24 February 2006 16:57, you 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?
>
> Another question is what the negative impact, if any, is when
returning
> say
> xs:byte when xs:integer is the static type(apart from Per Bothner's
> confusion
> when investigating these corner cases).
>
>
> Frans

[Jerome Simeon]

Right. and I think that from the paragraph about casting that you quoted
it is clear
that you get the type annotation of the type into which you are casting.

It seems the most natural semantics in a number of ways. Notably it is
useful is the
user wants to explicitely set the type annotation, as in:

xs:byte(1)

or in case of casting from another type:

xs:integer("1")

I think people will find it confusing if you change the type annotation
behind their
back.

I also remember that one feature that was discussed at some point for
XQuery was
something like Expr instance of only xs:integer, where you want to check
for the type
annotation but not one of its derived types. That kind of feature won't
really make sense
if we let implementation pick up a derived type arbitrarily.

The rules about type substitutability is not about giving implementations
the freedom
to chose the type annotation. I think the language is pretty deterministic
in that sense.
When you validate or cast you get a specific type annotation. When you
pass the
value to the function you preserve the existing type annotation. That
should helps
interoperability.

- Jerome



"Michael Kay" <mhk@...> wrote on 02/24/2006 11:57:55 AM:

> > 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?
>
> Michael Kay
> http://www.saxonica.com/
>
>

[Jerome Simeon]

Definitely agreeing with Vladimir. I'm not sure a rewording is absolutely
necessary though,
but if we want to be more explicit, adding something about the type
annotation
might help?

- Jerome


www-ql-request@... wrote on 02/24/2006 02:41:38 PM:

>
>
>
> 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
>