[Bug 3273] [FS] technical: 2.3.1 Formal values: () in Values


------- Comment #4 from jmdyck@ibiblio.org  2006-06-12 23:23 -------
(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
    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.

Received on Monday, 12 June 2006 23:23:22 UTC