Changeset f845e80 for doc

Timestamp:

Apr 25, 2019, 2:23:48 PM (5 years ago)

Author:

Aaron Moss <a3moss@…>

Branches:

ADT, aaron-thesis, arm-eh, ast-experimental, cleanup-dtors, enum, forall-pointer-decay, jacob/cs343-translation, jenkins-sandbox, master, new-ast, new-ast-unique-expr, pthread-emulation, qualifiedEnum

Children:

98b4b12

Parents:

69c37cc

Message:

thesis: apply round 2 revisions and strip change bars

Location:

doc/theses/aaron_moss_PhD/phd

Files:

• background.tex (modified) (5 diffs)
• conclusion.tex (modified) (1 diff)
• experiments.tex (modified) (5 diffs)
• frontpgs.tex (modified) (1 diff)
• generic-bench.tex (modified) (1 diff)
• generic-types.tex (modified) (1 diff)
• introduction.tex (modified) (1 diff)
• resolution-heuristics.tex (modified) (7 diffs)
• thesis.tex (modified) (2 diffs)
• type-environment.tex (modified) (3 diffs)

doc/theses/aaron_moss_PhD/phd/background.tex

@@ -13 +13 @@
 Notable features added during this period include generic types (Chapter~\ref{generic-chap}), constructors and destructors \cite{Schluntz17}, improved support for tuples \cite{Schluntz17}, reference types \cite{Moss18}, first-class concurrent and parallel programming support \cite{Delisle18}, as well as numerous pieces of syntactic sugar and the start of an idiomatic standard library \cite{Moss18}.
 
-\cbstart
 This thesis is primarily concerned with the \emph{expression resolution} portion of \CFA{} type-checking; resolution is discussed in more detail in Chapter~\ref{resolution-chap}, but is essentially determining which declarations the identifiers in each expression correspond to. 
-Given that no simultaneously-visible C declarations share identifiers, expression resolution in C is not difficult, but the added features of \CFA{} make its resolution algorithms significantly more complex. 
-Due to this complexity, the expression-resolution pass in \CFACC{} requires 95\% of compiler runtime on some source files, making an efficient procedure for expression resolution a requirement for a performant \CFA{} compiler.
-\cbend
+In C, no simultaneously-visible declarations share identifiers, hence expression resolution in C is not difficult. 
+In \CFA{}, multiple added features make the resolution process significantly more complex. 
+Due to this complexity, the expression-resolution pass in \CFACC{} requires 95\% of compiler runtime on some source files, making a new, more efficient procedure for expression resolution a requirement for a performant \CFA{} compiler.
 
 The features presented in this chapter are chosen to elucidate the design constraints of the work presented in this thesis. 
@@ -208 +207 @@
 Given a declaration !list_iterator it!, !*it! can be either an !int! or a !list!, with the meaning disambiguated by context (\eg{} !int x = *it;! interprets !*it! as !int!, while !(*it).value = 42;! interprets !*it! as !list!). 
 While a nominal-inheritance system with associated types could model one of those two relationships by making !El! an associated type of !Ptr! in the !pointer_like! implementation, 
-\cbstart
-the author is unaware of any nominal-inheritance system that could model both relationships simultaneously. 
+I am unaware of any nominal-inheritance system that can model both relationships simultaneously. 
 Further comparison of \CFA{} polymorphism with other languages can be found in Section~\ref{generic-related-sec}.
-\cbend
 
 The flexibility of \CFA{}'s implicit trait-satisfaction mechanism provides programmers with a great deal of power, but also blocks some optimization approaches for expression resolution. 
 The ability of types to begin or cease to satisfy traits when declarations go into or out of scope makes caching of trait satisfaction judgments difficult, and the ability of traits to take multiple type parameters can lead to a combinatorial explosion of work in any attempt to pre-compute trait satisfaction relationships.
 
-\cbstart
 \subsection{Deleted Declarations}
 
-Particular type combinations can be exempted from matching a given polymorphic function through use of a \emph{deleted function declaration}:
+Particular type combinations can be exempted from matching a given polymorphic function through the use of a \emph{deleted function declaration}:
 
 \begin{cfa}
@@ -228 +224 @@
 Deleted function declarations are implemented in \CFACC{} by adding them to the symbol table as usual, but with a flag set that indicates that the function is deleted. 
 If this deleted declaration is selected as the unique minimal-cost interpretation of an expression then an error is produced, allowing \CFA{} programmers to guide the expression resolver away from undesirable solutions.
-\cbend
 
 \section{Implicit Conversions} \label{implicit-conv-sec}
@@ -254 +249 @@
 Given some type !T!, a !T&! (``reference to !T!'') is essentially an automatically dereferenced pointer. 
 These types allow seamless pass-by-reference for function parameters, without the extraneous dereferencing syntax present in C; they also allow easy aliasing of nested values with a similarly convenient syntax. 
-\cbstart
 The addition of reference types also eliminated two syntactic special-cases present in previous versions of \CFA{}. 
-Considering a call !a += b! to a compound assignment operator, the previous declaration for that operator was !lvalue int ?+=?(int*, int)! -- to mutate the left argument, the built-in operators were special-cased to implicitly take the address of that argument, while the special !lvalue! syntax was used to mark the return type of a function as a mutable reference. 
-With references, this declaration can be re-written as !int& ?+=?(int&, int)! -- the reference semantics generalize the implicit address-of on the left argument and allow it to be used in user-declared functions, while also subsuming the (now removed) !lvalue! syntax for function return types.
-\cbend
+Consider the a call !a += b! to a compound assignment operator. 
+The previous declaration for that operator is !lvalue int ?+=?(int*, int)!. 
+To mutate the left argument, the built-in operators were special-cased to implicitly take the address of that argument, while the special !lvalue! syntax was used to mark the return type of a function as a mutable reference. 
+With references, this declaration is re-written as !int& ?+=?(int&, int)!. 
+The reference semantics generalize the implicit address-of on the left argument and allow it to be used in user-declared functions, while also subsuming the (now removed) !lvalue! syntax for function return types.
 
 The C standard makes heavy use of the concept of \emph{lvalue}, an expression with a memory address; its complement, \emph{rvalue} (a non-addressable expression) is not explicitly named in the standard. 
@@ -281 +277 @@
 \CFA{} supports all of these use cases without further added syntax. 
 The key to this syntax-free feature support is an observation made by the author that the address of a reference is a lvalue. 
-In C, the address-of operator !&x! can only be applied to lvalue expressions, and always produces an immutable rvalue; \CFA{} supports reference re-binding by assignment to the address of a reference\footnote{\cbstart The syntactic difference between reference initialization and reference assignment is unfortunate, but preserves the ability to pass function arguments by reference (a reference initialization context) without added syntax. \cbend }, and pointers to references by repeating the address-of operator:
+In C, the address-of operator !&x! can only be applied to lvalue expressions, and always produces an immutable rvalue; \CFA{} supports reference re-binding by assignment to the address of a reference\footnote{The syntactic difference between reference initialization and reference assignment is unfortunate, but preserves the ability to pass function arguments by reference (a reference initialization context) without added syntax.}, and pointers to references by repeating the address-of operator:
 
 \begin{cfa}

doc/theses/aaron_moss_PhD/phd/conclusion.tex

@@ -13 +13 @@
 An alternate approach would be to fork an existing C compiler such as Clang~\cite{Clang}, which would need to be modified to use one of the resolution algorithms discussed here, as well as various other features introduced by Bilson~\cite{Bilson03}.
 
-\cbstart
 More generally, the algorithmic techniques described in this thesis may be useful to implementors of other programming languages. 
 In particular, the demonstration of practical performance for polymorphic return-type inference suggests the possibility of eliding return-type-only template parameters in \CC{} function calls, though integrating such an extension into \CC{} expression resolution in a backwards-compatible manner may be challenging. 
-The \CFA{} expression resolution problem also bears some similarity to the \emph{local type inference} model put forward by Pierce \& Turner \cite{Pierce00} and Odersky \etal{} \cite{Odersky01}; compiler implementors for languages such as Scala \cite{Scala} that perform type inference based on this model may be able to profitably adapt the algorithms and data structures presented in this thesis.
-\cbend
+The \CFA{} expression resolution problem also bears some similarity to the \emph{local type inference} model put forward by Pierce \& Turner \cite{Pierce00} and Odersky \etal{} \cite{Odersky01}; compiler implementors for languages like Scala \cite{Scala}, which performs type inference based on this model, may be able to profitably adapt the algorithms and data structures presented in this thesis.

doc/theses/aaron_moss_PhD/phd/experiments.tex

@@ -7 +7 @@
 
 \CFACC{} can generate realistic test inputs for the resolver prototype from equivalent \CFA{} code; 
-the generated test inputs currently comprise all \CFA{} code currently in existence\footnote{ \cbstart Though \CFA{} is backwards-compatible with C, the lack of \lstinline{forall} functions and name overloading in C mean that the larger corpus of C code does not provide challenging test instances for \CFACC{} \cbend }, 9,000 lines drawn primarily from the standard library and compiler test suite. 
-\cbstart
+the generated test inputs currently comprise all \CFA{} code currently in existence\footnote{Though \CFA{} is backwards-compatible with C, the lack of \lstinline{forall} functions and name overloading in C mean that the larger corpus of C code does not provide challenging test instances for \CFACC{}.}, 9,000 lines drawn primarily from the standard library and compiler test suite. 
 This code includes a substantial degree of name overloading for common library functions and a number of fundamental polymorphic abstractions, including iterators and streaming input/output. 
-\cbend
 \CFACC{} is also instrumented to produce a number of code metrics. 
 These metrics were used to construct synthetic test inputs during development of the resolver prototype; these synthetic inputs provided useful design guidance, but the performance results presented in this chapter are based on the more realistic directly-generated inputs.
@@ -212 +210 @@
 A top-down algorithm was not attempted in \CFACC{} due to its poor performance in the prototype.
 The second round of modifications addressed assertion satisfaction, taking Bilson's original \textsc{cfa-imm} algorithm and modifying it to use the deferred approach \textsc{cfa-def}. 
-\cbstart
-Due to time constraints a deferred-cached assertion satisfaction algorithm for \CFACC{} could not be completed, but both preliminary results from this effort and the averaged prototype results from Section~\ref{proto-exp-sec} indicate that assertion satisfaction caching is not likely to be a fruitful optimization for \CFACC{}. 
-\cbend
+Due to time constraints, a deferred-cached assertion satisfaction algorithm for \CFACC{} could not be completed, but both preliminary results from this effort and the averaged prototype results from Section~\ref{proto-exp-sec} indicate that assertion satisfaction caching is not likely to be a fruitful optimization for \CFACC{}. 
 The new environment data structures discussed in Section~\ref{proto-exp-sec} have not been successfully merged into \CFACC{} due to their dependencies on the garbage-collection framework in the prototype; I spent several months modifying \CFACC{} to use similar garbage collection, but due to \CFACC{} not being designed to use such memory management the performance of the modified compiler was non-viable. 
 It is possible that the persistent union-find environment could be modified to use a reference-counted pointer internally without changing the entire memory-management framework of \CFACC{}, but such an attempt is left to future work.
@@ -221 +217 @@
 The results from \CFACC{} for \textsc{cfa-co} \vs{} \textsc{cfa-bu} do not mirror those from the prototype; I conjecture this is mostly due to the different memory-management schemes and sorts of data required to run type unification and assertion satisfaction calculations, as \CFACC{} performance has proven to be particularly sensitive to the amount of heap allocation performed. 
 This data also shows a noticeable regression in compiler performance in the eleven months between \textsc{cfa-bu} and \textsc{cfa-imm}, which use the same resolution algorithms; this approximate doubling in runtime is not due to expression resolution, as no integration work happened in this time, but I am unable to ascertain its actual cause. 
-\cbstart
 To isolate the effects of the algorithmic changes from this unrelated performance regression, the speedup results in Figure~\ref{cfa-speedup-fig} are shown with respect to the start of each modification round, \textsc{cfa-bu} \vs{} \textsc{cfa-co} and \textsc{cfa-def} \vs{} \textsc{cfa-imm}.
-\cbend
 It should also be noted with regard to the peak memory results in Figure~\ref{cfa-mem-fig} that the peak memory usage does not always occur during the resolution phase of the compiler. 
 
@@ -232 +226 @@
 \end{figure}
 
-\cbstart
 \begin{figure}
 \centering
@@ -238 +231 @@
 \caption[\CFACC{} speedup.]{\CFACC{} speedup against against \textsc{cfa-co} baseline runtime. To isolate the effect of algorithmic changes, \textsc{cfa-bu} speedup is \vs{} \textsc{cfa-co} while \textsc{cfa-def} speedup is \vs{} \textsc{cfa-imm}. The `inter-round' series shows slowdown between \textsc{cfa-bu} and \textsc{cfa-imm}.} \label{cfa-speedup-fig}
 \end{figure}
-\cbend
 
 \begin{figure}

doc/theses/aaron_moss_PhD/phd/frontpgs.tex

@@ -141 +141 @@
         The compilation performance improvements have all been experimentally validated with a new prototype system that encapsulates the key aspects of the \CFA{} language; this prototype is a promising basis for future research and a technical contribution of this work.
 
-        \cbstart
         \CFA{}, extended and refined in this thesis, presents both an independently interesting combination of language features and a comprehensive approach to the modernization of C. 
         This work demonstrates the hitherto unproven compiler-implementation viability of the \CFA{} language design, and provides a number of useful tools to implementors of other languages.
-        \cbend
 
 \cleardoublepage

doc/theses/aaron_moss_PhD/phd/generic-bench.tex

@@ -1 +1 @@
 \chapter{Generic Stack Benchmarks} \label{generic-bench-app}
 
-\cbstart
 This appendix includes the generic stack code for all four language variants discussed in Section~\ref{generic-performance-sec}. Throughout, !/***/! designates a counted redundant type annotation; these include !sizeof! on a known type, repetition of a type name in initialization or return statements, and type-specific helper functions.
-\cbend
 The code is reformatted slightly for brevity.
 

doc/theses/aaron_moss_PhD/phd/generic-types.tex

@@ -333 +333 @@
 \end{cfa}
 
-Here, !_assign_T! is passed in as an implicit parameter from !otype T! and takes two !T*! (!void*! in the generated code\footnote{ \cbstart A GCC extension allows arithmetic on \lstinline{void*}, calculated as if \lstinline{sizeof(void) == 1}. \cbend }), a destination and a source, and !_retval! is the pointer to a caller-allocated buffer for the return value, the usual \CFA{} method to handle dynamically-sized return types. 
+Here, !_assign_T! is passed in as an implicit parameter from !otype T! and takes two !T*! (!void*! in the generated code\footnote{A GCC extension allows arithmetic on \lstinline{void*}, calculated as if \lstinline{sizeof(void) == 1}.}), a destination and a source, and !_retval! is the pointer to a caller-allocated buffer for the return value, the usual \CFA{} method to handle dynamically-sized return types. 
 !_offsetof_pair! is the offset array passed into !value!; this array is statically generated at the call site as:
 

doc/theses/aaron_moss_PhD/phd/introduction.tex

@@ -37 +37 @@
 \end{itemize}
 
-\cbstart
 The prototype system, which implements the algorithmic contributions of this thesis, is the first performant type-checker implementation for a \CFA{}-style type system. 
 As the existence of an efficient compiler is necessary for the practical viability of a programming language, the contributions of this thesis comprise a validation of the \CFA{} language design that was previously lacking.
-\cbend
 
 Though the direction and experimental validation of this work is fairly narrowly focused on the \CFA{} programming language, the tools used and results obtained should be of interest to a wider compiler and programming language design community. 
 In particular, with the addition of \emph{concepts} in \CCtwenty{}~\cite{C++Concepts}, conforming \CC{} compilers must support a model of type assertions very similar to that in \CFA{}, and the algorithmic techniques used here may prove useful. 
-\cbstart
-Much of the difficulty of type-checking \CFA{} stems from the language design choice to allow type inference from the context of a function call in addition to its arguments; this feature allows the programmers to specify fewer redundant type annotations on functions that are polymorphic in their return type.
-\cbend \cbstartx
-The !auto! keyword in \CCeleven{} supports a similar but sharply restricted form of this contextual inference -- the demonstration of the richer inference in \CFA{} raises possibilities for similar features in future versions of \CC{}. 
-By contrast, Java~8~\cite{Java8} and Scala~\cite{Scala} use comparably powerful forms of type inference, so the algorithmic techniques in this thesis may be effective for those languages' compiler implementors. 
-\cbendx
+Much of the difficulty of type-checking \CFA{} stems from the language design choice to allow overload selection from the context of a function call based on function return type in addition to the type of the arguments to the call; this feature allows the programmers to specify fewer redundant type annotations on functions that are polymorphic in their return type.
+As an example in \CC{}:
+\begin{C++}
+template<typename T> T* zero() { return new T( 0 ); }
+
+int* z = zero<int>();  $\C{// must specify int twice}$
+\end{C++}
+
+\CFA{} allows !int* z = zero()!, which elides the second !int!. 
+While the !auto! keyword in \CCeleven{} supports similar inference in a limited set of contexts (\eg{} !auto z = zero<int>()!), the demonstration of the richer inference in \CFA{} raises possibilities for similar features in future versions of \CC{}. 
+By contrast to \CC{}, Java~8~\cite{Java8} and Scala~\cite{Scala} use comparably powerful forms of type inference to \CFA{}, so the algorithmic techniques in this thesis may be effective for those languages' compiler implementors. 
 Type environments are also widely modelled in compiler implementations, particularly for functional languages, though also increasingly commonly for other languages (such as Rust~\cite{Rust}) that perform type inference; the type environment presented here may be useful to those language implementors.
 
-\cbstarty
 One area of inquiry that is outside the scope of this thesis is formalization of the \CFA{} type system. 
-Ditchfield~\cite{Ditchfield92} defined the $F_\omega^\ni$ polymorphic lambda calculus which is the theoretical basis for the \CFA{} type system. 
+Ditchfield~\cite{Ditchfield92} defined the $F_\omega^\ni$ polymorphic lambda calculus, which is the theoretical basis for the \CFA{} type system. 
 Ditchfield did not, however, prove any soundness or completeness properties for $F_\omega^\ni$; such proofs remain future work. 
 A number of formalisms other than $F_\omega^\ni$ could potentially be adapted to model \CFA{}. 
-One promising candidate is \emph{local type inference} \cite{Pierce00,Odersky01}, which describes similar contextual propagation of type information; another is the polymorphic conformity-based model of the Emerald~\cite{Black90} programming language, which defines a subtyping relation on types that are conceptually similar to \CFA{} traits.
+One promising candidate is \emph{local type inference} \cite{Pierce00,Odersky01}, which describes similar contextual propagation of type information; another is the polymorphic conformity-based model of the Emerald~\cite{Black90} programming language, which defines a subtyping relation on types that is conceptually similar to \CFA{} traits.
 These modelling approaches could potentially be used to extend an existing formal semantics for C such as Cholera \cite{Norrish98}, CompCert \cite{Leroy09}, or Formalin \cite{Krebbers14}.
-\cbendy

doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex

@@ -6 +6 @@
 A given matching between identifiers and declarations in an expression is an \emph{interpretation}; an interpretation also includes information about polymorphic type bindings and implicit casts to support the \CFA{} features discussed in Sections~\ref{poly-func-sec} and~\ref{implicit-conv-sec}, each of which increase the number of valid candidate interpretations. 
 To choose among valid interpretations, a \emph{conversion cost} is used to rank interpretations. 
-\cbstart
 This conversion cost is summed over all subexpression interpretations in the interpretation of a top-level expression. 
-\cbend
 Hence, the expression resolution problem is to find the unique minimal-cost interpretation for an expression, reporting an error if no such unique interpretation exists.
 
 \section{Expression Resolution}
 
-\cbstart
-The expression resolution pass in \CFACC{} must traverse the input expression, match identifiers to available declarations, rank candidate interpretations according to their conversion cost, and check type assertion satisfaction for these candidates. 
-Once the set of valid interpretations for the top-level expression has been found, the expression resolver selects the unique minimal-cost candidate or reports an error. 
+The expression resolution pass in \CFACC{} must traverse an input expression, match identifiers to available declarations, rank candidate interpretations according to their conversion cost, and check type assertion satisfaction for these candidates. 
+Once the set of valid interpretations for the top-level expression is found, the expression resolver selects the unique minimal-cost candidate or reports an error. 
 
 The expression resolution problem in \CFA{} is more difficult than the analogous problems in C or \CC{}. 
-As mentioned above, the lack of name overloading in C makes its resolution problem substantially easier, but a comparison of the richer type systems in \CFA{} and \CC{} highlights some of the challenges in \CFA{} expression resolution. 
+As mentioned above, the lack of name overloading in C (except for built-in operators) makes its resolution problem substantially easier. 
+A comparison of the richer type systems in \CFA{} and \CC{} highlights some of the challenges in \CFA{} expression resolution. 
 The key distinction between \CFA{} and \CC{} resolution is that \CC{} uses a greedy algorithm for selection of candidate functions given their argument interpretations, whereas \CFA{} allows contextual information from superexpressions to influence the choice among candidate functions. 
-One key use of this contextual information is for type inference of polymorphic return types; \CC{} requires explicit specification of template type parameters that only occur in a function's return type, while \CFA{} allows the instantiation of these type parameters to be inferred from context (and in fact does not allow explicit specification of type parameters to a function). 
+One key use of this contextual information is for type inference of polymorphic return types; \CC{} requires explicit specification of template parameters that only occur in a function's return type, while \CFA{} allows the instantiation of these type parameters to be inferred from context(and in fact does not allow explicit specification of type parameters to a function), as in the following example:
+
+\begin{cfa}
+forall(dtype T) T& deref(T*); $\C{// dereferences pointer}$
+forall(otype T) T* def(); $\C{// new heap-allocated default-initialized value}$
+
+int& i = deref( def() );
+\end{cfa}
+
+In this example, the \CFA{} compiler infers the type arguments of !deref! and !def! from the !int&! type of !i!; \CC{}, by contrast, requires a type parameter on !def!\footnote{The type parameter of \lstinline{deref} can be inferred from its argument.}, \ie{} !deref( def<int>() )!.
 Similarly, while both \CFA{} and \CC{} rank candidate functions based on a cost metric for implicit conversions, \CFA{} allows a suboptimal subexpression interpretation to be selected if it allows a lower-cost overall interpretation, while \CC{} requires that each subexpression interpretation have minimal cost. 
 Because of this use of contextual information, the \CFA{} expression resolver must consider multiple interpretations of each function argument, while the \CC{} compiler has only a single interpretation for each argument\footnote{With the exception of address-of operations on functions.}. 
 Additionally, until the introduction of concepts in \CCtwenty{} \cite{C++Concepts}, \CC{} expression resolution has no analogue to \CFA{} assertion satisfaction checking, a further  complication for a \CFA{} compiler. 
 The precise definition of \CFA{} expression resolution in this section further expands on the challenges of this problem. 
-\cbend
 
 \subsection{Type Unification}
@@ -37 +43 @@
 \subsection{Conversion Cost} \label{conv-cost-sec}
 
-\cbstart
 \CFA{}, like C, allows inexact matches between the type of function parameters and function call arguments. 
 Both languages insert \emph{implicit conversions} in these situations to produce an exact type match, and \CFA{} also uses the relative \emph{cost} of different conversions to select among overloaded function candidates. 
-\cbend
 C does not have an explicit cost model for implicit conversions, but the ``usual arithmetic conversions'' \cite[\S{}6.3.1.8]{C11} used to decide which arithmetic operators to apply define one implicitly. 
 The only context in which C has name overloading is the arithmetic operators, and the usual arithmetic conversions define a \emph{common type} for mixed-type arguments to binary arithmetic operators. 
@@ -148 +152 @@
 In terms of the core argument-parameter matching algorithm, overloaded variables are handled the same as zero-argument function calls, aside from a different pool of candidate declarations and setup for different code generation. 
 Similarly, an aggregate member expression !a.m! can be modelled as a unary function !m! that takes one argument of the aggregate type.
-Literals do not require sophisticated resolution, as in C the syntactic form of each implies their result types: !42! is !int!, !"hello"! is !char*!, \etc{}\footnote{ \cbstart Struct literals (\eg{} \lstinline|(S)\{ 1, 2, 3 \}| for some struct \lstinline{S} \cbend ) are a somewhat special case, as they are known to be of type \lstinline{S}, but require resolution of the implied constructor call described in Section~\ref{ctor-sec}.}.
+Literals do not require sophisticated resolution, as in C the syntactic form of each implies their result types: !42! is !int!, !"hello"! is !char*!, \etc{}\footnote{Struct literals (\eg{} \lstinline|(S)\{ 1, 2, 3 \}| for some struct \lstinline{S}) are a somewhat special case, as they are known to be of type \lstinline{S}, but require resolution of the implied constructor call described in Section~\ref{ctor-sec}.}.
 
 Since most expressions can be treated as function calls, nested function calls are the primary component of complexity in expression resolution. 
@@ -306 +310 @@
 This approach of filtering out invalid types is unsuited to \CFA{} expression resolution, however, due to the presence of polymorphic functions and implicit conversions. 
 
-\cbstart
 Some other language designs solve the matching problem by forcing a bottom-up order. 
 \CC{}, for instance, defines its overload-selection algorithm in terms of a partial order between function overloads given a fixed list of argument candidates, implying that the arguments must be selected before the function. 
-This design choice improves worst-case expression resolution time by only propagating a single candidate for each subexpression, but type annotations must be provided for any function call that is polymorphic in its return type, and these annotations are often redundant.
-\CFA{}, by contrast, saves programmers from redundant annotations with its richer inference:
+This design choice improves worst-case expression resolution time by only propagating a single candidate for each subexpression, but type annotations must be provided for any function call that is polymorphic in its return type, and these annotations are often redundant:
+
+\begin{C++}
+template<typename T> T* malloc() { /* ... */ }
+
+int* p = malloc<int>(); $\C{// T = int must be explicitly supplied}$
+\end{C++}
+
+\CFA{} saves programmers from redundant annotations with its richer inference:
 
 \begin{cfa}
@@ -317 +327 @@
 int* p = malloc(); $\C{// Infers T = int from left-hand side}$
 \end{cfa}
-\cbend
 
 Baker~\cite{Baker82} left empirical comparison of different overload resolution algorithms to future work; Bilson~\cite{Bilson03} described an extension of Baker's algorithm to handle implicit conversions and polymorphism, but did not further explore the space of algorithmic approaches to handle both overloaded names and implicit conversions. 
@@ -394 +403 @@
 This adjusted assertion declaration is then run through the \CFA{} name-mangling algorithm to produce an equivalent string-type key.
 
-\cbstart
-One superficially-promising optimization which I did not pursue is caching assertion-satisfaction judgments between top-level expressions. 
+One superficially-promising optimization, which I did not pursue, is caching assertion-satisfaction judgments among top-level expressions. 
 This approach would be difficult to correctly implement in a \CFA{} compiler, due to the lack of a closed set of operations for a given type. 
 New declarations related to a particular type can be introduced in any lexical scope in \CFA{}, and these added declarations may cause an assertion that was previously satisfiable to fail due to an introduced ambiguity. 
 Furthermore, given the recursive nature of assertion satisfaction and the possibility of this satisfaction judgment depending on an inferred type, an added declaration may break satisfaction of an assertion with a different name and that operates on different types. 
 Given these concerns, correctly invalidating a cross-expression assertion satisfaction cache for \CFA{} is a non-trivial problem, and the overhead of such an approach may possibly outweigh any benefits from such caching.
-\cbend
 
 The assertion satisfaction aspect of \CFA{} expression resolution bears some similarity to satisfiability problems from logic, and as such other languages with similar trait and assertion mechanisms make use of logic-program solvers in their compilers. 
@@ -406 +413 @@
 The combination of the assertion satisfaction elements of the problem with the conversion-cost model of \CFA{} makes this logic-solver approach difficult to apply in \CFACC{}, however. 
 Expressing assertion resolution as a satisfiability problem ignores the cost optimization aspect, which is necessary to decide among what are often many possible satisfying assignments of declarations to assertions. 
-\cbstartx
 (MaxSAT solvers \cite{Morgado13}, which allow weights on solutions to satisfiability problems, may be a productive avenue for future investigation.) 
-\cbendx
 On the other hand, the deeply-recursive nature of the satisfiability problem makes it difficult to adapt to optimizing solver approaches such as linear programming. 
 To maintain a well-defined programming language, any optimization algorithm used must provide an exact (rather than approximate) solution; this constraint also rules out a whole class of approximately-optimal generalized solvers. 

doc/theses/aaron_moss_PhD/phd/thesis.tex

@@ -16 +16 @@
 \usepackage{ifthen}
 \newboolean{PrintVersion}
-\setboolean{PrintVersion}{false} 
+\setboolean{PrintVersion}{true} 
 % CHANGE THIS VALUE TO "true" as necessary, to improve printed results for hard copies
 % by overriding some options of the hyperref package below.
@@ -31 +31 @@
 \usepackage{caption} % for subfigure
 \usepackage{subcaption}
-
-\usepackage[color]{changebar}
-\cbcolor{blue}
-\newcommand{\cbstartx}{\cbcolor{red} \cbstart}
-\newcommand{\cbendx}{\cbend \cbcolor{blue}}
-\newcommand{\cbstarty}{\cbcolor{green} \cbstart}
-\newcommand{\cbendy}{\cbend \cbcolor{blue}}
 
 % Hyperlinks make it very easy to navigate an electronic document.

doc/theses/aaron_moss_PhD/phd/type-environment.tex

@@ -15 +15 @@
 Each individual type class $T_i$ may also be associated with a \emph{bound}, $b_i$; this bound contains the \emph{bound type} that the variables in the type class are replaced with, but also includes other information in \CFACC{}, including whether type conversions are permissible on the bound type and what sort of type variables are contained in the class (data types, function types, or variadic tuples).
 
-\cbstart
 The following example demonstrates the use of a type environment for unification:
 
@@ -26 +25 @@
 
 Expression resolution starts from an empty type environment; from this empty environment, the calls to !g! can be independently resolved. 
-These resolutions result in two new type environments, $T = \{ \myset{\mathsf{G}_1} \rightarrow$ !int!$\}$ and $T' = \{ \myset{\mathsf{G}_2} \rightarrow$ !int!$\}$; the calls to !g! have generated distinct type variables !G!$_1$ and !G!$_2$, each bound to !int! by unification with their argument type. 
+These resolutions result in two new type environments, $T = \{ \myset{\mathsf{G}_1} \rightarrow$ !int!$\}$ and $T' = \{ \myset{\mathsf{G}_2} \rightarrow$ !int!$\}$; the calls to !g! have generated distinct type variables !G!$_1$ and !G!$_2$, each bound to !int! by unification with the type of its argument (!10! and !20!, both !int!). 
 To complete resolution of the call to !f!, both environments must be combined; resolving the first argument to !f! produces a new type environment $T'' = \{ \myset{\mathsf{G}_1, \mathsf{F}_1} \rightarrow$ !int!$\}$: the new type variable !F!$_1$ has been introduced and unified with !G!$_1$ (the return type of !g(10)!), and consequently bound to !int!. 
 To resolve the second argument to !f!, $T''$ must be checked for compatibility with $T'$; since !F!$_1$ unifies with !G!$_2$, their type classes must be merged. 
 Since both !F!$_1$ and !G!$_2$ are bound to !int!, this merge succeeds, producing the final environment $T'' = \{ \myset{\mathsf{G}_1, \mathsf{F}_1, \mathsf{G}_2} \rightarrow$ !int!$\}$.
-\cbend
 
 \begin{table}
@@ -300 +298 @@
 However, allowing multiple threads concurrent access to the persistent data structure is likely to result in ``reroot thrashing'', as different threads reroot the data structure to their own versions of interest. 
 This contention could be mitigated by partitioning the data structure into separate subtrees for each thread, with each subtree having its own root node, and the boundaries among them implemented with a lock-equipped !ThreadBoundary! edit node. 
-\cbstartx
 Alternatively, the concurrent hash trie of Prokopec \etal{} \cite{Prokopec11,Prokopec12} may be a useful hash-table replacement.
-\cbendx