[Bug 1616] only the semantics of sequence types are specified, not all formal types

http://www.w3.org/Bugs/Public/show_bug.cgi?id=1616


simeon@us.ibm.com changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|NEW                         |ASSIGNED




------- Additional Comments From simeon@us.ibm.com  2005-07-21 00:06 -------
The comment is touching on a pretty important aspect of what the formal
semantics is doing.

There is in fact several ways to define what you would more formally call a
'meaning' for the type. One way is to extend the notion of 'a value matching a
type' to work on all types, not only sequence types. That used to be part of the
spec (and of a separate paper by Phil Wadler and my self at POPL), but was
removed since it is not actually used anywhere to define XQuery.

Another way to define the semantics of types is to define a 'validation'
judgment which tells which values can be validated against which types (and
yield a new value). There is still some (incomplete) specification of this in
Appendix E. But again, this is non-normative since the validation semantics is
fully specified in XML Schema.

What remains are two main judgments in the formal semantics:

dynEnv |- Value matches SequenceType

and 

statEnv |- Expr : Type

The last judgment is the one that is important for the purpose of this
specification. However, if you wanted to prove something like a soundness
theorem for the type system, you would have to go through the whole exercise of
defining matching, etc.

The main issue here is that we are defining a standard, not trying to formally
prove properties of the system. So the work is restricted to defining only what
is necessary for static typing. I do not believe this is something that the
group will be willing to change at this point, but I hope it makes some sense.

Now more concretely about your question related to document types. There is in
fact a judgement which infers the type for a document node. This is located in
Section 4.7.3.3 Document Node Constructors. The static inference rule looks as
follows:

  statEnv |- Expr : Type
  statEnv |- Type <: (element | text | processing-instruction | comment)*
  ------------------------------------------------------------------------
  statEnv |- document { Expr } : document

It gives precisely the constraints related to what type is acceptable inside a
document node type. In the case of document { () } you will get the static type
of document { empty }.

Do you have specific changes in the document that you would think help?

- Jerome & Michael

Received on Thursday, 21 July 2005 00:06:54 UTC