\documentclass[11pt]{article}
\setlength{\unitlength}{1 true cm}
\setlength{\oddsidemargin}{0 true mm}
\setlength{\evensidemargin}{\oddsidemargin}
\setlength{\textwidth}{160 true mm}
\setlength{\parindent}{5 true mm}
\setlength{\topmargin}{1 true mm}
\setlength{\headheight}{12 true pt}
\setlength{\headsep}{20 true pt}
\setlength{\textheight}{240 true mm}
\setlength{\footskip}{15 true mm}
\setlength{\voffset}{-10 true mm}
%\setlength{\footheight}{5 true mm}

\usepackage{prolog}

\title{Type--Inference in \javafive}
\author{J\"org B\"auerle, Markus Melzer, Martin Pl\"umicke\medskip\\
\small
University of Cooperative Education Stuttgart\\
  %Department of Information Technology\\
  %Florianstra{\ss}e 15\\
  %D--72160 Horb\\
  %tel. +49-7451-521142\\
  %fax. +49-7451-521190\\
\small m.pluemicke@ba-horb.de
}


\begin{document}
\bibliographystyle{alpha}
\maketitle
\section{Overview}
We have developed for \javafive a type inference system. This means that the
user can write programs without any type annotations and the system determines
the correct types. We have implemented a prototype for this
system. Furthermore we have implemented a plugin for the integrated development
environment \eclipse. 

\section{The Type Inference Algorithm}
Since then type inference in \oldjava similar languages is known as the
automatic parameter instantiation in polymorphic methods (local type inference)
\cite{PT00,OZZ01,MO02}. It is proved that this type inference is
unsound. Some techniques are presented, which solve these unsoundness.

We extend these approaches to a global variant, where additionally
the types of method parameters, methods' return types and the
types of local variables are determined automatically. The input of the algorithm
are only the types of the fields of the respective classes.

The type inference algorithm traverses the programming code as an abstract syntax
tree and forms sets of type inequations. As it is known that even the local
type inference is unsound, it is obvious that our approach is also unsound. We
deal with this problem, as we allow different type assumptions for the
parameters, the return type, the local variables, and the expressions of each
method, respectively. During traversing the set of type assumptions is adapted, such
that the set contains exactly the assumptions, which are possible assumptions at
the respective position during the traverse. The adaption is done by solving the
inequations as far as possible by a type unification algorithm
\cite{Plue04_1}. The type unification is not unitary but finitary. This means
that each unification step reduces the set of type assumptions if there is no
solution for one set of inequations. On the other hand the set of type assumptions is extended, if
there is more than one solution for a set of inequations.

The result of the type inference algorithm is the set of all correct
combinations of types of the parameters, the return type, and the local
variables. 

After the type inference step during the compilation, there are two possibilities. Either for each
combination of types of each method, byte code could be built,
respectively. This would lead to the property that method names, which are
declared only once, could be overloaded.
On the other hand one combination could
be selected. Then, for this combination of types byte code would be built. We
implemented the second possibility (cp. section \ref{sec:IDE}).

Furthermore, we have done comparisons to other type inference
approaches. We considered the 
type system of \textsf{Cecil} \cite{VL98}, which is a static type system 
providing type checking and local type inference. Furthermore we considered a
type system for a language oriented at \textsf{Smalltalk} \cite{PS91,
  PS94}. In this approach the types are computed by a least fixed point derivation.
In \cite{PC94} type inference for the language \textsf{Concurrent Aggregates} is
described, which contains a data flow analysis. Finally, we considered the type
system of \textsf{ocaml} \cite{CMP2000}. The approach of this type system
differs from our's, as  \textsf{ocaml} allows higher-order functions.

\section{Implementation}
We have done the implementation in \oldjava. The implementation consists of two
parts. First we describe the implementation of the type unification
algorithm. Then we present the implementation of the actual type inference via
code traverse. 

\subsection{Type Unification}
The implementation of the type unification \cite{TO04} contains as the main
datastructure a vector of type term pairs. The algorithm itself is
implemented as an extension of the usual unification algorithm. Pairs of
the form $a \olsub ty$ respectively $ty \olsub a$, where $a$ is a variable and
$ty$ is a term but no variable, generate multiple solutions.

\subsection{Type Inference}
The idea of the implementation of the actual type inference algorithm
\cite{JB05} is that each construct in a \javafive program (method, parameter,
return type, variable,  
expression) get first a variable as its type assumption. Then, for each variable a
type is determined by the algorithm.

There are two main datastructures.
The first one represents type assumptions for methods, fields, and
variables. During runtime a set of instances of this
datastructure represent the different possibilities of type assumptions. The
second main datastructure represents the substitutions of the variables to types,
calculated step by step.

During runtime each construct of the abstract syntax tree is registered
as a listener by the corresponding type variable. These registrations finally allow
to substitute the variables in the abstract syntax tree by the
calculated types.

\section{Integrated Development Environment (IDE)}
\label{sec:IDE}
For \javafive without explicite type declaration a plugin for \eclipse is
developed \cite{MM05}. The IDE allows to show all different correct
possibilities to give types to the methods, parameters, return types, and local
variables, which are determined by the type inference algorithm. Then, the user
can select the favored type for each construct step by step. Finally, the
selected types are substituted in the respective constructs of the abstract syntax
tree. 

\section{Summary and Outlook}
We have developed a system, which allows to give typeless \javafive
programs. The system calculates the correct types. The soundness problem is
solved such that all different possibilities are determined and the user
himself decides, which type should be used.

In the moment only a subset of \javafive is implemented. Interfaces and
F--bounded type parameters are not implemented yet. This should be done
henceforth. 
\bibliography{martin,SE}
\end{document}