Changeset 8fe7a85 for doc/theses/fangren_yu_MMath/resolution.tex

Timestamp:

May 12, 2025, 8:33:55 PM (5 months ago)

Author:

Fangren Yu <f37yu@…>

Branches:

master

Children:

edd11bd

Parents:

98c77b2

Message:

proofreading changes from Gregor

File:

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

doc/theses/fangren_yu_MMath/resolution.tex

@@ -2 +2 @@
 \label{c:content2}
 
-Recapping, the \CFA's type-system provides expressive polymorphism: variables can be overloaded, functions can be overloaded by argument and return types, tuple types, generic (polymorphic) functions and types (aggregates) can have multiple type parameters with assertion restrictions;
+Recapping, \CFA's type-system provides expressive polymorphism: variables can be overloaded, functions can be overloaded by argument and return types, tuple types, generic (polymorphic) functions and types (aggregates) can have multiple type parameters with assertion restrictions;
 in addition, C's multiple implicit type-conversions must be respected.
 This generality leads to internal complexity and correspondingly higher compilation cost directly related to type resolution.
@@ -24 +24 @@
 \end{enumerate}
 \VRef[Table]{t:SelectedFileByCompilerBuild} shows improvements for selected tests with accumulated reductions in compile time across each of the 5 fixes.
-To this day, the large reduction in compilation time significantly improves the development of the \CFA's runtime because of its frequent compilation cycles.
+The large reduction in compilation time significantly improves the development of the \CFA's runtime because of its frequent compilation cycles.
 
 \begin{table}[htb]
@@ -86 +86 @@
 
 \item \textbf{Safe} cost representing a widening conversion \eg @short@ to @int@, qualifier-adding conversions for pointer and reference types, and value conversion for enumeration constants.
-Even when conversions are safe, the fewest conversions it ranked better, \eg @short@ to @int@ versus @short@ to @long int@.
+When all conversions are safe, closer conversions are ranked better, \eg @short@ to @int@ versus @short@ to @long int@.
 \begin{cfa}
 void f( long int p ); $\C[2.5in]{// 1}$
@@ -110 +110 @@
 \end{cfa}
 \end{enumerate}
-Cost tuples are compared by lexicographical order, from unsafe (highest) to specialization (lowest), with ties moving to the next lowest item.
+Cost tuples are compared in lexicographical order, from unsafe (highest) to specialization (lowest), with ties moving to the next lowest item.
 At a subexpression level, the lowest cost candidate for each result type is included as a possible interpretation of the expression;
 at the top level, all possible interpretations of different types are considered (generating a total ordering) and the overall lowest cost is selected as the final interpretation of the expression.
 Glen Ditchfield first proposed this costing model~\cite[\S~4.4.5]{Ditchfield92} to generate a resolution behaviour that is reasonable to C programmers based on existing conversions in the C programming language.
 This model carried over into the first implementation of the \CFA type-system by Richard Bilson~\cite[\S~2.2]{Bilson03}, and was extended but not redesigned by Aaron Moss~\cite[chap.~4]{Moss19}.
-Moss's work began to show problems with the underlying costing model;
+Moss's work began to show problems with the underlying cost model;
 these design issues are part of this work.
 
@@ -171 +171 @@
 Other than the case of multiple exact matches, where all have cost zero, incomparable candidates under a partial ordering can often have different expression costs since different kinds of implicit conversions are involved, resulting in seemingly arbitrary overload selections.
 
-There are currently at least three different situations where the polymorphic cost element of the cost model does not yield a candidate selection that is clearly justifiable, and one of them is straight up wrong.
+There are currently at least three different situations where the polymorphic cost element of the cost model does not yield a candidate selection that is justifiable, and one of them is clearly wrong.
 \begin{enumerate}[leftmargin=*]
 \item Polymorphic exact match versus non-polymorphic inexact match.
@@ -193 +193 @@
 \end{itemize}
 In this example, option 1 produces the prototype @void f( int )@, which gives an exact match and therefore takes priority.
-The \CC resolution rules effectively make option 2 a specialization that only applies to type @long@ exactly,\footnote{\CC does have explicit template specializations, however they do not participate directly in overload resolution and can sometimes lead to unintuitive results.} while the current \CFA rules make option 2 apply for all integral types below @long@.
+The \CC resolution rules effectively make option 2 a specialization that only applies to type @long@ exactly,\footnote{\CC does have explicit template specializations, however they do not participate directly in overload resolution and can sometimes lead to unintuitive results.} while the current \CFA rules make option 2 apply for all integral types ranked lower than @long@ as well.
 This difference could be explained as compensating for \CFA polymorphic functions being separately compiled versus template inlining;
 hence, calling them requires passing type information and assertions increasing the runtime cost.
@@ -227 +227 @@
 Passing a @pair@ variable to @f@
 \begin{cfa}
-pair p;
+pair(int, double) p;
 f( p );
 \end{cfa}
 gives a cost of 1 poly, 2 variable for the @pair@ overload, versus a cost of 1 poly, 1 variable for the unconstrained overload.
 Programmer expectation is to select option 1 because of the exact match, but the cost model selects 2;
-while either could work, the type system should select a call that meets expectation of say the call is ambiguous, forcing the programmer to mediate.
+it is not possible to write a specialization for @f@ that works on any pair type and gets selected by the type resolver as intended.
 As a result, simply counting the number of polymorphic type variables is no longer correct to order the function candidates as being more constrained.
 \end{enumerate}
 
-These inconsistencies are not easily solvable in the current cost-model, meaning the current \CFA codebase has to workaround these defects.
+These inconsistencies are not easily solvable in the current cost-model, meaning that currently the \CFA codebase has to workaround these defects.
 One potential solution is to mix the conversion cost and \CC-like partial ordering of specializations.
 For example, observe that the first three elements (unsafe, polymorphic and safe conversions) in the \CFA cost-tuple are related to the argument/parameter types, while the other two elements (polymorphic variable and assertion counts) are properties of the function declaration.
@@ -469 +469 @@
 
 
-In previous versions of \CFA, this number was set at 4; as the compiler becomes more optimized and capable of handling more complex expressions in a reasonable amount of time, I have increased the limit to 8 and it does not lead to problems.
+In previous versions of \CFA, this number was set at 4; as the compiler has become more optimized and capable of handling more complex expressions in a reasonable amount of time, I have increased the limit to 8 and it has not led to problems.
 Only rarely is there a case where the infinite recursion produces an exponentially growing assertion set, causing minutes of time wasted before the limit is reached.
 Fortunately, it is very hard to generate this situation with realistic \CFA code, and the ones that have occurred have clear characteristics, which can be prevented by alternative approaches.
@@ -481 +481 @@
 In many cases, these problems can be avoided by examining other assertions that provide insight on the desired type binding: if one assertion parameter can only be matched by a unique option, the type bindings can be updated confidently without the need for backtracking.
 
-The Moss algorithm currently used in \CFA was developed using a simplified type system that captures most of \CFA type system features.
+The Moss algorithm currently used in \CFA was developed using a simplified type system that captures most of \CFA's type system features.
 The simulation results were then ported back to the actual language.
 The simulator used a mix of breadth- and depth-first search in a staged approach.
@@ -520 +520 @@
 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 (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{associate types}).
 \begin{cfa}
 forall( T | { void foo( @T@ ) } ) int f( float ) {
@@ -527 +527 @@
 \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.
-The next section presents a proposal for including type declarations in traits rather than having all type variables appear in the trait parameter list, which is 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}.
+\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}.
 
 
@@ -599 +599 @@
 \end{enumerate}
 
-\CFA does attempt to incorporate upstream type information propagated from variable a declaration with initializer, since the type of the variable being initialized is known.
+\CFA does attempt to incorporate upstream type information propagated from a variable declaration with initializer, since the type of the variable being initialized is known.
 However, the current type-environment representation is flawed in handling such type inferencing, when the return type in the initializer is polymorphic.
 Currently, an inefficient workaround is performed to create the necessary effect.