static typing of XQuery?

[David Carlisle]

> I'll await practical experience before deciding that pessimistic static
> typing is ever beneficial.
> 
> Michael Kay

Even if there are use cases where it is useful, I think that as
currently defined it has an overwhelmingly negative impact on XQuery
portability. As we are currently seeing in a flood of bug reports to the
XQuery test suite, queries developed on systems not using (FS defined)
static typing as will almost always fail on systems that do use the
static typing feature. It is already having a negative impact on declared
types of core functions, with the declared types being weakened to avoid
static type errors on natural looking expressions. It will have a
similar negative impact on any user-defined function libraries as the
only advice that you can give to people to assure that functions work on
the static typing systems is to declare everything with as weak a type
as possible.

Static typing is an "At risk" feature, so I do hope that it is seriously
considered that it be dropped from 1.0 and perhaps re-added for a later
release in a form that is less intrusive.

In a system like Standard ML that has highly effective "pessimistic"
static typing system, the types are almost always automatically inferred
by the type inference mechanism, and if that type inferencing fails, it
is almost always the case (in my experience) that it is a user error
that has been caught early.

With the static types as currently defined, there is no way that any
static inference system can ever do that for XQuery as the cardinality
constraints are not computationally feasible. 
It's possible to write the following in XQuery,

foo[Fermat's last theorem is false]

which has a static type of an empty sequence, but since it took 350
years or so to prove that, it's not really reasonable to expect that
the type system check this in real time.

One possible way forward would be for the "pessimistic" type
inferencing to treat _all_ types as if they had a cardinality
indicator of *, this would match other functional language type
systems where you can declare something as "list of integer"
but not "list of integer with at least one item". If this was done it
would mean that authors could still use the tighter cardinality
constraints which would benefit "optimistic" static checking and dynamic
type checking, while still giving hope of portability with systems using
the FS-defined pessimistic type checking.

David