Apr 23, 2019, 3:41:51 PM (5 years ago)
Aaron Moss <a3moss@…>
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

thesis: integrate defence answers as clarifications into thesis

1 edited


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

    rcf01d0b rc4b5486  
    66A 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.
    77To choose among valid interpretations, a \emph{conversion cost} is used to rank interpretations.
     8This conversion cost is summed over all subexpression interpretations in the interpretation of a top-level expression.
    89Hence, the expression resolution problem is to find the unique minimal-cost interpretation for an expression, reporting an error if no such unique interpretation exists.
    299300This approach of filtering out invalid types is unsuited to \CFA{} expression resolution, however, due to the presence of polymorphic functions and implicit conversions.
     302Some other language designs solve the matching problem by forcing a bottom-up order.
     303\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.
     304This 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 which is polymorphic in its return type, and these annotations are often redundant.
     305\CFA{}, by contrast, saves programmers from redundant annotations with its richer inference:
     308forall(dtype T | sized(T)) T* malloc();
     310int* p = malloc(); $\C{// Infers T = int from left-hand side}$
    301313Baker~\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.
    302314This thesis closes that gap in the literature by performing performance comparisons of both top-down and bottom-up expression resolution algorithms, with results reported in Chapter~\ref{expr-chap}.
    372384During the course of checking the assertions of a single top-level expression, the results are cached for each assertion checked.
    373385The search key for this cache is the assertion declaration with its type variables substituted according to the type environment to distinguish satisfaction of the same assertion for different types.
    374 This adjusted assertion declaration is then run through the \CFA{} name-mangling algorithm to produce an equivalent string-type key.
     386This adjusted assertion declaration is then run through the \CFA{} name-mangling algorithm to produce an equivalent string-type key.
     388One superficially-promising optimization which I did not pursue is caching assertion-satisfaction judgements between top-level expressions.
     389This 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.
     390New 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.
     391Furthermore, 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.
     392Given 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.
    376394The 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.
Note: See TracChangeset for help on using the changeset viewer.