141 lines
6.6 KiB
TeX
Executable File
141 lines
6.6 KiB
TeX
Executable File
\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 Menge 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}
|