% -*- Mode: LaTeX -*-

\section{Type Reconstruction Framework}
\label{framework}

\subsection{The Expression Language}

We will describe the basic theoretical idea behind our type
reconstruction scheme using the following small expression language. 
\[e ::= c \mid x \mid \lambda{}x.e \mid e_{1}\;e_{2} \mid
\tbx{let}\;x=e_{1}\;\tbx{in}\;e_{2}\] 
Here $c$ and $x$ are meta-variables for constants and variables
respectively.  We use such a small language in order to emphasize the
fundamental nature of this problem. Of course, in a realistic 
language such as Id, we will have to model
many other features such as multiple-arity functions, recursion,
data-structures \etc. But, the essential idea behind type
reconstruction remains the same.

The standard Hindley/Milner typing rules and call-by-value dynamic
semantics rules for this simple language are straightforward and we
will not show them here. The reader is referred to
\cite{Damas82,Milner78,Tofte88} for a detailed description.

\subsection{Run-time Model of Program Execution}

A program in our expression language is simply a set of nested {\tt
let}-bindings where the innermost expression is the user query to be
evaluated within their scope. Below, we describe an abstract model of
evaluation for such a program.

A function application executes in the context of an {\bf activation
frame} which records the actual arguments bound to its formal
parameters, the run-time objects bound to its free variables, and the
values of all its local variables during execution.  We assume that at
any time during execution, all accessible objects either reside
directly in activation frames or in global variables, or are heap
data-structures accessible through the frames or the global variables.
These objects, along with the current expression being evaluated,
define the complete state of the machine that we are interested in
deciphering. Note that we record every local variable of a computation
in its activation frame so that it can be examined later on. As an
optimization, it is also possible to omit type reconstruction of 
objects that are no longer in use as shown in
\cite{Goldberg91}.

In general, evaluation may proceed in parallel, so the run-time state
of the machine at any moment is essentially a tree of active or
suspended activation frames. We assume that at any time during
execution, it is possible to examine and traverse the activation tree.
In particular, the function corresponding to each activation frame is
known and for each leaf activation frame, all its ancestors are
visible. For the moment, this precludes the possibility of ``tail
calls'' which will be discussed later.

Typically, the evaluation of a program is carried out in several
phases. First the top-level bindings are type-checked and converted
into object code at {\bf compile-time}. Then, at {\bf load-time},
these definitions are installed into the root activation frame. This
process builds the global static and dynamic environments under which
the user query is to be evaluated.  When the query expression is
supplied at {\bf invocation-time}, first we type-check it in the
global static environment.  At this point, the exact types of all
top-level objects in the root activation frame are known by
construction. These typed top-level objects together with the typed
query expression constitute the complete {\em initial state} of the
machine.  Finally, we begin the evaluation of the query expression at
{\bf run-time} within the context of the root activation frame. As the
evaluation proceeds, the dynamic activation tree unfolds exposing more
objects and closure applications. Starting from the initial state as
described above, we can view type reconstructibility as an invariant
condition to be maintained at each subsequent evaluation step:

\begin{proposition}[Type Reconstruction Invariance]\label{inv}
As\-suming that the types all objects in the root activation frame and
the query expression are known initially, the exact types of all
accessible objects can be reconstructed after each subsequent step of
dynamic evaluation.
\end{proposition}

We will show how to preserve this invariance in the next
section. 

\subsection{Typed Dynamic Semantics}

\begin{figure}\centering
\begin{tabular}{|c|}
\hline
{\sc Syntactic Categories} \\
\hline\hline
\begin{tabular}{rcl}
$\tau \in$ Type & ::= & $\iota \mid \alpha \mid \tau_{1}\rightarrow\tau_{2}$ \\
$\sigma \in$ Type-Scheme & ::= & $\tau \mid \forall\alpha.\sigma$ \\
Closure & ::= & $[x:\tau',e:\tau,E:\ibx{TE}]$ \\
$v \in$ Value & ::= & Constant $\mid$ Closure \\
$E:\ibx{TE}\in$ Typed-Env & ::= & $\{x_{i}\mapsto{}v_{i}:\sigma_{i}\}$
\end{tabular} \\
\hline
\multicolumn{1}{c}{}\\
\hline
{\sc Inference Rules} \\
\hline\hline
\multicolumn{1}{|l|}{(\cbx{var})} \\
\inference{\stmt{(x\mapsto{}v:\sigma)\in{}E:\ibx{TE}\hmm\sigma\succeq\tau}}%
          {\stmt{E:\ibx{TE}\vdash x\Rightarrow{}v:\tau}} \\
\\
\multicolumn{1}{|l|}{(\cbx{abs})} \\
\inference{\stmt{\ibx{TE}+\{x\mapsto\tau'\}\vdash{}e_1:\tau}}%
          {\stmt{E:\ibx{TE}\vdash\lambda{}x.\:e_1\Rightarrow{[x:\tau',e_{1}:\tau,E:\ibx{TE}]}:\tau'\rightarrow\tau}} \\ 
\\
\multicolumn{1}{|l|}{(\cbx{app})} \\
\inference{\stmt{E:\ibx{TE}\vdash{}e_1\Rightarrow{[x_{0}:\tau',e_{0}:\tau,E_{0}:\ibx{TE}_{0}]}:\tau'\rightarrow\tau} \\
           \stmt{E:\ibx{TE}\vdash{}e_2\Rightarrow{}v_{2}:\tau'} \\
           \stmt{E_0:\ibx{TE}_{0}+\{x_0\mapsto{}v_2:\tau'\}\vdash{}e_0\Rightarrow{}v:\tau}}%
          {\stmt{E:\ibx{TE}\vdash{}e_1\;{}e_2\Rightarrow{}v:\tau}} \\
\\
\multicolumn{1}{|l|}{(\cbx{let})} \\
\inference{\stmt{E:\ibx{TE}\vdash{}e_1\Rightarrow{}v_{1}:\tau'} \\
           \stmt{E:\ibx{TE}+\{x\mapsto{}v_{1}:\fn{Gen}{\ibx{TE},\tau'}\}\vdash{}e_2\Rightarrow{}v:\tau}}%
          {\stmt{E:\ibx{TE}\vdash\tbx{let $x=e_1$ in $e_2$}\Rightarrow{}v:\tau}} \\
\hline
\end{tabular}
\caption{Typed Dynamic Inference Rules.}
\label{fig:typed-dynamic}
\end{figure}

It is possible to satisfy the invariance proposition~\ref{inv}
trivially by propagating the type information at each evaluation step.
\fig{typed-dynamic} shows a typed dynamic semantics for our expression
language that maintains types as it evaluates. Here, $\iota$ and
$\alpha$ are meta-variables for type-constructors and type-variables
respectively. Notation $\sigma\succeq\tau$ means that the type $\tau$
is an instance of the type-scheme $\sigma$, and the sentence
$E:\ibx{TE}\vdash{}e\Rightarrow{}v:\tau$ reads as ``under the typed
environment $E:\ibx{TE}$ the expression $e$ with a type $\tau$
evaluates to a value $v$ with that type''. Note that all syntactic
expressions are fully typed even though we do not show these types to
avoid clutter.

\fig{typed-dynamic} may be viewed as the semantics of a tagged
implementation that pays the price of maintaining types at each
evaluation step. A type reconstruction scheme can then be modeled by
carrying out just the value computation embedded in these rules and
delaying the type computation. In order to preserve the invariance
proposition~\ref{inv} under such a scheme, we must make sure that the
delayed type computation associated with each evaluation rule can be
performed later during a type reconstruction phase. Then, by induction
on the size of the evaluation tree at any given time, we will be able
to reconstruct the types of all accessible objects, starting from the
initial state of the machine. We discuss the various evaluation rules
below.

The first observation is that the \cbx{abs}-rule in
\fig{typed-dynamic} is the only rule that has a premise depending only
on the static type inference rules. That premise says that the body of
the function $\lambda{}x.e$ should be typable under the type
environment present at run-time. It is possible to omit this run-time
typing entirely because it can be reconstructed from the most general
Hindley/Milner typing of the function inferred at compile-time, given
the right run-time instantiation of its static type environment. This
fact follows directly from the completeness of the Hindley/Milner type
inference algorithm \cite{Damas82}.

Secondly, in both \cbx{var}-rule and \cbx{let}-rule, we can
reconstruct all the type information present in the premises by
looking at the corresponding information in the conclusion sentence.
This is because the premises involve only sub-expressions of the
expression present in the conclusion.  Finally, we discuss the
\cbx{app}-rule below.

\subsection{The \cbx{app}-rule and Opacity of Closures}

The \cbx{app}-rule is special because it expands the state of the
machine both in terms of new expressions to evaluate and new types
that they are instantiated to. This expansion happens when the
operator expression $e_{1}$ of the application $(e_{1}\;e_{2})$
evaluates to a closure that contains a typed expression body $e_{0}:\tau$
and a typed free variable environment $E_{0}:\ibx{TE}_{0}$. We can
reconstruct these run-time types by appropriately instantiating the
static type of the function body $e_{0}$ within the reconstructed run-time type
environment $\ibx{TE}$. The relevant static type information for a
function is gathered in a {\em type-map} as follows:
\begin{definition}[Type-map]\label{type-map}
Given a function $\lambda{}x.e$ and the most general static typing of
its body $\ibx{TE}_{\sibx{static}}+\{x\mapsto\tau_{1}\}\vdash{}e:\tau_{2}$, the {\bf type-map}
of the function records the following information:
\begin{tightenum}
\item\label{tm1} The function type, $\tau_{1}\rightarrow\tau_{2}$.
\item\label{tm2} The type-schemes of all the free variables of the function,
$\ibx{TE}_{\sibx{static}}\downarrow$\Proc{Free-Vars}($\lambda{}x.e$). 
\item\label{tm3} The type-schemes of all the local 
variables within the function body $e$.
\item\label{tm4} The type-instance of the expression $e_{1}$
at all application sites $(e_{1}\;e_{2})$ within the function body $e$.
\end{tightenum}
\end{definition}
A type-map is essentially a compile-time type-description of the
activation frame of a function with additional type information
about its internal call sites. The set of free type-variables
occurring in items~\ref{tm1} and \ref{tm2} above capture the essential
part of the static type environment that needs to be instantiated at
run-time to yield the appropriate run-time types of all
objects in the type-map. We will denote this set by
\Proc{Type-Vars}(\ibx{type-map})\footnote{In general,
\Proc{Type-Vars}(T) denotes the set of free type-variables of T, where
T may be a type, a type-scheme, or a type environment.}. This set
automatically excludes the bound type-variables in the type-schemes of
polymorphic free variables of the function as pointed out in
Section~\ref{free-vars}.

Looking back at the \cbx{app}-rule, we notice that the only
available information about the closure in the conclusion sentence is
its overall run-time type $\tau'\rightarrow\tau$. In particular, there
is no directly available information about the run-time types of its
free variables. Also, in curried applications of multiple-arity
functions, the available closure type will correspond to just the
remaining arguments of the function and may not be sufficient to
instantiate the previously accumulated argument types present in its
type-map. For example, recall that in Example~\ref{ex2} the run-time
type of the closure {\tt g2} within {\tt ex2} did not provide any hint
about the hidden first argument of the function {\tt f2}.

The above discussion leads us to the important observation that
closure types are sometimes {\em opaque} so that they are not
sufficient to completely instantiate the type-map of the function body
present inside them. We capture this fact in the following property
of general multiple-arity functions:
\begin{definition}[Type Conservation]\label{conserve}
A function $f$ with arity $k$ and type-scheme
$\forall\alpha_{1}\ldots\alpha_{n}.
\tau_{1}\rightarrow\cdots\rightarrow\tau_{k}\rightarrow\tau_{k+1}$
is said to be {\bf type-conserving} if,
\[\mbox{\Proc{Type-Vars}}(\ibx{type-map}_{f})=
\mbox{\Proc{Type-Vars}}(\tau_{k}\rightarrow\tau_{k+1})\] 
Furthermore, the type-variables
\Proc{Type-Vars}$(\tau_{k}\rightarrow\tau_{k+1})$ are said to be {\bf
conserved} at the application site of its final argument. 
\end{definition}
Informally, a type-conserving function can correctly instantiate its
entire type-map with just the run-time type of its final application
closure. It is easy to check that {\tt map} and {\tt enlist} from
Example~\ref{ex1} are type-conserving, while {\tt f2} from
Example~\ref{ex2} and {\tt f3} and {\tt h3} from Example~\ref{ex3} are
not, which is why we were losing type information in those cases.

Definition~\ref{conserve} may be used by a compiler to detect
functions that are not type-conserving. The next question is what type
reconstruction strategy should be devised for such functions? Our
scheme is to make every closure object {\bf self-sufficient}, which
means that a closure for a non-type-conserving function is required to
contain special ``tag'' objects in its environment that are inserted
at the time of its creation and are deposited into the dynamic
function activation. These tags are compiler-generated {\em
type-hints} that are interpreted at run-time in order to correctly
instantiate all the type-variables that were not conserved by the
function. We will show such a compilation scheme in the next section.

Given self-sufficient closures as described above, all
types in the premises of the \cbx{app}-rule in \fig{typed-dynamic}
can be correctly instantiated thereby preserving the invariance
proposition~\ref{inv} in all cases.  This implies that complete type
reconstruction is possible for every activation frame in the dynamic
activation tree by instantiating its type-map using type-hints and the
call site information available from its caller's type-map. The
details of this reconstruction scheme appear in
Section~\ref{reconstruct}.
