% -*- Mode: LaTeX -*-

\section{Compiling for Type Reconstruction}
\label{compile}

The basic insight of this paper is that the problem of information
propagation from closure creation sites to their call sites for
non-type-conserving functions may be formulated as an {\em overloading
resolution} problem which is then handled using well-known techniques
in the literature \cite{Gupta90,Haskell,Wadler89}. These techniques
systematically translate overloading into parametric polymorphism by
replacing unresolved instances of overloaded variables in a function
with explicit parameters that are supplied at its call site. In our
scheme, these parameters are the explicit type-hints that are used by
the type reconstruction algorithm rather than the function itself.

We will not discuss the overloading resolution schemes here; the
reader is referred to \cite{Gupta90,Wadler89} for a detailed
description. Instead, we will show how to formulate
our problem in terms of overloading \via examples and 
describe the exact nature of the type-hints.

\subsection{Detecting Violations of Type-Conservation}
\label{hint-detect}
The first step in our compilation process is to identify the functions
in the program that may require additional type-hints. First, we
type-check each function and generate its type-map according to
definition~\ref{type-map}. Then, using this information we determine
which type-variables, if any, in its type-map are not being conserved
according to definition~\ref{conserve}. For example, the type-map for
function {\tt h3} from Example~\ref{ex3} is shown below:
\begin{center}
\begin{tabular}{|l|l|}
\hline
\multicolumn{1}{|c|}{{\sc Function}} & \multicolumn{1}{c|}{{\sc
Defined Type}} \\
\hline\hline
{\tt h3} & $t_{1} \rightarrow (\ibx{list}\;t_{1})$ \\
\hline
\multicolumn{2}{c}{}\\
\hline
\multicolumn{1}{|c|}{{\sc Free Variables}} & \multicolumn{1}{c|}{{\sc
Defined Type-Scheme}} \\
\hline\hline
{\tt x} & $\ibx{list}\;t_{0}$\\
{\tt length} & $\forall{}t_{3}.(\ibx{list}\;t_{3})\rightarrow\ibx{int}$\\
{\tt nil} & $\forall{}t_{4}.(\ibx{list}\;t_{4})$\\
\hline
\multicolumn{2}{c}{}\\
\hline
\multicolumn{1}{|c|}{{\sc Local Variables}} & \multicolumn{1}{c|}{{\sc
Defined Type-Scheme}} \\\hline\hline
{\tt z} & $t_{1}$\\
\hline
\multicolumn{2}{c}{}\\
\hline
\multicolumn{1}{|c|}{{\sc Call Site}} & \multicolumn{1}{c|}{{\sc
Function Type Instance}} \\\hline\hline
{\tt length x} & $(\ibx{list}\;t_{0}) \rightarrow \ibx{int}$ \\
\hline
\end{tabular}
\end{center}
Looking at the type-map above we have,
\begin{eqnarray*}
\mbox{\Proc{Type-Vars}}(\ibx{type-map}) & = & \{t_{0},t_{1}\} \\
\mbox{\Proc{Type-Vars}}(t_{1}\rightarrow(\ibx{list}\;t_{1})) & = & \{t_{1}\}
\end{eqnarray*}
Therefore, the type-variable $t_{0}$ is not being conserved in {\tt h3}. 

\subsection{Reconstruction as Overloading} 
\label{hint-prop} 

The next step is to determine what additional type information is
required to correctly instantiate the non-conserved type-variables of
a function, and how to propagate this information to the function's
dynamic activation. This is accomplished by viewing these
type-variables as unresolved instances of a fictitious overloaded
operation. This allows the standard overloading resolution mechanism
to pick up these type-variables as candidates for information
propagation from external call sites where this information may be
available. We show this process for the function {\tt h3} below:

\begin{myexample}{ex6}
def f3$_{(\sibx{tr?}\:t_{0})}$ x = 
  \{ def h3$_{(\sibx{tr?}\:t_{0})}$ z = if length x == 1
                     then z:nil
                     else z:z:nil;
   in h3$_{(\sibx{tr?}\:t_{0})}$ \};
g3 = if ... 
     then f3$_{(\sibx{tr?}\:\sibx{int})}$ (1:nil)
     else f3$_{(\sibx{tr?}\:\sibx{bool})}$ (true:nil);
\end{myexample}

Here, we have added an {\em overloading predicate}\footnote{We follow
the terminology of \cite{Gupta90,Wadler89} where the usual
Hindley/Milner type of a function is extended with {\em predicates} to
model overloaded variables. In Haskell \cite{Haskell} these are known
as {\em class assertions}. The predicate name \sibx{tr?} in our scheme
stands for {\em type-reconstructible?}.} $(\ibx{tr?}\:t_{0})$ as a
subscript on the function {\tt h3}.  In general, a predicate is added
for every non-conserved type-variable in the function's type-map.
Subsequently, the standard overloading resolution mechanism
automatically propagates this predicate to the place where {\tt h3} is
referenced and to the enclosing lexical function {\tt f3} because it
remains uninstantiated (and hence unresolved) in its body.  Finally,
this predicate propagates to the call sites of {\tt f3} where it is
completely instantiated according to the types of the arguments being
supplied to {\tt f3} and is considered to be resolved.

Intuitively, the propagation of a predicate asssociated with a
function represents a lack of local type information which must be
supplied from the call site where this predicate is instantiated.
Furthermore, the type contained in the instantiated predicate reflects
the types of the objects present at that call site. This is exactly
the information required for type reconstruction by the function that
introduced the predicate. In the next section, we will show a simple
strategy that directly encodes this type information as data objects
and passes them as additional hint arguments to the function.

Note that in the propagation scheme described above, a predicate only
corresponds to a non-conserved type-variable of a function or one of
its lexical children; it does not correspond to the full type of any
of its formal parameters or its free variables as suggested in
\cite{Goldberg91}.  That additional type information is already
present in the function's type-map. Also, predicate instantiations
involving polymorphic type-variables are always considered as resolved
and are not propagated outwards in the light of the discussion in
Section~\ref{free-vars}. For instance, {\tt g3} in the above example
might have been defined as:

\begin{myexample}{ex7}
g3 = if ... 
     then f3$_{(\sibx{tr?}\:(\sibx{list}\:t))}$ (nil:nil)
     else f3$_{(\sibx{tr?}\:\sibx{bool})}$ (true:nil);
\end{myexample}

Here, $(\ibx{tr?}\;(\ibx{list}\;t))$ is an instantiation of {\tt f3}'s
predicate according to its polymorphic argument {\tt (nil:nil)}.  Even
though this predicate has an uninstantiated type-variable $t$, it is
not propagated any further because it is polymorphic at this point. It
follows immediately that there can be no unresolved predicates at the
top-level because there are no free type-variables in the top-level
type environment by construction.

\subsection{Program Translation and Hint Generation} 
\label{hint-gen}

The final step in our compilation process is to add extra hint
parameters to the function definitions that possess unresolved
predicates and generate type-hints at their call sites according to
the instantiations of these predicates. It is possible to either add
one hint parameter for each unresolved predicate or group the hints
together in a single {\em hint-record} from which the individual hints
may be fetched.  Our current scheme adds one hint parameter per
predicate in front of its regular parameters, because in our system,
passing a small number of additional parameters is cheaper than
allocating and fetching from heap data-structures. We record the
mapping between the type-variables present in the unresolved
predicates of a function and its additional hint parameters in a {\em
hint-map} as follows:
\begin{definition}[Hint-map]\label{hint-map}
Given a function with unresolved type-variables
$\alpha_{1},\ldots,\alpha_{n}$, its {\bf hint-map} is the mapping
$\{(\alpha_{1} \mapsto{}x_{1}),\ldots,(\alpha_{n}\mapsto{}x_{n})\}$,
where $x_{1},\ldots,x_{n}$ are its new additional hint parameters.
\end{definition}
For example, the hint-map of {\tt h3} in Example~\ref{ex6} above is
generated as follows:
\begin{center}
\begin{tabular}{|l|l|}
\hline
\multicolumn{1}{|c|}{{\sc Type Variable}} &
\multicolumn{1}{|c|}{{\sc Hint Parameter}}\\\hline\hline
$t_{0}$ & {\tt h3\_hint\_1} \\
\hline
\end{tabular}
\end{center}
A predicate $(\ibx{tr?}\;\tau)$ appearing at a call site within a
function is transformed into a type-hint that is passed as an explicit
argument at that call site.  This type-hint encodes the type $\tau$ 
using the following Id data-type:

\begin{code}
type id\_hint = none | tc string (list id\_hint);
\end{code}

The disjunct {\tt none} is used to encode polymorphic type-variables
that do not require any hint. The disjunct {\tt tc} encodes a
type-constructor by its name and a list of encoded type-parameters.
The free type-variables in $\tau$ are replaced by their corresponding
hint parameters given by the hint-map of the function. 
For instance, the Example~\ref{ex6} above will be translated as
follows:

\begin{myexample}{ex8}
def f3 f3\_hint\_1 x = 
  \{ def h3 h3\_hint\_1 z = if length x == 1
                        then z:nil
                        else z:z:nil;
   in h3 f3\_hint\_1 \};
g3 = if ... 
     then f3 (tc "int" nil) (1:nil)
     else f3 (tc "bool" nil) (true:nil);
\end{myexample}

Notice how the hints generated within {\tt g3} propagate into {\tt h3}
\via the hint parameters of {\tt f3} and {\tt h3}. The appropriate
hint will now be available in a dynamic activation of {\tt h3} where
it may be used along with its type-map to reconstruct the exact
run-time type of {\tt x}. We describe this reconstruction scheme in
the next section in the context of a source debugger for Id. 
