% -*- Mode: LaTeX -*-

\section{Type Reconstruction Problem}
\label{problem}

The problem of type reconstruction for Id can be described as follows.
At some point during the execution of a program, we wish to take a
snapshot of the state of the machine and determine the type of every
object accessible within the computation.  These types can then be
used to display the corresponding objects.

We assume that the program is statically typed and that the run-time
environment does not keep {\em any\/} type information. In particular,
Id run-time objects do not carry any type-tags. Therefore, the type
reconstruction information so obtained may also be useful for garbage
collection.\footnote{Goldberg and Gloger
\cite{Goldberg92} show that complete type information is not {\em
strictly necessary} for successful garbage collection, but its absence
greatly increases the complexity of the process.}

%The problem of type reconstruction addressed by this paper is
%conceptually simple.  At some point during the execution of a program,
%we wish to take a snapshot of the state of the machine, and we want to
%be able to determine the type of every object accessible by the
%program.  We assume that the program is statically typed and that the
%run-time environment does not keep {\em any\/} type information.
%
%The need to solve this problem initially arose during the development
%of a debugger for Id. This accounts for the broad scope of the
%reconstruction problem: in a debugger, it may become necessary to
%display the values of all the variables associated with every
%procedure activation. Without complete type information, this would be
%impossible. Complete type information is also quite useful for garbage
%collection.\footnote{Goldberg and Gloger \cite{Goldberg92} show that
%complete type information is not {\em necessary} for successful
%garbage collection, but its abscence greatly increases the complexity
%of the process.}
%
%Most implementations of statically-typed languages still use some form
%of type information (tags) at run-time.  In SML-NJ, the tags amount to
%a few bits per word, but in other languages, such LML, the tags
%manifest themselves as pointers to specialized code routines. Id data
%structures contain no run-time type information, and the
%implementation does not pay the associated costs in execution time and
%storage space.

Clearly, only polymorphic objects and functions pose some challenge;
complete type information can be obtained at compile-time for
monomorphic objects. Also note that the exact nature of the desired
information depends on the application that uses it. For example, a
source debugger may wish to inspect any particular object from the
current run-time state of the machine whereas a garbage collector only
needs to traverse those that are still in use. Also, most garbage
collectors only need to differentiate between scalars and pointers to
structures while a source debugger needs exact type information in
order to display the object properly. In general, we would like to
devise a flexible strategy that can be optimized according to the
level of information desired.

\subsection{A Preliminary Type Reconstruction Scheme}

The compile-time type of an object is a good starting point for the
reconstruction of its run-time type. The basic idea is to instantiate
this compile-time type with additional type information based on the
run-time call tree in order to obtain its full run-time type.

Appel noted in \cite{Appel89} that the types of the objects inside a
polymorphic function depend on the types of its arguments. Further,
the compile-time type-instances of the arguments of a polymorphic
function are recorded statically at the call site in its
caller. At run-time, the call site of a function can be
determined by examining the return address information in the run-time
call stack (which is the visible, suspended part of the dynamic activation
tree). The run-time types of the arguments are then determined from
their static type-instances inductively by following up the call
chain possibly up to the root where the run-time types of the
user-supplied arguments are available.  At that point, all polymorphic
functions in the call chain can be correctly instantiated revealing
the run-time types of their internal objects. We illustrate this idea
with a small example\footnote{We use the Id language \cite{Id90.1} for
our examples. Briefly, functions are introduced with a {\it def}
keyword and allow pattern-matching on their arguments. (:) is the
infix {\it cons} operation.}:

\begin{myexample}{ex1}
def enlist x$_{t_{0}}$ = x:nil;
def map f nil = nil
 |  map f (y:ys)$_{(\sibx{list}\:t_{1})}$ = (f y$_{t_{1}}$):(map f ys); 
\vsp
ex1 = map enlist (1:2:nil)$_{(\sibx{list}\:\sibx{int})}$;
\end{myexample}

The function {\tt enlist} has a type
$\forall{}t_0.t_0\rightarrow(\ibx{list}\;t_0)$ and {\tt map} has a
type $\forall{}t_1t_2.(t_1\rightarrow{}t_2)\rightarrow
(\ibx{list}\;t_1)\rightarrow(\ibx{list}\;t_2)$. We also show the type
instances of some internal identifiers as subscripts. The evaluation
of {\tt ex1} unfolds into a call to {\tt map} which in turn calls {\tt
enlist}. If we wish to examine the {\tt x} argument of {\tt enlist}
during one of these calls, then the run-time instantiation of its
static type $t_{0}$ can be determined by following up the call chain
within the definition of {\tt map}. Here, $t_{0}$ can be related to
the static type $t_{1}$ of the actual argument {\tt y} at that
call site. This relates to the type of the second argument
$(\ibx{list}\;t_{1})$ of {\tt map} which is found to be
$(\ibx{list}\;\ibx{int})$ at its call site inside {\tt ex1}.
Then, both $t_{1}$ and $t_{0}$ can be instantiated to \ibx{int} giving
the actual type of {\tt x} as desired. Goldberg showed in
\cite{Goldberg91} that this process can be conducted in one pass from
the root of the activation tree (bottom of the call stack) to its
leaves (top of the call stack) instantiating the types of all objects
correctly in a single sweep.

\subsection{Problems with Closures and Free Variables}
\label{free-vars}
Goldberg and Gloger noted in \cite{Goldberg92} that sometimes types of
objects hidden inside a closure are impossible to reconstruct.
Consider the following example:

\begin{myexample}{ex2}
def f2 x$_{t_{0}}$ y$_{t_{1}}$ = y;
g2 = if ... then f2 1$_{\sibx{int}}$ else f2 "foo"$_{\sibx{string}}$;
\vsp 
ex2 = g2 2;
\end{myexample}

Here, {\tt f2} has a type
$\forall{}t_{0}t_{1}.t_{0}\rightarrow{}t_{1}\rightarrow{}t_{1}$, and
therefore {\tt g2} gets bound to a partially applied function closure
with type $\forall{}t_{2}.t_{2}\rightarrow{}t_{2}$ that says nothing
about the type of the data hidden inside it. In fact, this type cannot
be determined at compile-time because it depends on the value of the
predicate ($\ldots$). Besides, during the evaluation of {\tt ex2}
the return address information on the call stack would point to the
call site of {\tt g2} inside {\tt ex2}, which does not help in
determining the contents of that closure either. Thus, we cannot
reconstruct the type of the argument {\tt x} within the activation of
{\tt f2} because the computation that created its closure is no longer
available as part of the dynamic activation tree.

It may appear that this problem arises only when an argument of a
function is never used within its body, but the following example
adapted from \cite{Goldberg92} shows that this is not the
case\footnote{Let-bindings in Id are enclosed within \{\}. The result
of such a block is the value of the expression following {\it in}.}:

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

Here, the type of the function {\tt f3} is
$\forall{}t_{0}t_{1}.(\ibx{list}\;t_{0})\rightarrow{}t_{1}\rightarrow{}(\ibx{list}\;t_{1})$,
and therefore the type of the computed closure {\tt g3} is
$\forall{}t_{2}.t_{2}\rightarrow(\ibx{list}\;t_{2})$. During the
evaluation of {\tt ex3} no information is available in the activation tree
whether this closure contains a list of booleans or a list of
integers. Goldberg and Gloger argue in \cite{Goldberg92} that since {\tt h3}
does not use the elements of its free variable list {\tt x} but only
its spine (to compute its length), a garbage collector can ignore these
elements and copy just the spine. But this approach
creates problems if these structures were shared in many places and is
quite unsatisfactory for a source debugger that needs to display the
full object.

Note that we do not have this problem all the time. For instance, the
type of argument {\tt z} within {\tt h3} in the above example may be
reconstructed to \ibx{int} by traversing up the call stack to its
call site inside {\tt ex3}. Some functions like {\tt map} of
Example~\ref{ex1} never have this problem:

\begin{myexample}{ex4}
g4 = (map enlist)$_{(\sibx{list}\:t_{0})\rightarrow(\sibx{list}\:(\sibx{list}\:t_{0}))}$;
ex4 = g4 (1:2:nil)$_{(\sibx{list}\:\sibx{int})}$;
\end{myexample}

Even though here {\tt map} is partially applied to {\tt enlist} to
yield a closure {\tt g4} with type $\forall{}t_{0}.
(\ibx{list}\;t_{0})\rightarrow(\ibx{list}\;(\ibx{list}\;t_{0}))$, we
have not lost any type information. Instantiation of $t_{0}$ to
\ibx{int} at the call site of {\tt g4} inside {\tt ex4} yields
complete type information about all the internal identifiers of both
{\tt map} and {\tt enlist}. The problem with Examples~\ref{ex2} and
\ref{ex3} is that sometimes the types of closures do not have any
connection with the types of objects hidden inside them. In such cases,
we are in danger of losing type reconstruction information because the
closure creation site may no longer be available on the call stack.

Another interesting point is that polymorphic objects with universally
quantified types do not pose this problem.  The run-time type of such
an object cannot be more specific than its compile-time definition
type. For instance, in the following example the variable {\tt x}
within the body of {\tt f5} has the universally quantified type 
$\forall{}t_{0}.(\ibx{list}\;t_{0})$.

\begin{myexample}{ex5}
def f5 y = 
  \{ x = nil;
    def h5 z$_{t_{1}}$ = if length x$_{(\sibx{list}\:t_{0})}$ == 1
                then z:nil
                else z:z:nil;
   in h5 \};
\end{myexample}

Now, there is no question about the contents of the closure formed by
{\tt h5} over its free variable {\tt x}. It can never contain an
object whose type is more specific than
$\forall{}t_{0}.(\ibx{list}\;t_{0})$. For our purposes, this means
that the compile-time type of a polymorphic object provides sufficient
information for its run-time type reconstruction.
