[Bug 1605] The inference engine is not specified (only the rule base it uses is)

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


simeon@us.ibm.com changed:

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




------- Additional Comments From simeon@us.ibm.com  2005-07-20 19:08 -------
This is a very good comment. This would probably help the reader a lot to have
such a description. This is mostly of editorial nature, but would make the whole
specification much more approachable. Let me try and sketch a description for
the 'inferrence engine' as you call it.

1. What does an inferrence rule mean. (See comment also on bug [1612]).

statEnv |- Expr1 : Type1
statEnv |- Expr2 : Type2
------------------------
statEnv |- Expr1, Expr2 : Type 1, Type2

logically means:

IF
  statEnv |- Expr1 : Type1
AND
  statEnv |- Expr2 : Type2
THEN
  statEnv |- Expr1, Expr2 : Type 1, Type2

The important point is the use of conjunctions between the preconditions.

2. What if you have several inferrence rules?

a set of rules is essentially a disjunction:

dynEnv |- Expr1 => false
--------------------------------------
dynEnv |- Expr1 and Expr2 => false

dynEnv |- Expr2 => false
--------------------------------------
dynEnv |- Expr1 and Expr2 => false

logically means:

IF
  dynEnv |- Expr1 => false
THEN
  dynEnv |- Expr1 and Expr2 => false

OR

IF
  dynEnv |- Expr2 => false
THEN
  dynEnv |- Expr1 and Expr2 => false

3. How does the inferrence engine works

You take the disjunction of all the rules and your try and 'prove'
that a judgment is true or not.

For static typing, typically, you are trying to prove:

statEnv |- Expr : Type

For the given expression, the inferrence rules will tell you if
this is true or not. This is true if you can logically infer that the
judgment holds, and results in a given type. If you cannot draw an inferrence,
then the judgement does not hold and static typing fails.

for example, take the following XQuery expression:

fn:count((1,2,3))

you are trying show that statEnv |- fn:count((1,2,3)) : Type holds

you can draw the inference as follows:

  statEnv |- 1 : xs:integer  (from typing of literals)
  statEnv |- 2 : xs:integer  (from typing of literals)
  ---------------------------------------- (from typing of sequence constr.)
    statEnv |- 1,2 : xs:integer, xs:integer
    statEnv |- 3 : xs:integer
    -----------------------------------------------------(sequence constr.)
    statEnv |- 1,2,3 : xs:integer, xs:integer, xs:integer

    declare function fn:count($x as item()*) as xs:integer
    statEnv |- xs:integer,xs:integer,xs:integer <: item*
    ----------------------------------------------------------(function call)
    statEnv |- fn:count((1,2,3)) : xs:integer

So the static typing succeeds and results in the static type of xs:integer

Here is another example:

   fn:nilled((1,2,3))

Here again, the inferrence can proceed up to:
    ....
    -----------------------------------------------------(sequence constr.)
    statEnv |- 1,2,3 : xs:integer, xs:integer, xs:integer

But there is no rule that can infer the type of fn:nilled((1,2,3)), notably
because the static typing rules for function calls will only hold if
xs:integer,xs:integer,xs:integer <: node?
which is false.

Would something along those lines help?

= Jerome

Received on Wednesday, 20 July 2005 19:08:27 UTC