% -*- Mode: TeX -*-

\appendix
\section{Optimizations for Algorithm $W_{1}$}
\label{opt-appendix}

\begin{figure}
\begin{tabular}{|p{\hlessm}|}
\hline
\begin{display}
\tbx{Def} W$_2$(TE$_{i-1}$,SE$_{i-1}$,B$_x$) =
\vsp
PHASE I:
    Let $B_x$ be the binding `$x = e_x$'.
    Construct the current call graph $G_i$ using the free identifiers (FId) property.
    $SCC_x^i=\{z_1,\ldots,x,\ldots,z_n\}$ be the current SCC of $x$ in $G_i$.
    \tbx{if} $SCC_x^i\neq\ibx{SE}_{i-1}(x)$ \tbx{then}
        SCC Environment: $\ibx{SE}_i{}=\ibx{SE}_{i-1}\setminus_{SCC_x^i}+\{z_k\mapsto{}SCC_x^i\}$       $\forall{}z_k\in{}SCC_x^i$.
        \tbx{for each} top-level identifier $z_k\in{}SCC_x^i$ \tbx{do}
            Let $e_k$ be the RHS expressions associated with $z_k$.
            SCC Assumptions: $Q_{z_k}=\{y\mapsto{}SCC_x^i\}$       $\forall{}y\in{}(\fn{free}{e_{z_k}}\cap{}SCC_{x}^{i})$.
            Let $\beta_{k1},\ldots,\beta_{kn}$ be new type-variables.
            $\ibx{New-TE}_k^i=\ibx{TE}_{i-1}\setminus_{SCC_x^i}+\{z_1\mapsto\beta_{k1},\ldots,z_n\mapsto\beta_{kn}\}$.
            $W'(\ibx{New-TE}_k^i,e_k)=(S_k^i,\tau_{z_k}^i,A_k^i)$.
            Local Assumptions: $A_k^{\sibx{local}}=\{z_1\mapsto{}S_k^i\beta_{k1},\ldots,z_n\mapsto{}S_k^i\beta_{kn}\}$.
        \tbx{endfor}.
        Local Assumption Environment: 
            $\ibx{AE}_i=\ibx{AE}_{i-1}\setminus_{SCC_x^i}+\{z_k\mapsto{}A_k^{\sibx{local}}\}$                           $\forall{}z_k\in{}SCC_x^i$.
        Local Type Environment: 
            $\ibx{WE}_i=\ibx{WE}_{i-1}\setminus_{SCC_x^i}+\{z_k\mapsto\tau_{z_k}^i\}$                            $\forall{}z_k\in{}SCC_x^i$.
    \tbx{else}
        SCC Assumptions: $Q_{x}=\{y\mapsto{}SCC_x^i\}$            $\forall{}y\in{}(\fn{free}{e_x}\cap{}SCC_{x}^{i})$.
        Let $\beta_1,\ldots,\beta_n$ be new type-variables.
        $\ibx{New-TE}_x^i=\ibx{TE}_{i-1}\setminus_{SCC_x^i}+\{z_1\mapsto\beta_1,\ldots,z_n\mapsto\beta_n\}$.
        $W'(\ibx{New-TE}_x^i,e_x)=(S_x^i,\tau_x^i,A_x^i)$.
\vsp
        Local Assumptions: $A_x^{\sibx{local}}=\{z_1\mapsto{}S_x^i\beta_1,\ldots,z_n\mapsto{}S_x^i\beta_n\}$.
        Local Assumption Environment: $\ibx{AE}_i=\ibx{AE}_{i-1}\setminus_{\{x\}}+\{x\mapsto{}A_x^{\sibx{local}}\}$.
        Local Type Enironment: $\ibx{WE}_i=\ibx{WE}_{i-1}\setminus_{\{x\}}+\{x\mapsto\tau_x^i\}$.
    \tbx{endif}.
\vsp
\end{display} \\
\hline
\end{tabular}
\caption{PHASE I of the Updated Incremental Algorithm $W_2$.}
\label{fig:algo-w2-1}
\end{figure}


\begin{figure}
\begin{tabular}{|p{\hlessm}|}
\hline
\begin{display}
PHASE II:
\end{display} \\
\hspace*{1.25em}$U_i=\ibx{Unify-Columns}\left(\begin{array}{ccccc}
                \ibx{AE}_i(z_1)(z_1) & \cdots & \ibx{AE}_i(z_1)(z_k) & \cdots & \ibx{AE}_i(z_1)(z_n) \\
                         \vdots   &        &     \vdots        &        &     \vdots        \\
                \ibx{AE}_i(z_n)(z_1) & \cdots & \ibx{AE}_i(z_n)(z_k) & \cdots & \ibx{AE}_i(z_n)(z_n) \\
                \ibx{WE}_i(z_1)      & \cdots & \ibx{WE}_i(z_k)      & \cdots & \ibx{WE}_i(z_n)      
                            \end{array}\right)$ \\
\vspace*{-.2in}
\begin{display}
    Type Environment: 
        $\ibx{TE}_i=\ibx{TE}_{i-1}\setminus_{SCC_x^i}+\{z_k\mapsto\fn{close}{U_i\ibx{WE}_i(z_k)}\}$               $\forall{}z_k\in{}SCC_x^i$.
    \tbx{if} only $x$ was type-checked in PHASE I \tbx{then}
        Upper Bound Type Assumptions: $M_x=U_i{}A_x^i\setminus_{SCC_x^i}$.
        Lower Bound Type Assumptions: 
            $N_x=\{y\mapsto\ibx{TE}_{i-1}(y)\}$                            $\forall{}y\in{}(\fn{free}{e_x}-SCC_x^i)$.
    \tbx{else}
        Upper Bound Type Assumptions: $M_{z_k}=U_i{}A_k^i\setminus_{SCC_x^i}$          $\forall{}z_k\in{}SCC_x^i$.
        Lower Bound Type Assumptions: 
            $N_{z_k}=\{y\mapsto\ibx{TE}_{i-1}(y)\}$           $\forall{}y\in{}(\fn{free}{e_k}-SCC_x^i)$, $\forall{}z_k\in{}SCC_x^i$.
    \tbx{endif}.
  \tbx{Return} $(\ibx{TE}_i,\ibx{SE}_i)$.
\end{display} \\
\hline
\end{tabular}
\caption{PHASE II of the Updated Incremental Algorithm $W_2$.}
\label{fig:algo-w2-2}
\end{figure}

As mentioned in section~\ref{optimize}, we can optimize the algorithm
$W_1$ by saving the type instances used by each top-level identifier
and using them later while typing other top-level identifiers from the
same SCC. Essentially, we need to save all the type information
necessary to reproduce the unification matrix in the latter half of
algorithm $W_1$ (see \fig{algo-w1}). We will use our incremental
property maintenence system to record this information as compilation
properties of the corresponding top-level identifiers. Note that these
properties are ``local'', \ie, they are independently computed for
each identifier in a SCC and do not use any information about other
identifiers from the same SCC. Therefore, we do not need to maintain
any assumption checks for them. We maintain the following two local
properties.
\begin{description}
\item[Local property] -- $\ibx{Local Type} = (\bx{Types},=)$. 
 For each identifier $x$, we record its local type
$\tau_x^i$ computed in the invocation of $W'$. We save this property in a
map from identifiers to types called Local-Type-Environment \ibx{WE}.

\item[Local property] -- $\ibx{Local Assumptions}=(\bx{Local-Type-Environments},=)$. 
For each identifier $x$, its local assumption set $A_x^{\sibx{local}}$
is a map from the identifiers in its SCC to their types as inferred
from the invocation of $W'$. We collect this property in
Local-Assumption-Environment \ibx{AE}.
\end{description}

The updated algorithm $W_2$ appears in Figures~\ref{fig:algo-w2-1} and
\ref{fig:algo-w2-2}, where we have also incorporated the collection of the
SCC and the lower bound type assumptions introduced in
section~\ref{extensions}. The algorithm now operates in two phases.

The first phase computes the SCC of the given definition and compares
it with its earlier value. If the SCC has changed then we proceed as
before, compiling each of the definitions belonging to the new SCC
afresh and accumulating their properties. We also record the locally
inferred type of each identifier and its local type assumptions about
the other identifiers in its SCC for future use.  If the SCC has not
changed from its earlier value, then it implies that only the current
binding needs to be compiled and we can use previously saved local
properties of the other identifiers of that SCC in the second phase,
instead of computing all of them afresh. 

The second phase, as before, constructs a unification matrix using
the freshly computed or previously saved local properties of all the
identifiers of the SCC and updates their type properties. It also
records the upper and the lower bound type assumptions for the
identifiers compiled in the first phase. 
