%%% Alejandro Caro
%%% Implementation Section, FPCA Paper.
%%%

\section{Type Reconstruction in the Id Debugger}
\label{reconstruct}

The problem of type reconstruction from the perspective of the Id
Debugger~\cite{Caro93} is broad and simple: reconstruct the type of
every object in an activation frame. Once the type of an
object is known, the debugger can invoke a graphical browser
specialized for that particular type should the user wish to inspect
the object.

The debugger utilizes both compile-time and run-time information for
type reconstruction. The compile-time information consists of the
type-map (definition~\ref{type-map}) and the hint-map
(definition~\ref{hint-map}) of a function that are stored in the
symbol table entry for that function. The run-time information
consists of the activation tree that is built dynamically, as the
program executes, by the procedure linkage code.  When the machine is
halted, the debugger can inspect the activation frame of a function
and extract a pointer to its caller (its parent in the activation
tree) and pointers to its callees (its children in the activation
tree). Access to the activation tree is crucial since it permits
correct instantiation of the type-variables that are conserved in a
function's type-map, according to the call site information in
its caller's type-map. Finally, as described in the previous section,
the additional compiler-generated type-hints for the non-conserved
type-variables in a function's type-map are also available from its
activation frame.

\subsection{The Type Reconstruction Algorithm}

\begin{figure}[t]\centering
{\em \codebox{%
\Proc{Reconstruct-Type}(activation)\\
\li activation-fn $\gets$ \Proc{Activation-Fn}(activation)\\ \label{rt:start}
    \Comment {\em Copy the function's type-map.}\\
\li type-map $\gets$ \Proc{Type-Map}(activation-fn)\\  \label{rt:type-map-begin}
\li $\{\alpha_{1},\ldots,\alpha_{n}\} \gets$ \Proc{Type-Vars}(type-map)\\
\li $S_{\sibx{copy}} \gets \{\alpha_{i}\mapsto\beta_{i}\}$ 
{\em where} $\beta_{1},\ldots,\beta_{n}$ {\em are new.}\\ \label{rt:type-map-end}
    \Comment {\em Process the type-hints.}\\
\li hint-map $\gets$ \Proc{Hint-Map}(activation-fn)\\ \label{rt:unify-hints-begin}
\li $S_{\sibx{hint}} \gets$ \{ \Forall $(\alpha\mapsto{}x)$ \In hint-map \\ 
\li \>\>\>$\tau \gets$ \Proc{Interpret-Type-Hint}($x$, activation)\\
\li \>\>\>\Collect $(S_{\sibx{copy}}\alpha \mapsto \tau)$\}\\ \label{rt:unify-hints-end}
    \Comment {\em Return if the type-map is fully instantiated.}\\
\li \If \Proc{Type-Vars}($S_{\sibx{hint}}S_{\sibx{copy}}$(type-map)) $=\phi$\\ \label{rt:test-done}
\li \Then\>\>\hspace{-2em}\Return $S_{\sibx{hint}}S_{\sibx{copy}}$(type-map)\\ \label{rt:end1}
    \Comment {\em Obtain call site information from the caller.}\\
\li \Else \\
\li \> parent-activation $\gets$ \\
\li \>\>\Proc{Parent-Activation}(activation)\\ \label{rt:unify-parent-begin}
\li \>parent-type-map $\gets$ \\
\li \>\> \Proc{Reconstruct-Type}(parent-activation)\\
\li \>$\tau_{\sibx{use}} \gets$ \Proc{Use-Type}(activation, parent-type-map)\\
\li \>$\tau_{\sibx{def}} \gets$ \Proc{Def-Type}(activation-fn, $S_{\sibx{copy}}$(type-map))\\
\li \>$S_{\sibx{def-use}} \gets $\Proc{Unify-Aligned}($\tau_{\sibx{def}}$,
$\tau_{\sibx{use}}$)\\ \label{rt:unify-parent-end}
\li \>\Return $S_{\sibx{def-use}}S_{\sibx{hint}}S_{\sibx{copy}}$(type-map) \label{rt:end2}
}}
\caption{The Type Reconstruction Algorithm}
\label{fig:reconst-type-alg}
\end{figure}

\fig{reconst-type-alg} shows the pseudo-code for the reconstruction
algorithm \Proc{Reconstruct-Type} which is invoked by the Id Debugger
to reconstruct the types of all variables in a function's activation
frame. \Proc{Reconstruct-Type} takes the current activation as a
parameter and returns a fully instantiated type-map for that
activation. For ease of presentation, the algorithm makes use of
several auxiliary functions which we will explain where necessary.

\Proc{Reconstruct-Type} is divided into several sections.  We begin by
extracting the name of the activation function from the current
activation.  The first section,
lines~\ref{rt:type-map-begin}--\ref{rt:type-map-end}, instantiates the
type-map of the function with fresh type-variables by building a type
substitution $S_{\sibx{copy}}$. This is necessary so that types from
multiple activations of the same polymorphic function do not
inadvertently interfere with each other.

The next section,
lines~\ref{rt:unify-hints-begin}--\ref{rt:unify-hints-end}, builds a
type substitution $S_{\sibx{hint}}$ for all the non-conserved
type-variables of the function as prescribed by its hint-map. This is
achieved \via the auxiliary function \Proc{Interpret-Type-Hint} which
extracts the encoded data-structure bound to a hint parameter from the
given activation frame, and converts it into a type according to the
encoding scheme shown in Section~\ref{hint-gen}.

Following this, line~\ref{rt:test-done} checks to see if all free
type-variables of the type-map have been instantiated to either ground
or polymorphic types. If so, the reconstruction is complete and the
instantiated type-map is returned at line~\ref{rt:end1}.  Otherwise,
lines~\ref{rt:unify-parent-begin}--\ref{rt:unify-parent-end} obtain
the remaining information from the activation tree as follows.

First, the type-map of the parent of the current activation is
reconstructed by calling \Proc{Reconstruct-Type} recursively with the
parent's activation frame.  Using this type-map and the current
activation, the auxiliary function \Proc{Use-Type} obtains
the reconstructed type-instance of the call site responsible
for invoking the current function (see item~\ref{tm4} of
definition~\ref{type-map}). This type-instance, $\tau_{\sibx{use}}$,
is then unified with the defined type of the current function,
$\tau_{\sibx{def}}$ that is available in the current type-map. Note
that for multiple-arity curried functions, $\tau_{\sibx{def}}$ will be
the full function type involving all its curried arguments, while
$\tau_{\sibx{use}}$ may simply correspond to the final curried
application type of that function. Therefore, \Proc{Unify-Aligned}
must ``align'' these types properly before unification. This
unification fully instantiates all the remaining type-variables in the
current type-map which is then returned at line~\ref{rt:end2}.

A few observations about our reconstruction algorithm are worth
pointing out. First, the entire activation frame of a function is
reconstructed at once. This is possible because the types of all
objects present in an activation frame share the same set of free
type-variables which are precisely captured and instantiated using its
type-map. This also obviates the need to traverse the activation tree
several times for each variable separately. Of course, it is still
possible to have several smaller type-maps for the same activation
frame if the entire information is not required as suggested in
\cite{Goldberg91} in the context of garbage collection.

Second, we traverse the activation tree from the current activation
frame only as far up as necessary. This avoids traversing the
activation tree from the root activation frame to all its leaves as
suggested in \cite{Goldberg91} which would involve a lot of activation
frames in our parallel system. Reconstructed type-maps can always
be cached, so that no activation frame may need to be examined more
than once.

\subsection{An Example}

Consider the problem of type reconstruction for the code in
Example~\ref{ex3}. Assume that the (...) in the definition of {\tt g3}
evaluates to {\tt false} at run-time. Furthermore, suppose the program
is halted when {\tt h3} is invoked due to the application of {\tt g3}
during the evaluation of {\tt ex3}.  The problem is to reconstruct the
types of the objects in {\tt h3}. 

Our compilation scheme described in Section~\ref{compile} translates
{\tt f3} and {\tt g3} of Example~\ref{ex3} into the code shown in
Example~\ref{ex8}. Here, {\tt h3} is augmented with an extra parameter
{\tt h3\_hint\_1}. The purpose of this parameter is to carry
type information concerning the non-conserved type-variable $t_{0}$
within {\tt h3}'s type-map as shown in Section~\ref{hint-detect}.

At run-time, \Proc{Reconstruct-Type} performs the following steps when
invoked on the activation of {\tt h3}. First, it decodes the type-hint
bound to the hint parameter {\tt h3\_hint\_1} and generates a
substitution $S_{\sibx{hint}}=\{(t_{0} \mapsto \ibx{bool})\}$ using
{\tt h3}'s hint-map. Since the free type-variable $t_{1}$ in {\tt
h3}'s type-map is still uninstantiated at this point, \Proc{Reconstruct-Type}
recursively reconstructs the type-map of {\tt h3}'s parent activation
frame. Using this type-map, the call site type-instance of {\tt h3} is
found to be $\tau_{\sibx{use}}=\ibx{int} \rightarrow
(\ibx{list}\;\ibx{int})$ corresponding to the application {\tt (g3 2)}
within {\tt ex3}.  Then, $\tau_{\sibx{def}}$ is assigned the type
$t_{1}\rightarrow(\ibx{list}\;t_{1})$ from {\tt h3}'s type-map.  The
unification of these two types yields the substitution
$S_{\sibx{def-use}}=(t_{1} \mapsto \ibx{int})$.  Finally, the
substitutions $S_{\sibx{hint}}$ and $S_{\sibx{def-use}}$ are applied
to {\tt h3}'s type-map which results in a type of
$(\ibx{list}\;\ibx{bool})$ for {\tt x} and $\ibx{int}$ for {\tt z}.

In contrast with our scheme, the type reconstruction algorithms
proposed by Appel \cite{Appel89} and by Goldberg and
Gloger \cite{Goldberg91,Goldberg92} fail to reconstruct the type of
{\tt x} in the body of {\tt h3}. The reason is that the only run-time
information they use to reconstruct types is that contained in the
run-time stack of the activation frames. When closures such as {\tt
g3} are created, the function that created the closure, {\tt f3}, may
not be present on the stack when the closure is actually {\em
invoked}. Any clues that {\tt f3} might have provided to the type
reconstruction algorithm are therefore not accessible.
