W3C home > Mailing lists > Public > www-ql@w3.org > October to December 2003

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

From: Michael Rys <mrys@microsoft.com>
Date: Thu, 20 Nov 2003 09:55:56 -0800
Message-ID: <EB0A327048144442AFB15FCE18DC96C70159447A@RED-MSG-31.redmond.corp.microsoft.com>
To: <stijn.vansummeren@luc.ac.be>, <www-ql@w3.org>

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

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 20:17:16 UTC