source: doc/theses/fangren_yu_MMath/resolution.tex@ 51b72bf5

\chapter{Resolution Algorithms}
\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;
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.
The reason is that the type resolver must analyze \emph{each} component of an expression with many possible forms of overloading, type restrictions, and conversions.
Designing a ruleset that is expressive, behaves as expected, \ie matches C programmer expectations, and can be efficiently implemented is a very challenging task.

I first worked on the \CFA type-system as a co-op student.
At that time, compiling a medium-sized \CFA program using advanced polymorphism took multiple minutes (5+ minutes)~\cite[\S~5]{Yu20}.
I found a number of type-resolution problems, which resulted in the following changes to the type-resolution algorithm.
\begin{enumerate}[itemsep=0pt]
\item
new AST data structure
\item
special symbol table and argument-dependent lookup
\item
late assertion-satisfaction
\item
revised function-type representation
\item
skip pruning on expressions for function types
\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.

\begin{table}[htb]
\centering
\caption{Compile time of selected files by compiler build in seconds}
\label{t:SelectedFileByCompilerBuild}
\lstset{deletekeywords={mutex,thread}}
\setlength{\extrarowheight}{1pt}
\vspace*{-4pt}
\begin{tabular}{l|r|rrrrr}
                                & \multicolumn{1}{c|}{Original} & \multicolumn{5}{c}{Accumulative fixes}        \\
\cline{3-7}                             
Test case               & \multicolumn{1}{c|}{resolver} & \multicolumn{1}{c}{1} & \multicolumn{1}{c}{2} & \multicolumn{1}{c}{3} & \multicolumn{1}{c}{4} & \multicolumn{1}{c}{5} \\
\hline
@lib/fstream@   & 86.4  & 25.2  & 10.8  & 9.5   & 7.8   & 7.1   \\
@lib/mutex@             & 210.4 & 77.4  & 16.7  & 15.1  & 12.6  & 11.7  \\
@lib/vector@    & 17.2  & 8.9   & 3.1   & 2.8   & 2.4   & 2.2   \\
@lib/stdlib@    & 16.6  & 8.3   & 3.2   & 2.9   & 2.6   & 2.4   \\
@test/io2@              & 300.8 & 53.6  & 43.2  & 27.9  & 19.1  & 16.3  \\
@test/thread@   & 210.9 & 73.5  & 17.0  & 15.1  & 12.6  & 11.8  \\
\end{tabular}
\medskip
\newline
Results are average of 5 runs (3 runs if time exceeds 100 seconds)
\end{table}

Since then, many new features utilizing the expressiveness of \CFA's type system have been implemented, such as generic container types similar to those in \CC's standard template library.
During the development of multiple \CFA programs and libraries, more weaknesses and design flaws have been discovered within the type system.
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 that have been 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.


\section{Expression Cost-Model}
\label{s:ExpressionCostModel}

\CFA has been using a total-order expression cost-model to resolve ambiguity of overloaded expressions from the very beginning.
Most \CFA operators can be overloaded in \CFA;
hence, they are treated the same way as other function calls with the same rules for overload resolution.

In \CFA, candidates of an overloaded expression are ranked by numerical cost elements, which accounts for any type conversions needed from a call-site argument type to the matching function parameter type, as well as polymorphic types and restrictions introduced by the @forall@ clause.
Currently, the expression cost has the following components, ranked from highest to lowest. where lower cost is better.
\begin{enumerate}[leftmargin=*]
\item \textbf{Unsafe} cost representing a narrowing conversion of arithmetic types, \eg @int@ to @short@, and qualifier-dropping conversions for pointer and reference types.
Narrowing conversions have the potential to lose (truncation) data.
A programmer must decide if the computed data-range can safely be shorted in the smaller storage.
Warnings for unsafe conversions are helpful.
\begin{cfa}
void f( short p );
f( 3L ); $\C[2.5in]{// unsafe conversion, possible warning}\CRT$
\end{cfa}

\item \textbf{Polymorphic} cost for a function parameter type that is or contains a polymorphic type variable.
The fewer polymorphic parameters means a more specific function, which may be able to compute faster or more accurately, like specialization templates in \CC.
\begin{cfa}
forall( T ) f( T p, int i ); $\C[2.5in]{// 1}$
forall( T ) f( T p, T i );   $\C{// 2}$
f( 3, 4 ); $\C{// 1}\CRT$
\end{cfa}

\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@.
\begin{cfa}
void f( long int p ); $\C[2.5in]{// 1}$
void f( double p );   $\C{// 2}$
f( 3h ); $\C{// 1, short constant}\CRT$
\end{cfa}

\item \textbf{Variable} cost that counts the number of polymorphic variables, if any, introduced by the @forall@ clause in the function declaration.
Fewer polymorphic variables implies more specificity.
\begin{cfa}
forall( T, T ) f( T p1, T p2 ); $\C[2.5in]{// 1}$
forall( T, U ) f( T p1, U p2 ); $\C{// 2}$
f( 3, 4 ); $\C{// 1}$
f( 3, 4.5 ); $\C{// 2}\CRT$
\end{cfa}

\item \textbf{Specialization} cost counting the number of restrictions introduced by type assertions.
Fewer restriction means fews parametric variables passed at the function call giving better performance.
\begin{cfa}
forall( T | { T ?+?( T, T ) } ) void f( T ); $\C[3.25in]{// 1}$
forall( T | { T ?+?( T, T ), void f( T, T ) } ); $\C{// 2}$
f( 42 ); $\C{// 1}\CRT$
\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.
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;
these design issues are part of this work.

\begin{comment}
From: Richard Bilson <rcbilson@gmail.com>
Date: Tue, 10 Dec 2024 09:54:59 -0500
Subject: Re: cost model
To: "Peter A. Buhr" <pabuhr@fastmail.fm>

I didn't invent it although I may have refined it somewhat. The idea of the
conversion cost is from Glen's thesis, see for instance page 90

On Tue, Dec 10, 2024 at 9:35AM Peter A. Buhr <pabuhr@fastmail.fm> wrote:
> Cforall has a costing model based on an N-tuple using lexicographical ordering.
> (unsafe, polymorphic, safe, variable, specialization)
>
> Did you invent this costing model as a cheap and cheerful way to encode Glen's
> type system?

From: Richard Bilson <rcbilson@gmail.com>
Date: Tue, 10 Dec 2024 17:04:26 -0500
Subject: Re: cost model
To: "Peter A. Buhr" <pabuhr@fastmail.fm>

Yes, I think that's fair to say.

On Tue, Dec 10, 2024 at 2:22PM Peter A. Buhr <pabuhr@fastmail.fm> wrote:
> Found it thanks. But Glen never implemented anything (small examples). So it
> feels like you took his conversion-cost idea and created an implementation table
> with the lexicographical comparison.
\end{comment}

In many languages that support function/method overloading, such as \CC and Java, a partial-order system decides which interpretation of the expression is selected.
Hence, sometimes the candidates are incomparable (none are considered a best match), and only when one candidate is considered better than all others (maximal with respect to the partial order) is the expression unambiguous.
Specifically, the resolution algorithms used in \CC and Java are greedy, selecting the best match for each subexpression without considering the higher-level ones (bottom-up).
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.
\begin{cfa}
@generate a C++ example here@

read more
\end{cfa}

In \CFA, trying to use such a system is problematic because of the presence of return-type overloading of functions and variable.
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.
This situation arises often in \CFA, even in the simple expression @f(x)@, where both the function name @f@ and variable name @x@ are overloaded (examples to follow).

Ada is another programming language that has overloading based on return type.
Ada has no type conversions but has subtyping so subtypes are convertible to supertypes.
There are only two preference rules in Ada overload resolution:
\begin{quote}
There is a preference for the primitive operators (and ranges) of the root numeric types @root_integer@ and @root_real@.
In particular, if two acceptable interpretations of a constituent of a complete context differ only in that one is for a primitive operator (or range) of the type @root_integer@ or @root_real@, and the other is not,
\end{quote}
However, I was unable to generate any Ada example program that demonstrates this preference.
In contrast, the \CFA overload resolution-system is at the other end of the spectrum, as it tries to order every legal interpretations of an expression and chooses the best one according to cost, occasionally giving unexpected results rather than an ambiguity.

Interestingly, the \CFA cost-based model can sometimes make expression resolution too permissive because it always attempts to select the lowest cost option, and only when there are multiple options tied at the lowest cost does it report the expression is ambiguous.
The reason is that there are so many elements in the cost tuple, the type system ``tries too hard to discover a match'', and therefore, ties are uncommon.
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.
\begin{enumerate}[leftmargin=*]
\item Polymorphic exact match versus non-polymorphic inexact match.
\begin{cfa}
forall( T ) void f( T );                $\C[2.5in]{// 1}$
void f( long );                                 $\C{// 2}$
f( 42 );                                                $\C{// currently selects 2}\CRT$
\end{cfa}
Under the current cost model, option 1 incurs a polymorphic cost from matching the argument type @int@ to type variable @T@, and option 2 incurs a safe cost from integer promotion of type @int@ to @long@.
Since polymorphic cost is ranked above safe conversion cost, option 2 is considered to have lower cost and gets selected.

In contrast, the template inferencing and overload resolution rules in \CC selects option 1 (converting @forall@ to the equivalent function template declaration).
\CC performs template argument inferencing and overload candidate ranking in two separate steps.
\begin{itemize}
\item
In the first step, the type parameters are deduced for each primary function template, and if the corresponding template instantiation succeeds, the resulting function prototype is added to the resolution candidate set.
\item
In the second step, the implicit conversions (if any) applied to argument types are compared after taking away top-level qualifiers and references.
It then prefers an exact match, followed by basic type promotions (roughly corresponds to safe conversion in \CFA), and then other kinds of conversions (roughly corresponds to unsafe conversion in \CFA).
Only when the type conversions are the same does it prioritize a non-template candidate.
\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 makes 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@.
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.
We are learning that having the type system consider performance may be inappropriate.

\item
Having a lower total polymorphic cost does not always mean a function is more specialized.
The following example is from Moss's thesis, which discusses some improvements to the \CFA cost-model.
He claims the following function prototypes are increasingly more constrained:
\begin{cfa}
forall( T, U ) void f( T, U );  $\C[2.75in]{// 1 polymorphic}$
forall( T ) void f( T, T );             $\C{// 2 less polymorphic}$
forall( T ) void f( T, int );   $\C{// 3 even less polymorphic}$
forall( T ) void f( T *, int ); $\C{// 4 least polymorphic}\CRT$
\end{cfa}
This argument is not entirely correct.
Although it is true that both the sequence 1, 2 and 1, 3, 4 are increasingly more constrained on the argument types, option 2 is not comparable to either of option 3 or 4;
they actually describe independent constraints on the two arguments.
Specifically, option 2 says the two arguments must have the same type, while option 3 states the second argument must have type @int@, 
Because two constraints can independently be satisfied, neither should be considered a better match when trying to resolve a call to @f@ with argument types @(int, int)@;
reporting such an expression as ambiguous is more appropriate.
The example illustrates the limitation of using a numerical cost value as it cannot represent these complicated cases.
\item
A generic type can require more type variables to describe a more specific type.
For example, consider a generic function taking a @pair@-type requires two type variables.
\begin{cfa}
forall( T, U ) void f( pair( T, U ) ); $\C[2.75in]{// 1}$
\end{cfa}
Add a function taking any type.
\begin{cfa}
forall( T ) void f( T );                $\C{// 2}\CRT$
\end{cfa}
Passing a @pair@ variable to @f@
\begin{cfa}
pair 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.
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 currently \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.
Using this observation, it is reasonable to have an ordering that compares the argument/parameter conversion costs first and uses the partial ordering of specializations as a tiebreaker.
Hence, the \CC template-specialization ordering can be applied to \CFA with a slight modification.

In the meantime, some other improvements have been made to the expression cost system.
Most notably, the expression resolution algorithm now consistently uses the globally minimal cost interpretation, as discussed in a previous technical report.
While implementing the change, there are also two detailed issues that need to be addressed for the new rules to fully work.

The first deals with a common idiom in \CFA that creates many overloads with equal cost.
Many C library functions have multiple versions for different argument types.
For example, the absolute-value function is defined for basic arithmetic types with different names, since C does not support overloading.
\begin{cquote}
\begin{tabular}{@{}lll@{}}
\begin{cfa}
int abs( int );
long labs( long );
long long int llabs( long long int );
\end{cfa}
&
\begin{cfa}
double fabs( double );
float fabsf( float );
long double fabsl( long double );
\end{cfa}
&
\begin{cfa}
cabs, cabsf, $and$ cabsl
$for$ _Complex

\end{cfa}
\end{tabular}
\end{cquote}
It is cumbersome for programmers to remember these function names and select the correct one.
If an incorrect version is picked, the program compiles but with potential negative consequences such as using an integral version with a floating-point argument.
In \CFA, these functions are wrapped by functions with the overloaded name @abs@, which results in multiple overloads with the same total cost when some conversion is needed.
For example, @long x = abs( 42 )@ resolves to @long abs( long )@ with @int@ argument 42 converted to @long@ or @int abs( int )@ converting the result to @long@.
In this example, the choice could be arbitrary because both yield identical results.
However, for @int i = abs( -9223372036854775807LL )@, the result is @-1@ due to the narrowing conversion from @long@ to @int@ on the assignment, suggesting at warning to the programmer to reconsider the type of @i@ or the compiler generates an error as the argument is too large for an @int@ parameter.
The \CFA system library has multiple overload groupings of C functions into a single name, so usage should not report an ambiguity or warning unless there is a significant chance of error.

While testing the effects of the updated cost rule, the following example was found in the \CFA standard library.
\begin{cfa}
static inline double __to_readyQ_avg( unsigned long long intsc ) {
        if ( unlikely( 0 == intsc ) ) return 0.0; 
        else return log2( @intsc@ ); // implicit conversion happens here
}
\end{cfa}
This helper function is used for performance logging as part of computing a geometric mean;
it is called during summing of logarithmic values.
However, the function name @log2@ is overloaded in \CFA for both integer and floating point types.
In this case, the integer overload returns an integral result, truncating any small fractional part of the logarithm, so the sum is slightly incorrect.
When experimenting with the updated cost rules, it flagged the @log2@ call as an ambiguous expression.
When asked, the developer expected the floating-point overload because of return-type overloading.
This mistake went unnoticed because the truncated component was insignificant in the performance logging.
To correct this mistake, I changed the resolution algorithm to favour a lower conversion cost up the expression tree when the total global cost is equal.

Another change addresses the issue that C arithmetic expressions have unique meanings governed by its arithmetic conversion rules.
From the C language reference manual:
\begin{enumerate}[leftmargin=*,topsep=5pt,itemsep=4pt]
\item
First, if the corresponding real type of either operand is @long double@, the other operand is converted, without change of type domain, to a type whose corresponding real type is @long double@.
\item
Otherwise, if the corresponding real type of either operand is @double@, the other operand is converted, without change of type domain, to a type whose corresponding real type is @double@.
\item
Otherwise, if the corresponding real type of either operand is @float@, the other operand is converted, without change of type domain, to a type whose corresponding real type is @float@.\footnote{
For example, addition of a \lstinline{double _Complex} and a \lstinline{float} entails just the conversion of the \lstinline{float} operand to \lstinline{double} (and yields a \lstinline{double _Complex} result).}
\item
Otherwise, the integer promotions are performed on both operands.
Then the following rules are applied to the promoted operands:
\begin{enumerate}[topsep=5pt,itemsep=4pt]
\item
If both operands have the same type, then no further conversion is needed.
\item
Otherwise, if both operands have signed integer types or both have unsigned integer types, the operand with the type of lesser integer conversion rank is converted to the type of the operand with greater rank.
\item
\label{p:SignedToUnsignedSafe}
Otherwise, if the operand that has unsigned integer type has rank greater or equal to the rank of the type of the other operand, then the operand with signed integer type is converted to the type of the operand with unsigned integer type.
\item
\label{p:UnsignedToSignedUnsafe}
Otherwise, if the type of the operand with signed integer type can represent all of the values of the type of the operand with unsigned integer type, then the operand with unsigned integer type is converted to the type of the operand with signed integer type.
\item
\label{p:Miscellaneous}
Otherwise, both operands are converted to the unsigned integer type corresponding to the type of the operand with signed integer type.

\hfill\cite[\S~6.3.1.8]{C11}
\end{enumerate}
\end{enumerate}
\VRef[Figure]{f:CExpressionConversions} shows the C arithmetic conversions graphically.
\VRef[Rule]{p:SignedToUnsignedSafe} says an unsigned type is safely convertible to an signed type with greater rank, while \VRef[rule]{p:UnsignedToSignedUnsafe} says a signed type is unsafely convertible to an unsigned type.
Therefore, these two rules cover every possible case.
\VRef[Rule]{p:Miscellaneous} is the odd-ball rule because it is really a demotion because signed to unsigned (marked in red) is unsafe.
Finally, assignment allows demotion of any larger type into a smaller type, with a possibly lossy conversion (and often no warning).
These promotion conversions are applied greedily at local points within an expression.
Because there is no overloading in C, except for builtin operators, no cost model is needed to differentiate among alternatives that could result in ambiguous matches.

\begin{figure}
\input{C_expression_conversion.pstex_t}
\caption{C Expression Conversions: T1 operator T2}
\label{f:CExpressionConversions}

\smallskip
\input{CFA_curr_arithmetic_conversion.pstex_t}
\caption{\CFA Total-Ordering Expression Conversions}
\label{f:CFACurrArithmeticConversions}

\smallskip
\input{CFA_arithmetic_conversion.pstex_t}
\caption{\CFA Partial-Ordering Expression Conversions}
\label{f:CFAArithmeticConversions}
\end{figure}

\VRef[Figure]{f:CFACurrArithmeticConversions} shows the current \CFA total-order arithmetic-conversions graphically.
Here, the unsafe cost of signed to unsigned is factored into the ranking, so the safe conversion is selected over an unsafe one.
Furthermore, an integral option is taken before considering a floating option.
This model locally matches the C approach, but provides an ordering when there are many overloaded alternative.
However, as Moss pointed out overload resolution by total cost has problems, \eg handling cast expressions.
\begin{cquote}
\ldots if a cast argument has an unambiguous interpretation as a conversion argument then it must be interpreted as such, even if the ascription interpretation would have a lower overall cost.
This is demonstrated in the following example, adapted from the C standard library:
\begin{cfa}
unsigned long long x;
(unsigned)( x >> 32 );
\end{cfa}
\vspace{5pt}
In C semantics, this example is unambiguously upcasting 32 to @unsigned long long@, performing the shift, then downcasting the result to @unsigned@, at cost (1, 0, 3, 1, 0, 0, 0).
If ascription were allowed to be a first-class interpretation of a cast expression, it would be cheaper to select the @unsigned@ interpretation of @?>>?@ by downcasting @x@ to @unsigned@ and upcasting 32 to @unsigned@, at a total cost of (1, 0, 1, 1, 0, 0, 0).
\PAB{[Note, this alternate interpretation is semantically incorrect, because the downcasting \lstinline{x} to from \lstinline{long long} to \lstinline{unsigned} is unsafe (truncation).]}
However, this break from C semantics is not backwards compatible, so to maintain C compatibility, the \CFA resolver selects the lowest-cost interpretation of the cast argument for which a conversion or coercion to the target type exists (upcasting to @unsigned long long@ in the example above, due to the lack of unsafe downcasts), using the cost of the conversion itself only as a tie-breaker.~\cite[pp.~46-47]{Moss19}
\end{cquote}
However, a cast expression is unnecessary to have such inconsistency to C semantics.
An implicit argument-parameter type conversion in a function calls can replicate this issue without an explicit cast.
\begin{cfa}
        unsigned long long x;
        void f( unsigned );
f( x >> 32 );
\end{cfa}
The argument generation has the same effect as using an explicit cast to coerce the type of expression @x >> 32@ to @unsigned@.
This example shows the problem is not coming from the cast expressions, but from modelling the C builtin operators as overloaded functions.
As a result, a different rule is used to select the builtin function candidates to fix this problem:
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 an 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.
This approach reduces the search space by partitioning into two categories.


\section{Type Unification}

Type unification is the algorithm that assigns values to each (free) type parameters such that the types of the provided arguments and function parameters match.

\CFA does not attempt to do any type \textit{inference} \see{\VRef{s:IntoTypeInferencing}}: it has no anonymous functions (\ie lambdas, commonly found in functional programming and also used in \CC and Java), and the variable types must all be explicitly defined (no auto typing).
This restriction makes the unification problem more tractable in \CFA, as the argument types at each call site are usually all specified.
There is a single exception case when the function return type contains a free type variable that does not occur in any of the argument types, and subsequently passed into the parent expression.
One such example is the \CFA wrapper for @malloc@ which also infers size argument from the inferred return type.
\begin{cfa}
forall( T * ) T * malloc() {
        return ( T *)malloc( sizeof(T) ); // calls C malloc with the size inferred from context
}
int * i = malloc();   // infer int for T from LHS
\end{cfa}
A top level expression whose type still contains an unbounded type variable is considered ill-formed as such an expression is inherently ambiguous.

The unification algorithm in \CFA is originally presented in Richard Bilson's thesis and it has remained as the basis of the algorithm currently in use.
Some additions have been made in order to accommodate for the newly added type features to the language.
To summarize, the \CFA type unification has two minor variants: an \textit{exact} mode and an \textit{inexact} mode.
The exact mode is required since the type matching algorithm operates recursively and the inner types often have to match exactly, \eg there is no common type for the pointer types @int *@ and @long *@ while there is for @int@ and @long@.
The inexact mode is applied at top level argument-parameter matching, and attempts to find an assignment to the type variables such that the argument types can be converted to parameter types with minimal cost as defined in the previous section.
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.

One simplification was made 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 
\begin{cfa}
void f( forall( T | { T -?( T ); } ) T (@*p@)( T, T ) );
\end{cfa}
Notably, the unification algorithm implemented in the \CFA compiler has never managed to trace the assertion parameters on the formal types at all, and the problem of determining if two assertion sets are compatible is likely undecidable in general, given the ability of synthesizing more complicated types by the nesting of generics.
Essentially, the reason for disallowing this construct is that it does not provide a useful type feature.
A function operates on the call-site arguments together with any local and global variables.
When the function is polymorphic, the types are inferred at each call site.
On each invocation, the types to be operate on are determined from the arguments provided, and therefore, there is no need to pass a polymorphic function pointer, which can take any type in principle.
For example, consider a polymorphic function that takes one argument of type @T@ and polymorphic function pointer.
\begin{cfa}
forall( T ) void f( T x, forall( U ) void (* g)( U ) );
\end{cfa}
Making @g@ polymorphic in this context is almost certainly unnecessary, since it can only be called inside the body of @f@ and the types of the argument must be known, although it can potentially depend on @T@.
Moreover, requesting a function parameter to be able to work on any input type would impose too much constraint on the arguments, as it only needs to make each call inside the body of @f@ valid.

Hence, rewriting the prototype (or potentially, some compound type synthesized from @T@):
\begin{cfa}
forall( T ) void f( T x, void (* g)( T ) );
\end{cfa}
is sufficient, so @g@ is no longer a polymorphic type itself.
This \emph{monomorphization} conversion is readily supported in \CFA, either by explicitly assigning a polymorphic function name to a compatible function pointer type, or implicitly done in inferring assertion parameters (which is discussed next).
This technique is applicable to argument passing, which is just an assignment to a function parameter variable.
In theory, there might be edge cases where the supplied function @g@ is called on arguments of different types inside the body of @f@ and so needs to be polymorphic, but this case is rare and its benefit seems to be minimal in practice.

The result of this change is that the unification algorithm no longer needs to distinguish open (unbounded) and closed (bounded) type-variables, as the latter is not allowed to exist.
The only type variables that need to be handled are those introduced by the @forall@ clause from the function prototype.
The subtype relationship among function types is now also rendered redundant since none of the function parameter or return types can be polymorphic, and no basic types or non-polymorphic function types are subtypes of any other type.
Therefore, the goal of (exact) type unification becomes finding a substitution that produces identical types.
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.

An 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.
However, to handle type conversions, the type environment needs to keep track of which type variables can be converted.
This behaviour is notably different from \CC template argument inferencing that enforces an exact match everywhere unless the template argument types are explicitly given.
For example, a polymorphic maximum function in \CFA can be called with arguments of different arithmetic types and the result follows the usual arithmetic conversion rules.
\begin{cfa}
forall( T | {int ?<? ( T, T ); } ) T max ( T, T );
max( 42, 3.14 );   $\C[2.5in]{\LstCommentStyle // \CFA implicitly infers T == double}$
max<double>(42, 3.14); $\C{\LstCommentStyle // \CC requires explicit type specification}\CRT$
\end{cfa}
From a theoretical standpoint, the simplified implementation of the type environment has its shortcomings.
Some cases do not work nicely with this implementation, and hence, some compromise has to be made.
A more detailed discussion follows in \VRef{s:CompilerImplementationConsiderations}.


\section{Assertion Satisfaction}
\label{s:AssertionSatisfaction}

The assertion-satisfaction problem greatly increases the complexity of \CFA expression resolution.
Past experiments have shown that the majority of compilation time is spent in resolving the assertions for those expressions that takes the longest time to resolve.
Even though a few heuristics-based optimizations have been introduced to the compiler, this remains the most costly part of a \CFA compilation.
The major difficulty of resolving assertions is that the problem can become recursive, since the expression used to satisfy an outstanding assertion can have its own assertions, and in theory this can go on indefinitely.
Detecting infinite recursion cases in general is not algorithmically possible and it is not attempted in the compiler.
Instead, a fixed maximum depth of recursive assertions is imposed.
This approach is also taken by \CC compilers as template argument inferencing is also similarly undecidable in general.


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.
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.
In fact, some of my performance optimizations come from analyzing these problematic cases.
One example is analysed in this section.

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.
A naive algorithm that simply picks any pending assertion to resolve and continue in a depth-first search could be very inefficient and especially prone to an infinite loop.
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-simulator that capture most of \CFA 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.
To resolve a set of assertions, the algorithm first attempts to resolve each assertion item individually.
There are three possible outcomes on resolving each assertion:
\begin{enumerate}
\item If no matches are found, the algorithm terminates with a failure (ambiguity).
\item If exactly one match is found, the type environment is updated immediately with this result, affecting the resolution of remaining assertions.
\item If multiple matches are found, the assertion candidates with their updated type environments are stored in a list that is checked for compatibility at the end.
\end{enumerate}
When all assertion items are resolved successfully, the algorithm attempts to combine the ambiguously resolved assertions to produce mutually compatible assignments.
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, 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}
forall( @T@ | { void foo( @T@ ), void bar( @T@ ) } ) T f( T );
void foo( int );
void bar( int );   void bar( double );   ...
f( 3 );
\end{cfa}
where one can be uniquely resolved and allow the type @T@ to be inferred immediately, and another has many ways to be resolved, each resulting in @T@ being bound to a different concrete type.
If the first assertion is examined by the algorithm, the inferred type can then be utilized in resolving the second assertion eliminating many incorrect options without producing a list of candidates requiring further checks.
In practice, this have a significant impact when an unbound type @T@ is declared to satisfy the basic \emph{object assertions}\footnote{The term is borrowed from object-oriented languages although \CFA is not object-oriented.} of having a default constructor, destructor, and copy assignment operations.
Since these functions are implicitly defined for almost every type in scope, there can be hundreds or even thousands of matches to these functions with an unspecified operand type.
In most cases, the value of @T@ can be inferred by resolving other assertions first, and then the object lifetime-functions can easily be fulfilled since functions are sorted internally by the operand type;
because of its size, this optimization greatly reduces the number of wasted resolution attempts.

This issue also limits the capability of the assertion resolution algorithm.
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.
However, loosening the assertion matching requirement causes many assertion variables to have multiple matches and makes the delayed combination step too costly.

Given all the issues caused by assertion resolution creating new type variable bindings, a natural progression is to restrict free type-variables such that all the type variables are bound when the expression reaches the assertion resolution stage.
A type variable introduced by the @forall@ clause of function declaration can appear in parameter types, return types and assertion variables.
If it appears in parameter types, it can be bound when matching the arguments to parameters at the call site.
If it only appears in the return type, it can be eventually be determined from the call-site context.
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).
\begin{cfa}
forall( T | { void foo( @T@ ) } ) int f( float ) {
        @T@ t;
}
\end{cfa}
This case is rare so forcing every type variable to appear at least once in parameter or return types limits 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}.


\subsection{Caching Assertion Resolution Results}

In Aaron Moss's prototype design and experiments, a potential optimization of caching the result of already resolved assertions is discussed.
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.

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.

The original design of \CFA includes unrestricted polymorphic formal parameters with assertions on themselves, making the problem more complicated as new declarations can be introduced in scope during expression resolution.
Here is an example taken from Bilson:
\begin{cfa}
void f( forall( T | { T -?( T ); } ) T (*p)( T, T ) );
forall( U, V | { U -?( U ); V -?( V ); } )  U @g@( U, V ) );
f( @g@ );
\end{cfa}
The inner assertion parameter on the \emph{closed} type-variable @T@ is used to satisfy the assertions on @U@ and @V@ in this example.

However, as per the previous discussions on this topic, polymorphic function-pointer types have been removed from \CFA, since correctly implementing assertion matching is impossible in general.
Without closed parameters (and therefore no have-set for assertions) the set of declarations in scope remains unchanged, while resolving an expression.
The current \CFA implementation also does not attempt to widen any bound type-parameters to satisfy an assertion.
Note, this restriction does mean certain kinds of expressions cannot be resolved, \eg:
\begin{cfa}
forall( T | { void f( T ); } )  void g( T );
void f( long );
g( 42 );
\end{cfa}
The call @g(42)@ is rejected since no attempt is made to widen the parameter type @T@ from @int@ to @long@.
Such problem could be mitigated by allowing inexact matches of assertions, but cannot be eliminated completely, if @T@ is matched in a parameterized type, including pointers and references:
\begin{cfa}
forall( T | {void f( T*);})  void g( T );
void f( long * );
g( 42 );
\end{cfa}
Here the only way to resolve the call @g(42)@ is to allow assertion resolution to widen the parameter @T@, but even with inexact matching, @int *@ cannot be converted to @long *@.


\section{Compiler Implementation Considerations}
\label{s:CompilerImplementationConsiderations}

\CFA is still an experimental language and there is no formal specification of expression resolution rules yet. 
Currently, there is only one reference implementation, namely the @cfa-cc@ translator, which is under active development and the specific behaviour of the implementation can change frequently as new features are added.
(This situation is standard for any new programming language.)

Ideally, the goal of expression resolution involving polymorphic functions is to find the set of type variable assignments such that the global conversion cost is minimal and all assertion variables can be satisfied. 
Unfortunately, there are a lot of complications involving implicit conversions and assertion variables;
hence, fully achieving this goal is unrealistic.
And as noted, the \CFA compiler is not covering all the edge cases for its current type-system design.
Instead it makes a few restrictions to simplify the resolution algorithm so most expressions in actual code still pass type checking within a reasonable amount of time.

As previously mentioned, \CFA polymorphic type resolution is based on a modified version of a unification algorithm, where both equivalence (exact) and subtyping (inexact) relations are considered.
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, this means 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}
        \item
        Type resolution almost exclusively proceeds in bottom-up order, which naturally produces lower bound constraints.
        Since all identifiers can be overloaded in \CFA, little information can be gained from top-down analysis.
        In principle, it is possible to detect non-overloaded function names and perform top-down resolution for those;
        however, Moss' prototype experiments showed this optimization does not give a meaningful performance benefit, and therefore was not implemented. 
        \item
        Few nontrivial subtyping relationships are present in \CFA, \eg the arithmetic types presented in \VRef[Figure]{f:CFACurrArithmeticConversions} and qualified pointer/reference types.
        The reason is that \CFA lacks nominal inheritance subtyping present in object-oriented languages, and the generic types do not support covariance on type parameters.
        As a result, named types such as structures are always matched by strict equivalence, even when type parameters exist.
        \item
        Unlike functional programming where subtyping between arrow types exists, \ie if $T_2 <: T_1$ and $U_1 <: U_2$ then $T_1 \rightarrow T_2 <: U_1 \rightarrow U_2$, \CFA uses C function pointer types and the parameter/return types must match exactly to be compatible.
\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.
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.
The following is an annotated example of the workaround.
\begin{cfa}
// If resolution is unsuccessful with a target type, try again without, since it sometimes succeeds
// when it does not with a target type binding. For example:
forall( T ) T & ?[]( T *, ptrdiff_t );
const char * x = "hello world";
int ch = x[0];
// * T is bound to int
// * (x: const char *) is unified with int *, which fails
\end{cfa}
The problem is that the type system can only represent the constraints $T = int$ and $int <: T$, but since the type information flows in the opposite direction, the proper constraint for this case is $T <: int$, which cannot be represented in the simplified type environment. Currently, an attempt to resolve with equality constraint generated from the initialized variable is still made, since it is often the correct type binding (especially in the case where the initialized variable is a structure), and when such attempt fails, the resolution algorithm is rerun without the initialization context.

One additional remark to make here is that \CFA does not provide a mechanism to explicitly specify values for polymorphic type parameters. In \CC for example, users may specify template arguments in angle brackets, which is necessary when automatic inferencing fails, \eg @max<double>(42, 3.14)@. 
There are some partial workarounds such as adding casts to the arguments, but they are not guaranteed to work in all cases.
If a type parameter appears in the function return type, however, using an ascription (return) cast
\begin{cfa}
(@return@ double (*)( double, double ))max( 42, 3.14 );   $\C[2.5in]{// tell resolver what type to use}\CRT$
\end{cfa}
forces the desired type binding, since the cast only compiles when the expression type matches exactly with the target.

\section{Related Work}

\CFA expression resolution may deal with extensive overloading and inference of polymorphic types with assertions, and we want to keep the base algorithm used in type unification simple enough so that resolving a complicated expression can still be done reasonably fast.
In this section, we look at some related work that handles the aforementioned bidirectional subtyping relations concisely.

Melo, et. al.~\cite{Melo17} developed PsycheC, a tool built for inferencing missing type and variable declarations of incomplete C programs, which can also be viewed as a dialect of C with type inferencing. As PsycheC is built for analyzing standard C programs, it does not have any kind of overloading or polymorphism. Instead, all top-level variables and function parameters may have indeterminate types. The scope of the problem PsycheC deals with is quite the opposite of that in \CFA, but the techniques used to solve for the unknown types are similar. 
In PsycheC, a unification variable is assigned to every identifier with unknown type, and each use of a variable generates a constraint on its type. Just like in \CFA, the most common kinds of expression contexts PsycheC deals with are assignments and function calls, which creates inequality constraints: the right hand side of the assignment is a subtype of the left hand side; function argument passing is treated the same as assignment. Since both sides of the inequality can have unknown types, type resolution needs to handle both upper bound and lower bound constraints. 
Instead of directly solving with lower and upper bounds, the authors developed a two-phase unification algorithm where the equivalences are first resolved and substituted into the inequalities, and showed that by ordering the inequalities using the partial order of concrete types involved, a second pass of unification treating inequalities as equivalences will be sufficient to resolve all type variables.
Note that, however, PsycheC does not consider the hierarchy of arithmetic types, as they are all mutually convertible in C and therefore considered "equivalent" in unification, and it also lacks structured types except simple pointers, meaning this strategy of unifying subtypes as equivalences will not work in a more general setting such as in \CFA. 

Pierce and Turner~\cite{Pierce00} presented a \textit{local} type inference method that restricts the propagation of types and use of unification variables within adjacent syntax tree nodes. The technique is developed to provide sufficient type checking and inference in the ML family of languages. Odersky, Zenger and Zenger~\cite{Odersky01} refined their method by introducing a colored type system which distinguishes inherited types (given directly by context) and synthesized types (deducted from the term itself), to handle bidirectional type propagation in a more concise manner. 
Their algorithms are designed for functional programming, where first-class (untyped) lambda expressions are common and type inference must also deduce the argument types of lambdas, and hence bidirectional inference must be supported. 
Given that \CFA does not have lambda expressions, and the rest of type inference cases are quite similar, implementing this type inference algorithm for \CFA expression resolution might be promising. Moreover, the current \CFA implementation also keeps unification variables \textit{almost} local, with the exception that whenever a type variable does not appear in the parameter list and therefore cannot be given a value by the argument types, it is passed upwards as a free variable. In all other cases, the substituted minimal types are passed upwards as the result types. This means that the current implementation of \CFA expression resolution semantically agrees with Pierce's type inference system in most of the cases. A question remains whether these methods can be adapted to handle \CFA assertion resolution.