RE: Interaction of type annotations with literals in the formal semantics

Your interpretation is correct. And while it seems somewhat inconvenient
for the user, type safety and strong typing requires the assignment to
be written as 

let $x as feet := feet(15) return $x

Best regards
Michael

> -----Original Message-----
> From: www-ql-request@w3.org [mailto:www-ql-request@w3.org] On Behalf
Of
> Stijn Vansummeren
> Sent: Thursday, November 20, 2003 8:43 AM
> To: www-ql@w3.org
> Subject: Interaction of type annotations with literals in the formal
> semantics
> 
> 
> I have a question concerning the typing of literals and its
interaction
> with
> type annotations (for instance in let expressions) in the formal
> semantics.
> 
> The static rule for integer literals is
> 
>   --------------------------------------------------
>   statenv |- integerLiteral : xs:integer
> 
> Now suppose we have the following type definition:
> 
>   define type feet restricts xs:integer
> 
> Is the following expression well-typed?
> 
>   let $x as feet := 15 return $x
> 
> I believe it is not, since the literal 15 is given the type xs:integer
by
> the
> literal typing rule above. The typing rule for let specifies that
> "xs:integer" should be a subtype of "feet".  By definition,
"xs:integer"
> is a
> subtype of type "feet" iff every value that matches "xs:integer" also
> matches
> "feet".  However, the value "15 of type xs:integer" will not match
type
> "feet", since there is only one matching rule for atomic values:
> 
>   statEnv |- AtomicTypeName1 derives from AtomicTypeName2
>
------------------------------------------------------------------------
--
> ----------------------------
>   statEnv |- AtomicValue of type AtomicTypeName1 matches
AtomicTypeName2
> 
> In our case, the value "xs:integer" is not derived from "feet".
Obviously,
> the
> value is matched by type "xs:integer". Hence, "xs:integer" is not a
> subtype
> of "feet", and the expression above is ill-typed.
> 
> Is my reasoning correct? If so, does this signal an error in the
static
> semantics or is there something inherently "wrong" with the expression
> above
> (justifying the ill-typedness)?
> 
> --Stijn Vansummeren
> 
> Limburgs Universitair Centrum
> Universitaire Campus
> Gebouw D
> 3590 Diepenbeek
> Belgium
> 
>

Received on Thursday, 20 November 2003 12:55:54 UTC