% -*- Mode: LaTeX -*-

\section{Garbage Collection using Type Reconstruction}
\label{trec}

The overall strategy for type-reconstruction-based garbage collection
is summarized below and described in the following sections:
\begin{tightenum}
\item At compile-time, we ensure that every object manipulated by the
user program (including function closures and activation frames) is
assigned a static, possibly polymorphic, datatype that accurately
describes the structure of that object (Section~\ref{typing}).
\item When the garbage collector is invoked at run-time, first we
reconstruct the type of every activation frame present within the
current dynamic call tree. The reconstruction mechanism instantiates
the compile-time type description of each activation frame to its
exact run-time type using the algorithm described in \cite{Aditya93}
(Section~\ref{reconstruct}).
\item During the mark phase of the garbage collector, the
reconstructed frame-slot types are used to mark the reachable heap
objects as live. This may be done in two ways: the reconstructed types
may be directly interpreted to identify and traverse the heap objects,
or the compiler may automatically generate specialized traversal and
mark routines that are appropriately composed at run-time in order to
mark the live objects (Section~\ref{traversal}). 
\item Finally, the unmarked objects are reclaimed as garbage by
sweeping the entire heap. 
\end{tightenum}

\subsection{Compiler Support for Object Identification}
\label{typing}

\subsubsection{Visible and Invisible Datatypes}

The scalar basetypes, algebraic datatypes, and array types in Kernel
Id correspond to pure data-objects whose types are directly
\ibx{visible} at the source language level. There is a direct, fixed
mapping from the source types of these objects to their internal
representations as described in Section~\ref{reptn}.  This mapping may
be directly used in traversing these objects at run-time once their
exact source type is determined.

On the other hand, arrow types ($\rightarrow$) correspond to two
different run-time objects: function closures which behave like
data-objects that must be garbage collected, and activation frames
which are control-objects consisting of the live object root set.
Neither of these is modeled completely by the source-level arrow type.
This is because the visible type signature of a function does not
provide any clue regarding the types of the arguments hidden inside
its closure, nor does it provide any information about the local
variables kept within the function's activation frame.  To remedy this
situation, we define \ibx{invisible} datatypes for these objects that
provide an accurate description of their contents.

\subsubsection{Modeling Function Closures}

In order to simplify the type reconstruction analysis, we model the
closures corresponding to partial applications of a function as
disjuncts of an invisible algebraic datatype that is automatically
derived at compile-time from the corresponding function signature.
This derivation is shown in \fig{kidaux}. The various disjuncts of
this hidden datatype represent successive partial applications of the
function and identify the number and the types of the accumulated
arguments. This indirect model captures all the necessary type
information required to traverse the actual run-time representation of
a function closure as shown in \fig{reptn}. Given a run-time closure
object, we can map it to an algebraic disjunct in this model by
examining its function code-block pointer and the remaining arity
slot. Then, given the exact algebraic type of the closure, the
arguments contained within the closure can be traversed using the
argument types of the mapped disjunct.

As an example, below we show a function \tbx{eqlen} that compares the
length of two lists. We also show its Hindley/Milner visible source
type and its automatically derived hidden closure datatype:

\begin{myexample}{ex1}
def eqlen l1 l2 =        \% eqlen $::\forall\alpha\beta.(\ibx{list}\;\alpha)\rightarrow$
  \{ len1 = length l1;    \%       $(\ibx{list}\;\beta)\rightarrow\ibx{bool}$
    len2 = length l2;
    p = len1 == len2;
   in p \};
\vsp 
type eqlen\_closure $\alpha$ $\beta$ =   \% \bx{Hidden Closure Type}
  eqlen\_ap$_{0}$
| eqlen\_ap$_{1}$ $(\ibx{list}\;\alpha)$;
\vsp 
f = eqlen (1:nil);  \% f $::\forall\beta.(\ibx{list}\;\beta)\rightarrow\ibx{bool}$
                    \% f $::\forall\beta.(\tbx{eqlen\_closure}\;\ibx{int}\;\beta)$
\end{myexample}

The constructor \tbx{eqlen\_ap$_{0}$} models the closure
representation of the \tbx{eqlen} function itself, while
\tbx{eqlen\_ap$_{1}$} represents the closure formed by a partial
application of the \tbx{eqlen} function to one argument. The example
also shows the source type and the invisible type of a partial
application of the \tbx{eqlen} function.\footnote{``:'' is the infix
\sibx{cons} constructor for lists.} Note that the invisible type
records the fact that the hidden first argument within the closure is
a list of integers while this information is not present in the source
type.

There is no need to make a closure for \tbx{eqlen} with two arguments
since at that point its arity is fully satisfied and the application
gives rise to an activation frame instead of a function
closure.\footnote{However, under delayed or lazy evaluation, we may
need to keep track of such \sibx{thunks}.} Finally, note that the
invisible closure datatype is parameterized by \ibx{all} the
type-variables present in the source type of the function. This is
necessary in order to model the exact run-time types of all the
arguments contained within the closure.

\subsubsection{Modeling Activation Frames}

\begin{figure}
\centering
\begin{tabular}{|l|}
\hline
\multicolumn{1}{|c|}{\cbx{Invisible Datatypes}} \\
\hline\hline
Given a Function Declaration: \\
\hm \tbx{def} $F\;x_{1} \cdots x_{n} = E$ \\
\hm $F::\forall\alpha_{1}\cdots\alpha_{m}.\tau_{1}
\rightarrow\cdots\rightarrow\tau_{n}\rightarrow\tau_{n+1}$ \\[.1in]

Define Function Closure Datatype: \\
\hm \tbx{type} $F\_\tbx{closure}\;\alpha_{1}\cdots\alpha_{m}$ = \\
\hmmm $F\_\tbx{ap}_{0}$ \\
\hmm $\mid\;F\_\tbx{ap}_{1}\;\tau_{1}$ \\
\hmm $\mid\cdots$ \\
\hmm $\mid\;F\_\tbx{ap}_{n-1}\;\tau_{1}\cdots\tau_{n-1}$; \\[.1in]

Let $(z_{1}::\sigma_{1})\cdots(z_{k}::\sigma_{k})$ be the Bound Identifiers of $E$.\\
Let $(f_{1}::\tau_{f_{1}})\cdots(f_{l}::\tau_{f_{l}})$ be the type-instances of all \\
function application sites within $E$. \\[.1in]

Define Function Typemap Datatype: \\
\hm \tbx{type} $F\_\tbx{typemap}\;\alpha_{1}\cdots\alpha_{m}$ = \\
\hmm \{record \\
\hmmm $\;(F::\tau_{1}\rightarrow\cdots\rightarrow\tau_{n}\rightarrow\tau_{n+1})$
\hm\tbx{\%} Fn. Signature \\  
\hmmm\begin{tabular}{ll} 
$(x_{1}::\tau_{1})$ & \tbx{\%} Argument Types \\ 
$\cdots$ & \\ 
$(x_{n}::\tau_{n})$ & \\ 
$(z_{1}::\sigma_{1})$ & \tbx{\%} Bound Identifier Types \\ 
$\cdots$ & \\ 
$(z_{k}::\sigma_{k})$ & \\ 
$(f_{1}::\tau_{f_{1}})$ & \tbx{\%} Application Site Types \\
$\cdots$ & \\ 
$(f_{l}::\tau_{f_{l}})\;\};$ &
\end{tabular} \\
\hline
\end{tabular}
\caption{Automatic Derivation of Invisible Datatypes.}
\label{fig:kidaux}
\end{figure}

Function activation frames are modeled using an automatically derived,
invisible datatype called the function \ibx{typemap}. One typemap
datatype is defined for each function definition in the program as
shown in \fig{kidaux}. The typemap of a function captures all the
necessary compile-time information to reconstruct the complete type of
its activation frame at run-time using the mechanism described
in \cite{Aditya93}.

The typemap of a function is parameterized by the type-variables
present in the function's type signature. The typemap records the
function's signature, the types of its arguments and its bound
identifiers, and the compile-time type-instances of all function
application sites within the body of the given function. The argument
and the bound identifier types model the corresponding frame slots of
the function's activation frame, while the application site
information is used for type reconstruction. Once all the parameter
type-variables of a function's typemap are properly instantiated \via
type reconstruction, the typemap datatype provides the exact run-time
type of all objects accessible through each argument and bound
identifier slot of the corresponding activation frame.

As an example, we show the typemap datatype for the \tbx{eqlen}
function given above:

\begin{myexample}{ex2}
type eqlen\_typemap $\alpha$ $\beta$ =
  \{record
     (eqlen   :: $(\ibx{list}\;\alpha)\rightarrow(\ibx{list}\;\beta)\rightarrow\ibx{bool}$)
     (l1      :: $(\ibx{list}\;\alpha)$)
     (l2      :: $(\ibx{list}\;\beta)$)
     (len1    :: \ibx{int})
     (len2    :: \ibx{int})
     (p       :: \ibx{bool})
     (length$_{1}$ :: $(\ibx{list}\;\alpha)\rightarrow\ibx{int}$)
     (length$_{2}$ :: $(\ibx{list}\;\beta)\rightarrow\ibx{int}$) \};
\end{myexample}

Note that the two application sites of the \tbx{length} function are
separately recorded with their own compile-time type-instances. 

\subsection{Compiler-directed Type Reconstruction}
\label{reconstruct}

Compiler-directed type reconstruction requires some cooperation
between the compiler and the run-time system. In the preceding
section, we described the compiler support necessary to facilitate
run-time type reconstruction. In this section, we describe the
run-time data-structures and the reconstruction algorithm. A more
detailed description of the algorithm may be found in \cite{Aditya93}.

\subsubsection{Run-Time Type Encodings}

\begin{figure}
\centering
\begin{tabular}{|l|}
\hline
\multicolumn{1}{|c|}{\cbx{Encoding Schema} \lbx{C}} \\
\hline\hline
Given a Type $T^{n}$, define \\
\hm$\lbx{C}\dlb T^{n} \drb = \tbx{encode\_}T$, where \\
\hm$\;\tbx{def}\;\tbx{encode\_}T\;(x_{1},\ldots,x_{n}) = 
\fn{pack}{\overline{T^{n}},x_{1},\ldots,x_{n}}$ \\[.1in]
Given a polymorphic type-variable $\alpha_{i}$, define \\
\hm$\lbx{C}\dlb T^{0}_{\alpha_{i}} \drb = \tbx{encode\_}T_{\alpha_{i}}$, where \\
\hm$\;\tbx{def}\;\tbx{encode\_}T_{\alpha_{i}}\;() = \overline{T^{0}_{\alpha_{i}}}$ \\
\hline
\end{tabular}
\caption{Run-time Encodings for Datatypes.}
\label{fig:code-schema}
\end{figure}

Run-time type reconstruction requires an \ibx{encoding} of
the datatypes that may be computed and instantiated during
reconstruction.  Each datatype $T^{n}$ is encoded into a corresponding
type descriptor $\overline{T^{n}}$ that contains all the necessary
compiler information about its arity, internal field structure, and
its representation. Conceptually, for each polymorphic datatype
$T^{n}$ with $n$ type parameters, we define a corresponding encoding
function \tbx{encode\_$T$} that takes $n$ encoded arguments and \ibx{pack}s
them along with the encoded type descriptor $\overline{T^{n}}$ into a
single type data-structure. Such an {\it encoding schema} \lbx{C} is shown in
\fig{code-schema}. These functions may be used to create encodings of
type-instances computed during type reconstruction. The bound type
variables $\alpha_{i}$ of a polymorphic type-scheme
$\forall\alpha_{1}\cdots\alpha_{n}.\tau$ are encoded as special
parameterless datatypes $\overline{T^{0}_{\alpha_{i}}}$ because they
do not participate in type reconstruction.\footnote{This is because
the exact run-time type of an object with a closed polymorphic type
(\eg, $\stbx{nil}::\forall\alpha.(\sibx{list}\;\alpha)$) is that
polymorphic type itself, see \cite{Aditya93} for details.}

In practice, our compiler generates static type descriptors
$\overline{T^{n}}$ for all the user-defined algebraic datatypes within
the program and for the automatically derived closure and typemap
datatypes corresponding to every function in the program.  These
static descriptors are linked together with the program and are used
during type reconstruction. Run-time types are encoded as a flat array
of static type descriptors using back-pointers to preserve sharing.
This representation permits very efficient copying, unification, and
instantiation operations on encoded types. The packing and unpacking
of these encoded types is carried out on the fly within the run-time
system, therefore no separate encoding functions are actually
necessary.

\subsubsection{Run-Time Type Reconstruction}

When the type reconstruction of an activation frame is requested at
run-time, we check whether the corresponding function is polymorphic
and therefore may need some additional type context in order to
properly instantiate its typemap. If not, then the compiler-generated
encoding of the function's typemap already contains all the type
information necessary to traverse the corresponding activation frame
and no more work is necessary.

If the current function is polymorphic, then its parent activation
frame is identified using the return continuation and is recursively
type reconstructed.  This recursive process continues towards the root
of the dynamic call tree until a non-polymorphic function or the root
frame is reached. At the root, the types of all the user-supplied
arguments completely determine the type context for instantiating the
root typemap. On unwinding the recursion back to the original
activation frame, the return continuation in the current frame
identifies its particular application site recorded within the
parent's typemap. Now, the fully reconstructed application site type
from the parent's typemap is matched against the current function's
type signature to determine the exact type-instances of its
polymorphic type parameters. This instantiates the typemap of the
current function which can then be used to traverse its activation
frame.

Note that the entire typemap for an activation frame is instantiated
at once and is remembered subsequently. Therefore, no activation frame
needs to be reconstructed more than once even if it has several
branches below it. Thus, the overall complexity of reconstructing
every frame in the dynamic call tree is proportional to the total
number of activation frames present in the tree.\footnote{Each
reconstruction step manipulates Hindley/Milner types of the original
program which in the worst case could be very large \cite{Mairson90},
but such cases rarely occur in practice.}

The only problem with the above scheme is that sometimes the
type-instance of an application site may not be sufficient to
instantiate all the type parameters of a function's typemap or its
hidden closure type. As an example, consider the following situation
involving the \tbx{eqlen} function shown earlier:

\begin{myexample}{ex3}
eqlen $::\forall\alpha\beta.(\ibx{list}\;\alpha)\rightarrow(\ibx{list}\;\beta)\rightarrow\ibx{bool}$
f = eqlen (1:nil);    \% f :: $\forall\beta.(\ibx{list}\;\beta)\rightarrow\ibx{bool}$
                      \% \bx{Instantiation} $\{\alpha\mapsto\ibx{int}\}$
...
p = f ("foo":nil);    \% \bx{Instantiation} $\{\beta\mapsto\ibx{string}\}$
\end{myexample}

At the first application site, the function \tbx{eqlen} is partially
applied to create a closure \tbx{f}. Neither the source type, nor the
subsequent type-instance of this closure at the second application
site reflect the hidden type instantiation
$\{\alpha\mapsto\ibx{int}\}$. Without this information, the exact type
of the elements of the list hidden inside the closure \tbx{f} can not
be reconstructed.  In such a situation, Goldberg and Gloger
\cite{Goldberg92} argue that since those elements are never accessed
by the function \tbx{eqlen}, they need not be traversed and marked as
live. Only the spine of the list is marked as live.  Unfortunately, if
this list is shared among other activation frames its elements may
still be live and may not be garbage collected.

Managing partially marked, shared objects is a difficult and unsolved
problem \cite{Goldberg92}. Instead, our scheme guarantees full type
reconstruction at every object reference so that an object can be
marked completely the first time around. In the above example, our
reconstruction mechanism encodes the hidden type instantiation
explicitly at the first application site and passes it to the
\tbx{eqlen} function as an additional parameter \cite{Aditya93}. This
encoded \ibx{type-hint} is directly used to reconstruct the invisible
type of the closure \tbx{f} and to instantiate \tbx{eqlen}'s typemap.
This is the only situation where an explicit, compiler-generated
encoded type needs to be propagated at run-time to ensure full type
reconstruction.

\subsection{Object Traversal and Marking}
\label{traversal}

In this section, we describe our scheme for object traversal and
marking after complete type reconstruction has been performed. We
present two mechanisms:
\begin{tightdesc}
\item[{\bf Interpreted Marking}] -- In this mechanism, the encoded types
generated by type reconstruction are directly used to guide the
traversal and marking of the heap objects.
\item[{\bf Compiled Marking}] -- In this mechanism, the compiler
automatically generates marking functions for each datatype in the
program based solely on the static type information. These functions
are appropriately composed at run-time using the reconstructed types
and then directly applied to the corresponding objects.
\end{tightdesc}
Both mechanisms are specified as a set of mark functions, one for each
basetype, array type, and algebraic datatype present in the program.
The algebraic datatype could be a user-defined datatype (\fig{kid}) or
an invisible datatype defined by the compiler for function closures
and activation frames (\fig{kidaux}).

\subsubsection{Interpreted Marking}
\label{intmark}

\begin{figure}
\centering
\begin{tabular}{|l|}
\hline
\multicolumn{1}{|c|}{\cbx{Marking Schema} \lbx{M}} \\
\hline\hline
Given a Type $T^{n}$, define \\
\hm$\lbx{M}\dlb T^{n} \drb = \tbx{mark\_}T$, where \\ \\

1. $T^{0}$ is a BaseType ($\ibx{int}\mid\ibx{float}$): \\
\hm$\begin{array}{l}
\tbx{def}\;\tbx{mark\_}T\;() = \lambda{}x.()
\end{array}$ \\ \\

2. $T^{1}$ is an ArrayType ($\fbx{n}\ibx{d\_array}\;\alpha$): \\
\hm$\begin{array}{l}
\tbx{def}\;\tbx{mark\_}\fbx{n}\ibx{d\_array}\;(z) = \\
\hm \lambda{}a.\{ \; \fn{Mark}{a}; \\
\hmmm (l_1,u_1),\ldots,(l_n,u_n) = \fn{bounds}{a}; \\
\hmmm \tbx{for}\;i_1 \leftarrow l_1\;\tbx{to}\;u_1 \;\cdots \\
\hmmm\; \tbx{for}\;i_n \leftarrow l_n\;\tbx{to}\;u_n \\
\hmmmm \interpret\dlb\lbx{M}\drb \\
\hmmmm \hm\;(\compile\dlb\lbx{C}\drb\;\{\alpha\mapsto{}z\}\;\alpha) \\
\hmmmm \hm\;a[i_1,\ldots,i_n]; \}
\end{array}$ \\ \\

3. $T^{n}$ is an Algebraic DataType ($T^{n}\;\alpha_{1}\cdots\alpha_{n}$): \\
\hm$\begin{array}{l}
\tbx{def}\;\tbx{mark\_}T\; (z_1,\ldots,z_n) = \\
\hm \lambda{}x. \{\; \fn{Mark}{x}; \\
\hmmm \tbx{Case\_}T\;x \\
\hmmmm C_1\;x_1\cdots{}x_{k_1} = \\
\hmmmm \{\; \interpret\dlb\lbx{M}\drb \\
\hmmmm \hmm\;(\compile\dlb\lbx{C}\drb\;\{\alpha_i\mapsto{}z_i\}\;\tau_{11})\;x_1;\\
\hmmmm\hm \cdots \\
\hmmmm\hm \interpret\dlb\lbx{M}\drb \\
\hmmmm \hmm\;(\compile\dlb\lbx{C}\drb\;\{\alpha_i\mapsto{}z_i\}\;\tau_{1k_1})\;x_{k_1}; \}\\
\hmmm \mid \cdots \\
\hmmm \mid C_m\;x_1\cdots{}x_{k_m} = \cdots \}
\end{array}$ \\ \\

Given a polymorphic type-variable $\alpha_{i}$, define \\
\hm$\begin{array}{l}
\lbx{M}\dlb T^{0}_{\alpha_{i}} \drb = \tbx{mark\_}T_{\alpha_{i}}, \bx{where} \\ 
\tbx{def}\;\tbx{mark\_}T_{\alpha_{i}}\;() = \lambda{}x.()
\end{array}$ \\
\hline
\end{tabular}
\caption{Generating Mark Functions for Datatypes.}
\label{fig:mark-schema}
\end{figure}

The {\it Interpreted Marking Schema} \lbx{M} for a type $T^n$ is
shown in \fig{mark-schema}. In this schema, for each type $T^{n}$ with
$n$ type parameters $\alpha_{1}\cdots\alpha_{n}$, we define a mark
function \tbx{mark\_$T$} that is parameterized by $n$ corresponding
encoded type arguments $z_{1}\cdots{}z_{n}$. At run-time, this
function is supplied with the exact encoded type instantiation of its
type parameters, say $\overline{\tau_{1}}\cdots\overline{\tau_{n}}$,
which produces an appropriate marking function for an object
with type $(T^{n}\;\tau_{1}\cdots\tau_{n})$.

The internal structure of the mark functions closely follows the
structure of their corresponding datatypes.  All our base types are
scalars, so the mark functions for them do nothing.  The mark function
for arrays and algebraic datatypes first mark the object itself and
then proceed to mark their internal components. This is achieved by
first building their exact run-time type encoding by appropriately
\ibx{composing} the encoding functions given by
\fig{code-schema}, and then recursively \ibx{interpreting} that
encoding.  Finally, the polymorphic, bound type-variables of a
type-scheme are also mapped to dummy mark functions because
polymorphic objects contain no information.

\begin{figure}
\centering
\begin{tabular}{|l|}
\hline
\multicolumn{1}{|c|}{\cbx{Type-based Translation}} \\
\hline\hline
Given a Compilation Schema \lbx{R}, \\
and a Translation Environment $\rho_{r}$, define  \\[.1in]
$\begin{array}{lccl}
\compile\dlb\lbx{R}\drb\;\rho_{r} & \alpha & = & \rho_{r}(\alpha) \\
\compile\dlb\lbx{R}\drb\;\rho_{r} & (T^n\;\tau_1\cdots\tau_n) & = & \\ 
\multicolumn{4}{l}{\hm(\lbx{R}\dlb T \drb)\;(\compile\dlb\lbx{R}\drb\;\rho_{r}\;\tau_1,\ldots,
\compile\dlb\lbx{R}\drb\;\rho_{r}\;\tau_n)} \\
\compile\dlb\lbx{R}\drb\;\rho_{r} & \forall\alpha_{1}\cdots\alpha_{n}.\tau & = & \\
\multicolumn{4}{l}{\hm\compile\dlb\lbx{R}\drb\;\rho_{r}\;(\tau[T^{0}_{\alpha_{i}}/\alpha_{i}])}\\
\end{array}$ \\
\hline\multicolumn{1}{c}{}\\\hline
\multicolumn{1}{|c|}{\cbx{Type-code Interpretation}} \\
\hline\hline
Given a Compilation Schema \lbx{R}, define \\[.1in]
$\interpret\dlb\lbx{R}\drb\;\overline{\tau} = $ \\ 
\hm$\begin{array}{l}
\{\tbx{Case}\;\fn{head}{\overline{\tau}}  \\
\hm \overline{T^{n}_{1}} = \{\; x_{1},\ldots,x_{n} = \fn{arguments}{\overline{\tau}};\\
\hmmmm\tbx{in}\;(\lbx{R}\dlb T^{n}_{1}\drb)\;(x_{1},\ldots,x_{n})\;\}\\
\mid \;\overline{T^{m}_{2}} = \cdots \\
\mid \;\cdots \}\}
\end{array}$ \\
\hline
\end{tabular}
\caption{Type-based Translation and Interpretation.}
\label{fig:compint}
\end{figure}

The general mechanism of type-based function composition
$(\compile\dlb\lbx{R}\drb\;\rho_{r}\;\tau)$ for an arbitrary schema
\lbx{R} (such as the encoding schema \lbx{C} or the mark schema
\lbx{M}) is shown in \fig{compint}. This process translates a given
type $\tau$ into a composition of schema functions specified by
\lbx{R} under a translation environment $\rho_{r}$ that maps free type
variables of $\tau$ to schema-dependent values. In our present case,
$(\compile\dlb\lbx{C}\drb\;\linebreak\{\alpha_{i}\mapsto{}z_{i}\}\;\tau)$
generates a function composition that computes the type encoding of
the exact run-time type instantiation of the static type $\tau$.

Similarly, the mechanism of interpreting the type encodings
$(\interpret\dlb\lbx{R}\drb\;\overline{\tau})$ can also be generalized
for an arbitrary schema \lbx{R} as shown in \fig{compint}. This
process unpacks the encoded type and invokes the schema function for
the appropriate type descriptor passing it the rest of the encoded
type arguments. In our present case,
$(\interpret\dlb\lbx{M}\drb\;\overline{\tau}\;x)$ traverses and marks
the object $x$ according to its exact run-time type encoding
$\overline{\tau}$ by recursively instantiating and invoking the mark
functions associated with the type descriptors in $\tau$.

In our current implementation, the type-code interpretation mechanism
of \fig{compint} is built into the run-time system. It directly
executes the marking specification of \fig{mark-schema} corresponding
to each class of datatypes given a run-time object $x$ and its
reconstructed run-time type encoding $\overline{\tau}$. No separate
marking functions are generated.  

The interpretive marking process starts up by examining the
frame-slots of every activation frame using the argument and the bound
identifier types from its reconstructed typemap. This process is
optimized based on the actual representation chosen for a particular
class of datatypes as shown in \fig{reptn}.  For example, the marking
function for linearized arrays computes the total size of the array
and marks each of its elements in a single loop. In case of algebraic
types, nullary disjuncts under enumerated or implicit representation
are never marked, a product disjunct is always marked, and a tag
dispatch is made for explicitly tagged disjuncts.  Finally, the hidden
arguments inside function closures are traversed and marked according
to their reconstructed hidden closure types.

%As an aside, it may be worth pointing out that the marking schema
%$\lbx{M}\dlb T^{n}\drb$ shown in \fig{mark-schema} constitutes an
%$\Omega$-\ibx{algebra} over the set of type constructors symbols
%$T^{n}$ of arity $n$. The type-directed compilation scheme
%$\compile\dlb\lbx{M}\drb\;\rho_{m}$ then constitutes a {\it semantic
%interpretation} (an $\Omega$-\ibx{homomorphism}) of the initial term
%algebra of types into the algebra of mark functions.  This
%formalization brings out the generality of our compiler-directed
%translation framework. A different semantic interpretation, for
%example, to an algebra of print functions, or I/O functions, may
%easily be generated using the same translation framework.

%\subsubsection{Run-time Encoding Schema}
%
%After the type reconstruction of an activation frame is over, the
%fully instantiated encoding of its typemap is converted
%into a suitable composition of mark functions by syntactically
%interpreting each encoded type descriptor $\overline{T^{n}}$ with its
%corresponding mark function $\lbx{M}\dlb T^{n}\drb$ as shown in
%\fig{code-schema}. The mark function so obtained is then applied to
%the current activation frame in order to traverse and mark all heap
%objects reachable from it.
%
%Again, it may be worth pointing out that $\interpret\dlb\lbx{M}\drb$
%computes a {\it syntactic interpretation\/} (another
%$\Omega$-{\it{}ho\-mo\-mor\-phism}) of terms from the algebra of type
%encodings into the algebra of mark functions. This alternate route of
%producing mark functions at run-time (generating type encodings and
%then interpreting them) can be verified using
%Figures~\ref{fig:mark-schema} and \ref{fig:code-schema} to be a simple
%homomorphism composition:
%\[\compile\dlb\lbx{M}\drb\;\rho_{m} =
%(\interpret\dlb\lbx{M}\drb)\circ(\compile\dlb\lbx{C}\drb\;\rho_{c})\]
%
%This composition expresses the correctness of interpreting the
%reconstructed type encodings to produce the marking functions desired
%at run-time.

\subsubsection{Compiled Marking}
\label{compmark}

Rather than interpreting type encodings as in our interpreted marking
schema, it is also possible to generate compiled marking functions for
each datatype that know how to traverse the object directly without
any type interpretation. In this {\em Compiled Marking Schema}
$\lbx{M}'$, for each datatype $T^{n}$ the compiler automatically
generates a mark function \tbx{mark$'\_T$} that is parameterized by
$n$ mark function arguments $f_{1}\cdots{}f_{n}$ instead of encoded
type arguments.

This alternate marking schema $\lbx{M}'$ can be directly obtained from
our interpreted marking schema \lbx{M} shown in \fig{mark-schema} by
replacing the recursive call for interpretation:
\[\interpret\dlb\lbx{M}\drb\;(\compile\dlb\lbx{C}\drb\;\{\alpha_{i}\mapsto{}z_{i}\}\;\tau)\]
by a type-based function composition:
\[(\compile\dlb\lbx{M}'\drb\;\{\alpha_{i}\mapsto{}f_{i}\}\;\tau)\]
This transformation expresses the fact that building the exact
run-time type encoding of an object and then interpreting it to guide
the traversal and marking is functionally equivalent to directly
traversing it using a compiled marking function that knows the
structure of that object. Note that marking functions so generated do
not contain any type-code interpretation. Their execution directly
results into the appropriate traversal and marking of the given
object.

The compiled marking process is initiated by converting the
reconstructed typemap of each activation frame into a composition of
compiler-generated marking functions. This translation is similar to
the type-based function composition shown in \fig{compint} except that
it operates on type encodings rather than static types. The resulting
function composition may be directly executed to mark all objects
reachable from the activation frame. The compiled marking schema is
currently unimplemented.

%the encoded types directly in order to
%traverse and mark the objects rather than to convert them into a
%composition of pre-compiled mark functions first. In this alternate
%scheme, the run-time system would unpack the type-code
%$\overline{T^{n}}$ as before and then emulate the appropriate mark
%function $\lbx{M}\dlb T^{n} \drb$ directly. At each recursive call to
%mark an array element or a constructor field, the interpreter would
%use the encoded type arguments to build the exact run-time encoded
%type of the object and then interpret that type to mark the contents
%of the object. 
%
%A little thought indicates that the above process can be described as
%an interpretation of the type encodings under an alternate marking
%schema $\overline{\lbx{M}}$, which is obtained from the compiled
%marking schema \lbx{M} by replacing 
%$(\compile\dlb\lbx{M}\drb\;\rho\;\tau)$ by
%$(\interpret\dlb\overline{\lbx{M}}\drb\;(\compile\dlb\lbx{C}\drb\;\rho\;\tau))$.
%The interpreted marking schema $\overline{\lbx{M}}$ so obtained
%defines equivalent mark functions $\overline{\lbx{M}}\dlb T^{n} \drb$
%that take type encodings as parameters rather than compiled mark
%functions.  The transformation of the compiled marking schema \lbx{M}
%into the interpreted marking schema $\overline{\lbx{M}}$ can be
%expressed as a homomorphic congruence:
%\[\compile\dlb\lbx{M}\drb\;\rho_{m} \cong
%(\interpret\dlb\overline{\lbx{M}}\drb)\circ(\compile\dlb\lbx{C}\drb\;\rho_{c})\]
%This congruence states that the compiled marking function produced by
%the marking schema \lbx{M} under a mark function environment
%$\rho_{m}$ is functionally equivalent to the interpretation of the
%encoded types at run-time under an encoded type environment
%$\rho_{c}$. It is this congruence that allows us to freely mix compiled
%marking functions along with direct interpretation of encoded types
%generated by run-time type reconstruction. 

