[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-25 20:51 -------
regarding additional comment 4, you are right, my use of <: was a mistake;
the correct symbol is : in judgments such as Expr : Type.

regarding additional comment 5, I can accept a prose description of choosing
the best type, especially if there is a judgment of the form
"Type is the best formal type for Expr".

As to the definition of "best", is it possible to define it as 
follows:  "The best formal type for a [query/expression] Expr is that 
Type1 such that, for all formal types Type2, if 'statEnv |- Expr : Type2'
is inferrable, then 'statEnv |- Type1 <: Type2' is inferrable"?
This would define the best formal type as the minimal formal type.  
However, I don't know the Formal Semantics well enough to know if there
always is a minimum formal type for an expression.

Once you have a definition of the best type, then the best quantifier
is presumably the OccurrenceIndicator of the best type.

Received on Monday, 25 July 2005 20:51:42 UTC