Index: doc/theses/aaron_moss_PhD/phd/background.tex =================================================================== --- doc/theses/aaron_moss_PhD/phd/background.tex (revision c4b548680decf267a7f89bf48d4c62432c9a2cca) +++ doc/theses/aaron_moss_PhD/phd/background.tex (revision 3b40801b86ac09b0f7245748a95b4b64fecc1f91) @@ -13,7 +13,9 @@ 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 The features presented in this chapter are chosen to elucidate the design constraints of the work presented in this thesis. @@ -183,5 +185,6 @@ Traits, however, are significantly more powerful than nominal-inheritance interfaces; firstly, due to the scoping rules of the declarations that satisfy a trait's type assertions, a type may not satisfy a trait everywhere that that type is declared, as with !char! and the !nominal! trait above. -Secondly, because \CFA{} is not object-oriented and types do not have a closed set of methods, existing C library types can be extended to implement a trait simply by writing the requisite functions\footnote{\CC{} only allows partial extension of C types, because constructors, destructors, conversions, and the assignment, indexing, and function-call operators may only be defined in a class; \CFA{} does not have any of these restrictions.}. Finally, traits may be used to declare a relationship among multiple types, a property that may be difficult or impossible to represent in nominal-inheritance type systems\footnote{This example uses \CFA{}'s reference types, described in Section~\ref{type-features-sec}.}: +Secondly, because \CFA{} is not object-oriented and types do not have a closed set of methods, existing C library types can be extended to implement a trait simply by writing the requisite functions\footnote{\CC{} only allows partial extension of C types, because constructors, destructors, conversions, and the assignment, indexing, and function-call operators may only be defined in a class; \CFA{} does not have any of these restrictions.}. +Finally, traits may be used to declare a relationship among multiple types, a property that may be difficult or impossible to represent in nominal-inheritance type systems\footnote{This example uses \CFA{}'s reference types, described in Section~\ref{type-features-sec}.}: \begin{cfa} @@ -204,10 +207,14 @@ In this example above, !(list_iterator, int)! satisfies !pointer_like! by the user-defined dereference function, and !(list_iterator, list)! also satisfies !pointer_like! by the built-in dereference operator for pointers. 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, the author is unaware of any nominal-inheritance system that could model both relationships simultaneously. +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. 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} @@ -221,4 +228,5 @@ 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} @@ -246,7 +254,9 @@ 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 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. @@ -271,5 +281,5 @@ \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{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: +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: \begin{cfa} Index: doc/theses/aaron_moss_PhD/phd/conclusion.tex =================================================================== --- doc/theses/aaron_moss_PhD/phd/conclusion.tex (revision c4b548680decf267a7f89bf48d4c62432c9a2cca) +++ doc/theses/aaron_moss_PhD/phd/conclusion.tex (revision 3b40801b86ac09b0f7245748a95b4b64fecc1f91) @@ -13,5 +13,7 @@ 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 Index: doc/theses/aaron_moss_PhD/phd/experiments.tex =================================================================== --- doc/theses/aaron_moss_PhD/phd/experiments.tex (revision c4b548680decf267a7f89bf48d4c62432c9a2cca) +++ doc/theses/aaron_moss_PhD/phd/experiments.tex (revision 3b40801b86ac09b0f7245748a95b4b64fecc1f91) @@ -7,6 +7,8 @@ \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{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. +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 +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. @@ -108,5 +110,5 @@ As a matter of experimental practicality, test runs that exceeded 8~GB of peak resident memory usage are excluded from the data set. This restriction is justifiable by real-world use, as a compiler that is merely slow may be accommodated with patience, but one that uses in excess of 8~GB of RAM may be impossible to run on many currently deployed computer systems. -8~GB of RAM is not typical of the memory usage of the best-performing two variants, \textsc{bu-dca-bas} and \textsc{bu-dca-per}, which were able to run all 131 test inputs to completion with maximum memory usage of 70~MB and 78~MB, respectively. +8~GB of RAM is not typical of the memory usage of the best-performing two variants, \textsc{bu-dca-bas} and \textsc{bu-dca-per}, which were able to run all 131 test inputs to completion with maximum memory usage of 70~MB and 78~MB, respectively. However, this threshold did eliminate a significant number of algorithm-test variants, with the worst-performing variant, \textsc{td-imm-inc}, only completing 62 test inputs within the memory bound. Full results for tests completed by algorithm variant are presented in Figure~\ref{tests-completed-fig}. @@ -210,5 +212,7 @@ 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 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. @@ -217,5 +221,7 @@ 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. @@ -226,4 +232,5 @@ \end{figure} +\cbstart \begin{figure} \centering @@ -231,4 +238,5 @@ \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} Index: doc/theses/aaron_moss_PhD/phd/frontpgs.tex =================================================================== --- doc/theses/aaron_moss_PhD/phd/frontpgs.tex (revision c4b548680decf267a7f89bf48d4c62432c9a2cca) +++ doc/theses/aaron_moss_PhD/phd/frontpgs.tex (revision 3b40801b86ac09b0f7245748a95b4b64fecc1f91) @@ -141,6 +141,8 @@ 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 Index: doc/theses/aaron_moss_PhD/phd/generic-bench.tex =================================================================== --- doc/theses/aaron_moss_PhD/phd/generic-bench.tex (revision c4b548680decf267a7f89bf48d4c62432c9a2cca) +++ doc/theses/aaron_moss_PhD/phd/generic-bench.tex (revision 3b40801b86ac09b0f7245748a95b4b64fecc1f91) @@ -1,5 +1,7 @@ \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. Index: doc/theses/aaron_moss_PhD/phd/generic-types.tex =================================================================== --- doc/theses/aaron_moss_PhD/phd/generic-types.tex (revision c4b548680decf267a7f89bf48d4c62432c9a2cca) +++ doc/theses/aaron_moss_PhD/phd/generic-types.tex (revision 3b40801b86ac09b0f7245748a95b4b64fecc1f91) @@ -333,5 +333,5 @@ \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{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. +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. !_offsetof_pair! is the offset array passed into !value!; this array is statically generated at the call site as: Index: doc/theses/aaron_moss_PhD/phd/introduction.tex =================================================================== --- doc/theses/aaron_moss_PhD/phd/introduction.tex (revision c4b548680decf267a7f89bf48d4c62432c9a2cca) +++ doc/theses/aaron_moss_PhD/phd/introduction.tex (revision 3b40801b86ac09b0f7245748a95b4b64fecc1f91) @@ -37,11 +37,15 @@ \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 which 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 which are polymorphic in their return type. Java's diamond type-inference operator~\cite{Java-diamond} and the !auto! keyword in \CCeleven{} support similar but sharply restricted forms of this contextual inference -- the demonstration of the richer inference in \CFA{} raises possibilities for similar features in future versions of these languages. Scala~\cite{Scala}, by contrast, already supports a similarly-powerful \emph{local type inference} model~\cite{Pierce00,Odersky01}, so the algorithmic techniques in this thesis may be effective for Scala compiler implementors. +\cbend 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}) which perform type inference; the type environment presented here may be useful to those language implementors. Index: doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex =================================================================== --- doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex (revision c4b548680decf267a7f89bf48d4c62432c9a2cca) +++ doc/theses/aaron_moss_PhD/phd/resolution-heuristics.tex (revision 3b40801b86ac09b0f7245748a95b4b64fecc1f91) @@ -6,9 +6,12 @@ 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. @@ -22,4 +25,5 @@ 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} @@ -33,6 +37,8 @@ \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. @@ -142,5 +148,5 @@ 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{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}.}. +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}.}. Since most expressions can be treated as function calls, nested function calls are the primary component of complexity in expression resolution. @@ -300,4 +306,5 @@ 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. @@ -310,4 +317,5 @@ 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. @@ -386,4 +394,5 @@ 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 judgements between 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. @@ -391,4 +400,5 @@ Furthermore, given the recursive nature of assertion satisfaction and the possibility of this satisfaction judgement 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. Index: doc/theses/aaron_moss_PhD/phd/thesis.tex =================================================================== --- doc/theses/aaron_moss_PhD/phd/thesis.tex (revision c4b548680decf267a7f89bf48d4c62432c9a2cca) +++ doc/theses/aaron_moss_PhD/phd/thesis.tex (revision 3b40801b86ac09b0f7245748a95b4b64fecc1f91) @@ -31,4 +31,7 @@ \usepackage{caption} % for subfigure \usepackage{subcaption} + +\usepackage[color]{changebar} +\cbcolor{blue} % Hyperlinks make it very easy to navigate an electronic document. Index: doc/theses/aaron_moss_PhD/phd/type-environment.tex =================================================================== --- doc/theses/aaron_moss_PhD/phd/type-environment.tex (revision c4b548680decf267a7f89bf48d4c62432c9a2cca) +++ doc/theses/aaron_moss_PhD/phd/type-environment.tex (revision 3b40801b86ac09b0f7245748a95b4b64fecc1f91) @@ -15,4 +15,5 @@ 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: @@ -29,4 +30,5 @@ 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}