This is an archived snapshot of W3C's public bugzilla bug tracker, decommissioned in April 2019. Please see the home page for more details.
2.3.1 Formal values [7 (Formal)] Value ::= Item | (Value "," Value) | ("(" ")") Presumably, the Value () represents the empty sequence. (I don't think the FS actually says so; maybe it should.) The odd thing is that this production allows Values with () *within* them. E.g., Value derives 1 of type xs:integer, (), (), "a" of type xs:string Since an item (in a sequence) can't be the empty sequence, what is the point of such a Value? (Please note that I'm talking about Values, not Exprs.) At first, I thought it was just a mistake in the production, so I was going to suggest an (editorial) change to: Value ::= "(" ")" | Item ("," Item)* But then I noticed the example in 8.2.3.2, which actually shows a Value with embedded ()'s. The following Note ("while preserving the structure of the sequence") appears to indicate that the embedded ()'s are essential to the workings of the 'test' judgment (though as far as I can tell, they aren't). Moreover, the inference rule 4.3.1 / DEv / rule 1 appears happy to construct such values. E.g., I can use it to conclude that dynEnv |- 1, () => 1 of type xs:integer, () I would have expected the resulting Value to be just 1 of type xs:integer So maybe it's more than an editorial matter. (On a related note, the corresponding STA rule allows me to conclude: statEnv |- 1, () : xs:integer, empty but presumably the Type should be just xs:integer.)
Michael, The ability to use the empty sequence (resp. the empty type) for values (resp. types). Is intentional. For values, the values follows the same rules as the corresponding sequence constructors in XQuery. so (),((),1,()),2 = 1,2. I believe there used to be a sentence about that in the formal values section. For types, there are many expressions which generate sequences or unions of empty types. (e.g., if Expr then () else 1). Fortunately all those types are equivalent ((), xs:integer = xs:integer ; () | xs:integer = xs:integer?, etc.). That is covered by the subtyping/equivalence rules in 8.3.2 Subtyping (<:). So I believe this may be editorial, although I'm not sure what you think would help clarify. I would recommend at least to add the sentence about values (explaining the first part above) Best, - Jerome
I think you misunderstood me somewhat. Please note that I'm talking about "Values" (i.e., syntactic objects that can be derived from the symbol 'Value') as distinct from "values" (i.e., members of an abstract value space). (Similarly for Type vs type.) I agree with what you say about values & the empty sequence, or types & the empty type, but what concerns me is that the formal machinery that operates on Values and Types doesn't reflect what we know to be true of values and types. To repeat, the inference rules allow me to conclude: dynEnv |- 1, () => 1 of type xs:integer, () but I can find no way to conclude: dynEnv |- 1, () => 1 of type xs:integer Similarly, I can conclude: statEnv |- 1, () : xs:integer, empty but not: statEnv |- 1, () : xs:integer In each case, I think the latter conclusion is necessary to satisfy premises elsewhere, but it's unreachable. Perhaps we need rules such as dynEnv |- Expr => Value, () ----------------------------- dynEnv |- Expr => Value and statEnv |- Expr : Type, empty ------------------------------ statEnv |- Expr : Type
Michael, Some more thoughts on that thread. Notably a few things: * I can't think of a place where we get in trouble with this at this point. The type infered can be xs:integer,() or many other more complex types. * There are may syntactic variations for the same type (T | () or T?, T* or T+|() or T?+, T*,T or T,T* etc.). To the best of my knowledge there is no finite set of rules to define those equivalances. * It seems that those rules would merely reinvent the notion of equivalence that is already in section 8.3.2. - Jerome
(In reply to comment #3) [in a slightly different order] > > * It seems that those rules would merely reinvent the notion of equivalence > that is already in section 8.3.2. Do the rules of 8.1.4 "reinvent" the notion of type lookup, or those of section 8.5.1 "reinvent" the notion of type promotion? Not really, they just *formalize* those notions. Similarly for rules that would formalize the notion of type equivalence. > * There are may syntactic variations for the same type (T | () or T?, T* or > T+|() or T?+, T*,T or T,T* etc.). To the best of my knowledge there is no > finite set of rules to define those equivalances. According to 8.3.1, "the structural component of the [XPath/XQuery] type system can be modeled by regular expressions", so equivalence of two Types presumably reduces to equivalence of two regular expressions, for which algorithms exist. So I imagine you could express it with a finite set of rules, though you probably wouldn't want to. > * I can't think of a place where we get in trouble with this at this point. > The type infered can be xs:integer,() or many other more complex types. This is the main point, I think; if the inability to conclude dynEnv |- 1, () => 1 of type xs:integer or statEnv |- 1, () : xs:integer doesn't actually cause problems in the inference process, then the other points are irrelevant. I *thought* I had examples of problems, but now they're deserting me, hiding behind unformalized things like subtyping and built-in functions. However, it doesn't seem like the FS was written in such a way as to *guarantee* the absence of such problems, so they might still be out there. I'll let you know if I find one.
... > > * It seems that those rules would merely reinvent the notion of equivalence > > that is already in section 8.3.2. > > Do the rules of 8.1.4 "reinvent" the notion of type lookup, or thoseof section > 8.5.1 "reinvent" the notion of type promotion? Not really, they just > *formalize* those notions. Similarly for rules that would formalize the notion > of type equivalence. > sorry I wasn't clear. the purpose of 8.5.1 is to be a replacement for such rules (which as far as I know can't be written using the inference rules notations -- see below). > > * There are may syntactic variations for the same type (T | () or T?, T* or > > T+|() or T?+, T*,T or T,T* etc.). To the best of my knowledge there is no > > finite set of rules to define those equivalances. > > According to 8.3.1, "the structural component of the [XPath/XQuery] > type system > can be modeled by regular expressions", so equivalence of two Types presumably > reduces to equivalence of two regular expressions, for which algorithms exist. Right and the typical algorithms for regular expression operations usually go through automatas which is what 8.5.1 is about. > So I imagine you could express it with a finite set of rules, though you > probably wouldn't want to. > Actually I believe I recall there is a theoretical result showing there isn't a finite set of rules. The reference eludes me though. If I recall you can build a family of regexps of depth n for which you would need a number of rules depending on n. something along those lines. In addition, it seemed that this kind of treatment would take a lot of space and be mostly reproducing state of the art material from the literature on regexp/FSAs and I believe the WGs decided not to go there. > > * I can't think of a place where we get in trouble with this at this point. > > The type infered can be xs:integer,() or many other more complex types. > > This is the main point, I think; if the inability to conclude > dynEnv |- 1, () => 1 of type xs:integer > or > statEnv |- 1, () : xs:integer > doesn't actually cause problems in the inference process, then the > other points > are irrelevant. > > I *thought* I had examples of problems, but now they're deserting me, hiding > behind unformalized things like subtyping and built-in functions. However, it > doesn't seem like the FS was written in such a way as to *guarantee* the > absence of such problems, so they might still be out there. I'll let you know > if I find one. I believe that the FS was designed in such a way that locations where you would get into such problems are checked through subtyping. Based this your last commentis it ok with you if we close that bug now without action? Thanks, - Jerome
Michael, Since there does not seem to be any specific issue or fix suggested at this point, so the working groups have decided to close that issue with no action. Best, - Jerome