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 BelgiumReceived on Thursday, 20 November 2003 11:45:57 UTC
This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 22:43:43 UTC