[Bug 1721] [FS] need a judgment to find the "best" type and quantifier

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





------- Additional Comments From fred.zemke@oracle.com  2005-07-21 21:10 -------
I think this may be one of the places in the spec that logically depend
on the execution model of the inference engine.  See my proposed description
of the inference engine in comment #1605 as an additional remark.
If the inference engine is conceptually "firing" an inference whenever it
detects that the premises of the inference are fulfilled, in a 
non-deterministic order, then you know when you have deduced that 
"|- Expr : Type" for some specific Expr and Type, but you never know whether 
you have found the "best" Type.  In addition, you cannot have a judgment of 
the form "statEnv |- (for all Type1)[ if Expr : Type2 then Type1 <: Type2 ]"
which is conceptually what is needed for the informal judgment,
"statEnv |- Type1 is the best formal type for Expr".
The reason is that the inference engine is not powerful enough to 
prove theorems about "for all" statements, it is only powerful enough
to deduce single concrete judgments.

You are right, we don't want to start over, so perhaps an English-language
definition of a judgment "statEnv |- Type1 is the best type for Expr"
is needed.  But supplying a hand-wavy definition looks like a big
conceptual hole that I would rather see filled.

A bottom-up implementation would start at the leaves of the
parse tree and recursively decide the best static type for each node of the
tree.  It is possible to model bottom-up implementations using an
inference engine as described in my comment #1605.  The thing is, don't
bother to define "statEnv |- Expr : Type" via inferences.  Instead, define 
"statEnv |- Type is the best formal type for Expr" for each kind of 
expression.

Received on Thursday, 21 July 2005 21:10:10 UTC