% -*- Mode: LaTeX -*-

\section{Introduction}

In modern programming languages, high-level functional abstractions
are often implemented using low-level imperative operations either
directly within the compiler or separately within accompanying
libraries. The imperative implementations have obvious advantages in
terms of storage efficiency and avoiding data-copying overhead on
every update.  But arbitrary use of imperative constructs in a
functional program destroys its nice functional properties that
otherwise lead to powerful reasoning techniques and compiler
optimizations. In this paper, we propose a type system which provides
a reasonable solution to this problem in the context of the implicitly
parallel and mostly functional programming languages Id \cite{Id90.1}
and pH \cite{pH-doc} (a parallel version of Haskell \cite{Haskell90}). 

\subsection{The Problem}
\label{sec:problem}
Consider the problem of implementing {\em functional arrays} that are
homogeneous, non-mutable, polymorphic arrays.  The function
\tbx{make\_vector} creates a one dimensional functional array that
memoizes a computation for a given index range. A direct and efficient
way of implementing \tbx{make\_vector} is to allocate memory and then
fill it with the value of the computation function at each index:

\begin{myexample}{ex-make-vector-sol1}
make\_vector :: $\forall{}t.(\ibx{int}\rightarrow{}t)\rightarrow(\ibx{int},\ibx{int})\rightarrow(t\;\ibx{m\_vector})$
def make\_vector f (l,u) = 
   \{ a = alloc\_vector (l,u);
     \{for i <- l to u do
       a[i] := f i \}
   in a \};
\end{myexample}

The problem with providing the above definition in a standard library
as opposed to hard-coding it into the compiler is the following.
First, the above code is not functional and hence it is not
expressible in a functional language. Second, it returns a mutable
array of type $(t\;\ibx{m\_vector})$ instead of a functional array of
type $(t\;\ibx{vector})$.  There is no guarantee that the user will
not tamper with the contents of the array once it is returned.
Furthermore, in order to be sound, mutable objects must be restricted
in polymorphism \cite{Tofte90} which is not what we want
for fully polymorphic functional arrays.

In order to express the above code in a standard library, the language
must support an imperative kernel in which low-level imperative
operations such as memory allocation and assignment are permitted.
This means that the type system must have the capability to deal with
imperative objects and functions that create and manipulate such
objects in a sound manner. Furthermore, there must be a way to {\em
encapsulate} such imperative programs that guarantees that the
returned array \tbx{a} is non-mutable and is given a polymorphic
functional type.

\subsection{A Proposal for ``Close''}

There are many existing type systems in the literature that already
deal with the problem of extending the Hindley/Milner type system to
imperative objects
\cite{HMV93,Leroy92,Leroy91,SML90,Talpin92,Tofte90,Wright92}. Any
one of these may be used to support an imperative kernel language in a
type-safe manner. As for making the \tbx{make\_vector} function return
a functional array in Example~\ref{ex-make-vector-sol1}, we
introduce a {\em type conversion\/} operator called \tbx{close}:
\begin{myexample}{ex-make-vector-sol2}
make\_vector :: $\forall{}t.(\ibx{int}\rightarrow{}t)\rightarrow(\ibx{int},\ibx{int})\rightarrow(t\;\ibx{vector})$
def make\_vector f (l,u) =  close \{ \ldots \};
\end{myexample}
Now, the returned vector has a functional type which prohibits any
subsequent assignments from being performed over it.  In
general, the \tbx{close} operator can be used to convert arbitrary
non-functional data-structures like I-structures \cite{Arvind89} and
M-structures \cite{Barth92} into functional ones, retaining all the
advantages of using these data-structures inside the \tbx{close}'d
expression. The \tbx{close} operator delimits a well-defined {\em
control block} within which the user has full flexibility and the raw
power of an imperative language before exporting mutable
data-structures across its boundary and rendering them functional.

\subsection{Soundness Issues}

However, simply converting the type of the returned result from an
imperative program does not automatically ensure its non-mutability.
If the returned result somehow escapes the scope of the control block
in which it is being closed then that \tbx{close} operation is unsafe
because the returned object may be mutated even after it is assigned a
functional type. For example:

\begin{myexample}{ex-escape}
b = ref ...;
def escape\_1 n =
  close \{ a = alloc\_vector (1,n);
          ...
          b := a;                 \% \bx{Storing into an external data structure}
         in a \};
\vsp
def escape\_2 n = 
  close \{ a = alloc\_vector (1,n);
          ...
          def g i v =             \% \bx{Allowing a write handle to escape}
            \{ a[i] := v;
              in v \};
        in a,g \};
\end{myexample}

In function \tbx{escape\_1}, a reference to the locally allocated
imperative array \tbx{a} is stored into an external object \tbx{b}. The
type of the object \tbx{b} is constrained to be
$((t\;\ibx{m\_vector})\;\ibx{ref})$ implying that the array
\tbx{a} is still accessible in its open form through this indirection.
The same effect is achieved in the function \tbx{escape\_2}, although
it is disguised in the form of a function that provides a write handle
to the array being closed.  

\subsection{Our Work}

The goal of this paper is to design a type system that automatically
verifies the soundness of the type conversions implied by the
\tbx{close} operations provided by the user. Our type system closes a
polymorphic mutable data-structure only if it is guaranteed that no
write handle pointing to that object remains accessible to the user
after it is closed. Unsafe uses of the \tbx{close} operator such as
those in Example~\ref{ex-escape} are flagged as compile-time
``close-errors''. 

Note that \tbx{close} is purely a type domain operation, no run-time
copying is involved while doing this type conversion. Therefore, there
is no time or space overhead of using the \tbx{close} operation once
it has been verified by the type system. Also, this approach may yield
more parallelism because no single-threading constraint is imposed on
the underlying imperative program encapsulated within the \tbx{close}
operator. The following histogram example illustrates these
issues:\footnote{We use pattern-matching to destructure and dispatch
according to the shape of the given tree. In a parallel
implementation, the array increment is performed atomically and the
barrier ({\tt{}---}) prevents the final array from being released
before all the accumulations have finished.}

\begin{myexample}{ex-histogram}
type tree $t$ = leaf | node $t$ (tree $t$) (tree $t$);
\vsp
def histogram t n = 
 close \{ a = alloc\_vector (1,n);
         \{for i <- 1 to n do
            a[i] := 0 \};
         \_ = accum t a n;
         ---
        in a \};
\vsp
def accum leaf a n = ()
 |  accum (node x l r) a n = 
   \{ i = hash x n;
     a[i] := a[i] + 1;
     \_ = accum l a n;
     \_ = accum r a n; \};
\end{myexample}

In this example, a histogram of objects drawn from a binary tree is
accumulated into an array \tbx{a} which is closed and returned at the
end. No copying is involved during accumulations or at the time of
returning the final array.  Furthermore, the histogram initialization
and the entire tree accumulation can potentially be done in parallel.
Thus, the \tbx{close} construct enables returning a functional result
without any copying or restricting the parallelism inherent in the
underlying implementation.

From a practical standpoint, our type system provides a sound semantic
interface between high-level functional constructs of the language and
their imperative implementations in libraries. Furthermore, the
language is not restricted to a fixed set of functional constructs
built into the system; the users can program their own imperative
implementations of arbitrary functional data-structures and extend
existing ones using the type system without disturbing the compiler at
all. As illustrated above in Example~\ref{ex-histogram}, our type
system also enables implementing functional computations using
imperative algorithms that can not otherwise be expressed in a
functional style efficiently.

From a technical standpoint, we believe we have the first type system
which directly models imperative implementations of functional
data-structures along with a complete proof of its soundness. The main
result of this paper is the soundness theorem shown in \sec{soundness}
which provides the guarantee that well-typed terms in our system do
not run into dynamic type-errors. This directly implies that in a
type-correct program, it is not possible to mutate an object once it
is converted into a functional type.

\subsection{Related Work}

The {\em Closure Typing} system proposed by Leroy \cite{Leroy92} is
the basis of our work. This powerful type system was designed to
determine when type-generalization was safe in the presence of
side-effects.  Our contribution is adding {\em regions} to this type
system and recognizing that such a system has all the information
needed to express and verify type-coercions between imperative and
functional data-structures.

Effect systems \cite{Lucassen88,Talpin92,Wright92} are closely related
to our work. {\em Effects} and {\em regions} in this type system
describe the side effects that expression can have. Effect systems are
able to determine when it is safe to evaluate expressions in parallel
\cite{Lucassen88}, and when to permit type-generalization
\cite{Talpin92,Wright92}.  Although Talpin and Jouvelot
\cite{Talpin92} use regions to {\em mask} side-effects that are not
visible from outside, they do not convert imperative data-structures
into functional ones.  However, as it seems that their system is at
least as powerful as the closure typing system \cite{Leroy92}, we
conjecture that our system can be adapted to work in their framework.
We have chosen to work with the closure typing system because it
provides a direct relationship between types and actual structure of
objects and a simpler theoretical framework to deal with.

A different approach to integrate imperative and (lazy) functional
programming has been the focus of many recent papers
\cite{Guzman90,Swarup91,Wadler90,Odersky93,Bloss89,Sastry93,Hudak92,Launchbury94}.
These papers attempt to introduce assignments into a functional
language without destroying its strong functional properties (\eg, {\em
confluence} and {\em referential transparency}).  To preserve these
properties, they ensure that assignments in a program are {\em
single-threaded} \cite{Schmidt85} by means of type systems
\cite{Guzman90,Swarup91,Wadler90}, reduction rules \cite{Odersky93},
dataflow analysis \cite{Bloss89,Sastry93}, or data abstraction and monadic
function composition \cite{Hudak92,Launchbury94}.  Side-effect
analysis using regions, such as ours, is orthogonal to the techniques
given in these papers and such analysis could be used to make these
languages or type systems more permissive.  Our system inherits the
properties of the underlying imperative kernel and simply provides a
sound mechanism to encapsulate and convert mutable objects into
functional abstractions rather than enforcing additional functional
properties (\eg, confluence) on the underlying kernel.

\subsection{Outline}

The rest of the paper is organized as follows.  \sec{dynamic-semantics}
describes a small expression language and its operational semantics.
\sec{static-semantics} describes the type system proposed in this
paper. \sec{soundness} shows the soundness of the type system.
\sec{extensions} describes a few extensions to the basic type system
and \sec{conclusion} concludes.
