Changeset 00ad2a0

Timestamp:

May 20, 2025, 12:22:33 AM (4 months ago)

Author:

Fangren Yu <f37yu@…>

Branches:

master

Children:

4791307

Parents:

206f4cf

Message:

add a paragraph to explain an optimization for resolving unbound
assertions

File:

• doc/theses/fangren_yu_MMath/resolution.tex (modified) (3 diffs)

doc/theses/fangren_yu_MMath/resolution.tex

@@ -504 +504 @@
 where one can be uniquely resolved and allow the type @T@ to be inferred immediately, and another has many ways to be resolved, each resulting in @T@ being bound to a different concrete type.
 If the first assertion is examined by the algorithm, the inferred type can then be utilized in resolving the second assertion eliminating many incorrect options without producing a list of candidates requiring further checks.
-In practice, this have a significant impact when an unbound type @T@ is declared to satisfy the basic \emph{object assertions}\footnote{The term is borrowed from object-oriented languages although \CFA is not object-oriented.} of having a default constructor, destructor, and copy assignment operations.
-Since these functions are implicitly defined for almost every type in scope, there can be hundreds or even thousands of matches to these functions with an unspecified operand type.
-In most cases, the value of @T@ can be inferred by resolving other assertions first, and then the object lifetime-functions can easily be fulfilled since functions are sorted internally by the operand type;
-because of its size, this optimization greatly reduces the number of wasted resolution attempts.
-
-This issue also limits the capability of the assertion resolution algorithm.
+In practice, this have a significant impact when an unbound type @T@ is declared to satisfy the basic \emph{object assertions}\footnote{The term is borrowed from object-oriented languages although \CFA is not object-oriented.} of having a default constructor, destructor, and copy assignment operations. Since these functions are implicitly defined for almost every type in scope, there can be hundreds or even thousands of matches to these functions with an unspecified operand type.
+
+Based on this observation, I implemented an optimization to the assertion resolution algorithm that will only attempt to resolve object assertions after all other assertions are resolved successfully, and further delay resolving object assertions with an unbound first argument type, \ie the type of the argument being constructed or destructed, until no progress can be made otherwise. 
+This simple optimization on assertion resolution order eliminates over 80 percent of unbound object lifetime function lookups. 
+In most cases, the operand type can be inferred by resolving other assertions first, and then the object lifetime functions can be looked up efficiently, since these functions are indexed by the operand type in the identifier table of the compiler.
+Although the unbound parameter case appears infrequently in practice, it is potentially very costly due to thousands of wasted type unification runs each time it occurs. As a result, this optimization is able to produce an overall compilation speedup of around 10 percent.
+
+The issue of having unbound parameters also limits the capability of the assertion resolution algorithm.
 Assertion matching is implemented to be more restrictive than expression resolution in general, in that the parameter types must match exactly, rather than just merely callable.
 If a function declaration includes the assertion @void f(T)@ and only a @f(long)@ is in scope, trying to resolve the assertion with @T == int@ does not work.
@@ -520 +522 @@
 Currently, type resolution cannot do enough return-type inferencing while performing eager assertion resolution: the return type information is unknown before the parent expression is resolved, unless the expression is an initialization context where the variable type is known.
 By delaying the assertion resolution until the return type becomes known, this problem can be circumvented.
-The truly problematic case occurs if a type variable does not appear in either of the parameter or return types and only appears in assertions or variables (\newterm{associate types}).
+The truly problematic case occurs if a type variable does not appear in either of the parameter or return types and only appears in assertions or variables (\newterm{associated types}).
 \begin{cfa}
 forall( T | { void foo( @T@ ) } ) int f( float ) {
@@ -526 +528 @@
 }
 \end{cfa}
-This case is rare so forcing every type variable to appear at least once in parameter or return types does not limit the expressiveness of \CFA type system to a significant extent.
-\VRef{s:AssociatedTypes} presents a proposal for including type declarations in traits rather than having all type variables appear in the trait parameter list, which provides equivalent functionality to an unbound type parameter in assertion variables, and also addresses some of the variable cost issue discussed in \VRef{s:ExpressionCostModel}.
+This case is rare, so forcing every type variable to appear at least once in parameter or return types does not limit the expressiveness of \CFA type system to a significant extent.
+\VRef{s:AssociatedTypes} presents a proposal for including type declarations in traits rather than having all type variables appear in the trait parameter list, which provides equivalent functionality to an unbound type parameter in assertion variables, serves as a guidance to the resolution algorithm that works in more general cases than the specific optimization for object assertions mentioned above, and also addresses some of the variable cost issue discussed in \VRef{s:ExpressionCostModel}.