Changeset 4791307

Timestamp:

May 20, 2025, 7:09:17 AM (3 weeks ago)

Author:

Peter A. Buhr <pabuhr@…>

Branches:

master

Children:

a7b78c3

Parents:

00ad2a0

Message:

remove unnecessary PAB markers, and proofread added text on code improvements

Location:

doc/theses/fangren_yu_MMath

Files:

• features.tex (modified) (5 diffs)
• future.tex (modified) (1 diff)
• resolution.tex (modified) (11 diffs)

doc/theses/fangren_yu_MMath/features.tex

@@ -123 +123 @@
 the call to @foo@ must pass @x@ by value, implying auto-dereference, while the call to @bar@ must pass @x@ by reference, implying no auto-dereference.
 
-\PAB{My analysis shows} without any restrictions, this ambiguity limits the behaviour of reference types in \CFA polymorphic functions, where a type @T@ can bind to a reference or non-reference type.
+My analysis shows without any restrictions, this ambiguity limits the behaviour of reference types in \CFA polymorphic functions, where a type @T@ can bind to a reference or non-reference type.
 This ambiguity prevents the type system treating reference types the same way as other types, even if type variables could be bound to reference types.
 The reason is that \CFA uses a common \emph{object trait}\label{p:objecttrait} (constructor, destructor and assignment operators) to handle passing dynamic concrete type arguments into polymorphic functions, and the reference types are handled differently in these contexts so they do not satisfy this common interface.
@@ -287 +287 @@
 \end{figure}
 
-\PAB{I identified} the primary issues for tuples in the \CFA type system are polymorphism and conversions.
+I identified the primary issues for tuples in the \CFA type system are polymorphism and conversions.
 Specifically, does it make sense to have a generic (polymorphic) tuple type, as is possible for a structure?
 \begin{cfa}
@@ -386 +386 @@
 Scala, like \CC, provides tuple types through a library using this structural expansion, \eg Scala provides tuple sizes 1 through 22 via hand-coded generic data-structures.
 
-However, after experience gained building the \CFA runtime system, \PAB{I convinced them} making tuple-types first-class seems to add little benefit.
+However, after experience gained building the \CFA runtime system, I convinced them making tuple-types first-class seems to add little benefit.
 The main reason is that tuples usages are largely unstructured,
 \begin{cfa}
@@ -574 +574 @@
 
 Currently in \CFA, variadic polymorphic functions are the only place tuple types are used.
-\PAB{My analysis showed} many wrapper functions are generated to implement both user-defined generic-types and polymorphism with variadics, because \CFA compiles polymorphic functions versus template expansion.
+My analysis showed many wrapper functions are generated to implement both user-defined generic-types and polymorphism with variadics, because \CFA compiles polymorphic functions versus template expansion.
 Fortunately, the only permitted operations on polymorphic function parameters are given by the list of assertion (trait) functions.
 Nevertheless, this small set of functions eventually needs to be called with flattened tuple arguments.
@@ -824 +824 @@
 
 In general, non-standard C features (@gcc@) do not need any special treatment, as they are directly passed through to the C compiler.
-However, \PAB{I found} the Plan-9 semantics allow implicit conversions from the outer type to the inner type, which means the \CFA type resolver must take this information into account.
+However, I found the Plan-9 semantics allow implicit conversions from the outer type to the inner type, which means the \CFA type resolver must take this information into account.
 Therefore, the \CFA resolver must implement the Plan-9 features and insert necessary type conversions into the translated code output.
 In the current version of \CFA, this is the only kind of implicit type conversion other than the standard C arithmetic conversions.

doc/theses/fangren_yu_MMath/future.tex

@@ -4 +4 @@
 The following are feature requests related to type-system enhancements that have surfaced during the development of the \CFA language and library, but have not been implemented yet.
 Currently, developers must work around these missing features, sometimes resulting in inefficiency.
-\PAB{The following sections discuss new features I am proposing to fix these problems.}
+The following sections discuss new features I am proposing to fix these problems.
 
 

doc/theses/fangren_yu_MMath/resolution.tex

@@ -54 +54 @@
 Some of those problems arise from the newly introduced language features described in the previous chapter.
 In addition, fixing unexpected interactions within the type system has presented challenges.
-This chapter describes in detail the type-resolution rules currently in use and some major problems \PAB{I} have identified.
+This chapter describes in detail the type-resolution rules currently in use and some major problems I have identified.
 Not all of those problems have immediate solutions, because fixing them may require redesigning parts of the \CFA type system at a larger scale, which correspondingly affects the language design.
 
@@ -152 +152 @@
 Therefore, at each resolution step, the arguments are already given unique interpretations, so the ordering only needs to compare different sets of conversion targets (function parameter types) on the same set of input.
 
-\PAB{My conclusion} is that trying to use such a system in \CFA is problematic because of the presence of return-type overloading of functions and variables.
+My conclusion is that trying to use such a system in \CFA is problematic because of the presence of return-type overloading of functions and variables.
 Specifically, \CFA expression resolution considers multiple interpretations of argument subexpressions with different types, \eg:
 so it is possible that both the selected function and the set of arguments are different, and cannot be compared with a partial-ordering system.
@@ -379 +379 @@
 if an expression has any legal interpretations as a C builtin operation, only the lowest cost one is kept, regardless of the result type.
 
-\VRef[Figure]{f:CFAArithmeticConversions} shows \PAB{my} alternative \CFA partial-order arithmetic-conversions graphically.
+\VRef[Figure]{f:CFAArithmeticConversions} shows my alternative \CFA partial-order arithmetic-conversions graphically.
 The idea here is to first look for the best integral alternative because integral calculations are exact and cheap.
 If no integral solution is found, than there are different rules to select among floating-point alternatives.
@@ -408 +408 @@
 With the introduction of generic record types, the parameters must match exactly as well; currently there are no covariance or contravariance supported for the generics.
 
-\PAB{I made} one simplification to the \CFA language that makes modelling the type system easier: polymorphic function pointer types are no longer allowed.
+I made one simplification to the \CFA language that makes modelling the type system easier: polymorphic function pointer types are no longer allowed.
 The polymorphic function declarations themselves are still treated as function pointer types internally, however the change means that formal parameter types can no longer be polymorphic.
 Previously it was possible to write function prototypes such as 
@@ -441 +441 @@
 The assertion set that needs to be resolved is just the declarations on the function prototype, which also simplifies the assertion satisfaction algorithm, which is discussed further in the next section.
 
-\PAB{My} implementation sketch stores type unification results in a type-environment data-structure, which represents all the type variables currently in scope as equivalent classes, together with their bound types and information such as whether the bound type is allowed to be opaque (\ie a forward declaration without definition in scope) and whether the bounds are allowed to be widened.
+My implementation sketch stores type unification results in a type-environment data-structure, which represents all the type variables currently in scope as equivalent classes, together with their bound types and information such as whether the bound type is allowed to be opaque (\ie a forward declaration without definition in scope) and whether the bounds are allowed to be widened.
 In the general approach commonly used in functional languages, the unification variables are given a lower bound and an upper bound to account for covariance and contravariance of types.
 \CFA does not implement any variance with its generic types and does not allow polymorphic function types, therefore no explicit upper bound is needed and one binding value for each equivalence class suffices.
@@ -475 +475 @@
 One example is analysed in this section.
 
-\PAB{My analysis shows that} while the assertion satisfaction problem in isolation looks like just another expression to resolve, its recursive nature makes some techniques for expression resolution no longer possible.
+My analysis shows that while the assertion satisfaction problem in isolation looks like just another expression to resolve, its recursive nature makes some techniques for expression resolution no longer possible.
 The most significant impact is that type unification has a side effect, namely editing the type environment (equivalence classes and bindings), which means if one expression has multiple associated assertions it is dependent, as the changes to the type environment must be compatible for all the assertions to be resolved.
 Particularly, if one assertion parameter can be resolved in multiple different ways, all of the results need to be checked to make sure the change to type variable bindings are compatible with other assertions to be resolved.
@@ -494 +494 @@
 If any new assertions are introduced by the selected candidates, the algorithm is applied recursively, until there are none pending resolution or the recursion limit is reached, which results in a failure.
 
-However, \PAB{I identify that} in practice the efficiency of this algorithm can be sensitive to the order of resolving assertions.
+However, I identify that in practice the efficiency of this algorithm can be sensitive to the order of resolving assertions.
 Suppose an unbound type variable @T@ appears in two assertions:
 \begin{cfa}
@@ -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.
-
-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 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.
+
+\PAB{Based on this observation, I implemented an optimization to the assertion resolution algorithm that only attempts to resolve object assertions after all other assertions are resolved successfully.
+As well, it further delays 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.
+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.}
+
+\PAB{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.
@@ -528 +531 @@
 }
 \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, 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}.
+\PAB{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}.}
 
 
@@ -537 +540 @@
 Based on the experiment results, this approach can improve the performance of expression resolution in general, and sometimes allow difficult instances of assertion resolution problems to be solved that are otherwise infeasible, \eg when the resolution encounters an infinite loop.
 
-\PAB{I identify that} the tricky problem in implementing this approach is that the resolution algorithm has side effects, namely modifying the type bindings in the environment.
+I identify that the tricky problem in implementing this approach is that the resolution algorithm has side effects, namely modifying the type bindings in the environment.
 If the modifications are cached, \ie the results that cause the type bindings to be modified, it is also necessary to store the changes to type bindings, too.
 Furthermore, in cases where multiple candidates can be used to satisfy one assertion parameter, all of them must be cached including those that are not eventually selected, since the side effect can produce different results depending on the context.
@@ -585 +588 @@
 However, the implementation of the type environment is simplified;
 it only stores a tentative type binding with a flag indicating whether \emph{widening} is possible for an equivalence class of type variables. 
-Formally speaking, \PAB{I concluded} the type environment used in \CFA is only capable of representing \emph{lower-bound} constraints.
+Formally speaking, I concluded the type environment used in \CFA is only capable of representing \emph{lower-bound} constraints.
 This simplification works most of the time, given the following properties of the existing \CFA type system and the resolution algorithms:
 \begin{enumerate}