introduction.tex

@@ -59,10 +59,8 @@ is scope for a global type inference algorithm that infers
 method signatures even if no type information (except class headers
 and types of field variables) is given.
 We present such a global type inference algorithm for Featherweight
-Generic Java with wildcards, a Java core calculus with generics and
+Generic Java with wildcards. The same approach can also be used for
-wildcards in the tradition of Featherweight Java \cite{FJ} and its
+regular Java programs. 
-extensions \cite{WildFJ,WildcardsNeedWitnessProtection}. Our approach can also be used for regular Java programs,
-but we limit the formal presentation to this core calculus.
 
 %The goal is to find a correct typing for a given Java program.
 Our algorithm enables programmers to write Java code with only a
@@ -71,17 +69,15 @@ variables), it can fill in missing type annotations in partially
 type-annotated programs, and it can suggest better (more general)
 types for ordinary, typed Java programs.
 
-Listing~\ref{lst:intro-example-typeless} shows an example input of a
-method implementation without any type annotation. Our algorithm
-infers the type annotations in Listing~\ref{lst:intro-example-typed}:
-it adds the type arguments to \texttt{List} at object creation and it
-infers the most specific return type \texttt{List<?>}, which is a
-wildcard type. Our algorithm is the first to infer wildcard types that
-comes with a soundness proof.
-Previous work on global type inference for Java either does not
-consider wildcards or it simplifies the problem by not modeling key
-features of Java wildcards.
 
+\textbf{TO BE CONTINUED}
+
+
+We propose a global type inference algorithm for Java supporting Wildcards and proven sound.
+Global type inference allows input programs without any type annotations.
+A programmer could write Java code without stressing about types and type annotations which
+are infered and inserted by our algorithm.
+%This leads to better types (Poster referenz)
 
 %The algorithm proposed in this paper can determine a correct typing for the untyped Java source code example shown in listing \ref{lst:intro-example-typeless}.
 %In this case our algorithm would also be able to propose a solution including wildcards as shown in listing \ref{lst:intro-example-typed}.
@@ -90,7 +86,7 @@ features of Java wildcards.
 %The last step to create a type inference algorithm compatible to the Java type system.
 
 
-\begin{figure}[tp]
+\begin{figure}
 \begin{minipage}{0.43\textwidth}
 \begin{lstlisting}[style=java,label=lst:intro-example-typeless,caption=Missing return type]
 genList() {
@@ -117,52 +113,57 @@ List<?> genList() {
 \end{figure}
   
 
-
+\subsection{Comparision to similar Type Inference Algorithms}
-Global Type Inference for Featherweight Java \cite{TIforFGJ} is a
+To outline the contributions in this paper we will list the advantages and improvements to smiliar type inference algorithms:
-sound, but incomplete inference algorithm for Featherweight Generic
+\begin{description}
-Java. It does not support wildcards, which means that it infers the
+    \item[Global Type Inference for Featherweight Java] \cite{TIforFGJ} is a predecessor to our algorithm.
-return type \texttt{Object} for the method \texttt{genList} in
+The type inference algorithm presented here supports Java Wildcards.
-Listing~\ref{lst:intro-example-typeless}. Like our algorithm, their
+% Proven sound on type rules of Featherweight Java, which are also proven to produce sound programs
-algorithm restricts to monomorphic recursion, which leads to
+% implication rules that follow the subtyping rules directly. Easy to understand soundness proof
-incompleteness. 
+% capture conversion is needed
-
+\textit{Example:} The type inference algorithm for Generic Featherweight Java produces \texttt{Object} as the return type of the
-
+\texttt{genBox} method in listing \ref{lst:intro-example-typeless}
-A type unification algorithm for Java with wildcards \cite{plue09_1} states the same capabilities,
+whereas our type inference algorithm will infer the type solution shown in listing \ref{lst:intro-example-typed}
-but it does not handle capture conversion correctly because it only supports types which are expressible in Java syntax (more details in
+involving a wildcard type.
-section~\ref{challenges}).  
+\item[Type Unification for Java with Wildcards]
-Moreover, it appears that the subtype relation changes depending on whether a type is used as an argument to a method invocation.
+An existing unification algorithm for Java with wildcards \cite{plue09_1} states the same capabilities,
-We resolve this problem by modeling Java wildcards as existential
+but exposes some errors when it comes to method invocations.
-types \cite{WildFJ,WildcardsNeedWitnessProtection}, which also serve
+Especially the challenges shown in chapter \ref{challenges} are handled incorrectly.
-as the basis of our soundness proof.
+The main reasons are that Plümickes algorithm only supports types which are expressible in Java syntax
-% forces us to define a new kind of subtype constraint. %, the current state of the art
+and its soundness is proven towards a self-defined subtype ordering, but never against a complete type system.
+It appears that the subtype relation changes depending on whether a type is used as an argument to a method invocation.
+We resolve this by denoting Java wildcards as existential types
+and introducing a second kind of subtype constraint. %, the current state of the art
 %and is able to deal with types that are not directly denotable in Java. 
-
+Additionally the soundness of our algorithm is proven using a Featherweight Java calculus \cite{WildFJ}.
 
 %The algorithm presented in this paper is able to solve all those challenges correctly
 %and it's correctness is proven using a Featherweight Java calculus \cite{WildFJ}.
 %But they are all correctly solved by our new type inference algorithm presented in this paper.
 
-
+\item[Java Type Inference]
-\begin{lstlisting}[caption=Part of a valid Java program, style=tfgj, label=lst:tiExample,float=tp]
+Standard Java provides type inference in a restricted form % namely {Local Type Inference}.
+which only works for local environments where the surrounding context has known types.
+But our global type inference algorithm is able to work on input programs which do not hold any type annotations at all.
+We will show the different capabilities with an example.
+In listing \ref{lst:tiExample} the method call \texttt{emptyList} is missing
+its type parameters.
+Java is using a matching algorithm \cite{javaTIisBroken} to replace \texttt{T} with \texttt{String} 
+resulting in the correct expected type \texttt{List<String>}.
+%The invocation of \texttt{emptyList} missing type parameters can be added by Java's local type inference
+%because the expected return type is known. \texttt{List<String>} in this case.
+\begin{lstlisting}[caption=Extract of a valid Java program, label=lst:tiExample]
 <T> List<T> emptyList() { ... }
 
 List<String> ls = emptyList();
 \end{lstlisting}
-Standard Java provides type inference in a restricted form % namely {Local Type Inference}.
+
-which only works for local environments where the surrounding context has known types.
+%\textit{Local Type Inference limitations:}
-The example in Listing~\ref{lst:tiExample} exhibits the main differences to our global type inference algorithm.
+Note that local type inference depends on the type annotation on the left side of the assignment.
-The method call \texttt{emptyList} lacks its type parameters.
+When calling the \texttt{emptyList} method without this type context its return value will be set to a \texttt{List<Object>}.
-Java relies on a matching algorithm \cite{javaTIisBroken} to instantiate \texttt{T} with \texttt{String} 
+The Java code snippet in \ref{lst:tiLimit} is incorrect, because \texttt{emptyList()} returns
-resulting in the correct expected type \texttt{List<String>}.
+a \texttt{List<Object>} instead of the required $\exptype{List}{\exptype{List}{String}}$.
-This local type inference depends on the type annotation on the left side of the assignment.
+\begin{lstlisting}[caption=Limitations of Java's Type Inference, label=lst:tiLimit]
-When calling the \texttt{emptyList} method without this type context
-its return value will be inferred as \texttt{List<Object>}.
-Therefore, Java rejects the code snippet in Listing~\ref{lst:tiLimit}:
-it infers the type  \texttt{List<Object>} for
-\texttt{emptyList()} instead of the required
-$\exptype{List}{\exptype{List}{String}}$. 
-\begin{lstlisting}[caption=Limitations of Java's Type Inference,
-  label=lst:tiLimit, float=tp]
 emptyList().add(new List<String>())
     .get(0)
     .get(0); //Typing Error
@@ -171,12 +172,14 @@ emptyList().add(new List<String>())
 %List<A> <: List<B>, B <: List<C> 
 % B = A and therefore A on the left and right side of constraints.
 % this makes matching impossible
-Hence, the second call to \texttt{get} produces a type error.
+The second call to \texttt{get} produces a type error, because Java expects \texttt{emptyList} to return
-
+a \texttt{List<Object>}.
-The type inference algorithm presented in this paper correctly instantiates the type parameter \texttt{T} of the \texttt{emptyList}
+The type inference algorithm presented in this paper will correctly replace the type parameter \texttt{T} of the \texttt{emptyList}
-method with \texttt{List<List<String>>} and render this code snippet correct.
+method with \texttt{List<List<String>>} and proof this code snippet correct.
-
+The local type inference algorithm based on matching cannot produce this solution.
+Here our type inference algorithm based on unification is needed.
 
+\end{description}
 % %motivate constraints: 
 % To solve this example our Type Inference algorithm will create constraints
 % $
@@ -194,20 +197,20 @@ method with \texttt{List<List<String>>} and render this code snippet correct.
 % - Easy to implement
 % - Capture Conversion support
 % - Existential Types support
-We summarize our contributions:
+Our contributions are
 \begin{itemize}
 \item
-We introduce the language \tifj{} (section \ref{sec:tifj}), 
+We introduce the language \tifj{} (chapter \ref{sec:tifj}).
-a Featherweight Java derivative including generics, wildcards, and type inference.
+A Featherweight Java derivative including Generics, Wildcards and Type Inference.
 \item
-  Our algorithm handles existential types in a form which is not
+We support capture conversion and Java style method calls.
-  denotable by Java syntax \cite{aModelForJavaWithWildcards}. Thus, we support capture conversion and Java style method calls.
+This requires existential types in a form which is not denotable by Java syntax \cite{aModelForJavaWithWildcards}.
 \item
-  We present a novel approach to deal with existential types and capture conversion during constraint unification.
+We present a novel approach to deal with existential types and capture conversion during constraint unification.
-% \item The algorithm is split in two parts. A constraint generation step and an unification step.
+\item The algorithm is split in two parts. A constraint generation step and an unification step.
-% Input language and constraint generations can be extended without altering the unification part.
+Input language and constraint generations can be extended without altering the unification part.
 \item
-  We prove soundness and aim for a good compromise between completeness and time complexity.
+We prove soundness and aim for a good compromise between completeness and time complexity.
 \end{itemize}
 % Our algorithm finds a correct type solution for the following example, where the Java local type inference fails:
 % \begin{verbatim}
@@ -237,25 +240,25 @@ a Featherweight Java derivative including generics, wildcards, and type inferenc
 % The type inference algorithm has to find the correct type involving wildcards (\texttt{List<?>}).
 
 \section{Java Wildcards}
-\label{sec:java-wildcards}
 
-As Java is an imperative language, subtyping for generic types is invariant.
+Java has invariant subtyping for polymorphic types.
 %but it incooperates use-site variance via so called wildcard types.
-Even though \texttt{String} is subtype of \texttt{Object},
+A \texttt{List<String>} is not a subtype of \texttt{List<Object>}
-a \texttt{List<String>} is not a subtype of \texttt{List<Object>}:
+even though it seems intuitive with \texttt{String} being a subtype of \texttt{Object}.
-because someone might store an  \texttt{Integer} in the list, which is
+To make the type system more expressive Java incooperates use-site variance by allowing wildcards (\texttt{?}) in type annotations.
-compatible with \texttt{Object}, but not with \texttt{String} (see Listing~\ref{lst:invarianceExample}).
+For example a type \texttt{List<?>} (short for \texttt{List<? extends Object>}, with \texttt{?} being a placeholder for any type) %with the wildcard \texttt{?} representing a placeholder for any type
-
-Invariance is overly restrictive in read-only or write-only
-contexts. Hence, Java incooperates use-site variance by allowing wildcards (\texttt{?}) in types.
-For example, the type \texttt{List<?>} (short for \texttt{List<? extends Object>}, with \texttt{?} being a placeholder for any type)
 is a supertype of \texttt{List<String>} and \texttt{List<Object>}.
 %The \texttt{?} is a wildcard type which can be replaced by any type as needed.
-%
-Listing~\ref{lst:wildcardIntro} shows a use of wildcards that renders the assignment \texttt{lo = ls} correct.
-The program still does not compile, because the addition of an \texttt{Integer} to \texttt{lo} is still incorrect.
 
-\begin{figure}[tp]
+%Class instances in Java are mutable and passed by reference.
+Subtyping must be invariant in Java otherwise the integrity of data classes like \texttt{List} cannot be guaranteed.
+See listing \ref{lst:invarianceExample} for example
+where an \texttt{Integer} would be added to a list of \texttt{String}
+if not for the Java type system which rejects the assignment \texttt{lo = ls}.
+Listing \ref{lst:wildcardIntro} shows the use of wildcards rendering the assignment \texttt{lo = ls} correct.
+The program still does not compile, because now the addition of an Integer to \texttt{lo} is rightfully deemed incorrect by Java.
+
+\begin{figure}
 \begin{minipage}{0.48\textwidth}
 \begin{lstlisting}[caption=Java Invariance Example,label=lst:invarianceExample]{java}
 List<String> ls = ...;
@@ -275,13 +278,14 @@ lo.add(new Integer(1)); // error!
 \end{minipage}
 \end{figure}
 
-Wildcard types like \texttt{List<?>} are virtual types, i.e., the run-time 
+Wildcard types are virtual types.
-type of an object is always a fully instantiated type like
+There is no instantiation of a \texttt{List<?>}.
+It is a placeholder type which can hold any kind of list like
 \texttt{List<String>} or \texttt{List<Object>}.
-The issue is that the run-time type underlying a wildcard type can
+This type can also change at any given time, for example when multiple threads
-change at any time, for example when multiple threads share a reference to the same field.
+share a reference to the same field.
-Hence, a wildcard \texttt{?} must be considered a different type everytime it is accessed.
+A wildcard \texttt{?} must be considered a different type everytime it is accessed.
-For that reason, the  call to the method \texttt{concat} with two wildcard lists in Listing~\ref{lst:concatError} is rejected.
+Therefore calling the method \texttt{concat} with two wildcard lists in the example in listing \ref{lst:concatError} is incorrect.
 % The \texttt{concat} method does not create a new list,
 % but adds all elements from the second argument to the list given as the first argument.
 % This is allowed in Java, because both lists are of the polymorphic type \texttt{List<X>}.
@@ -289,52 +293,50 @@ For that reason, the  call to the method \texttt{concat} with two wildcard lists
 % if Java would treat \texttt{?} as a regular type and instantiate the type variable \texttt{X}
 % of the \texttt{concat} function with \texttt{?}.
 
-\begin{figure}[tp]
+\begin{figure}
 \begin{lstlisting}[caption=Wildcard Example with faulty call to a concat method,label=lst:concatError]{java}
 <X> List<X> concat(List<X> l1, List<X> l2){
     return l1.addAll(l2);
 }
 
-List<?> l1 = new List<String>("foo");
+List<String> ls = new List<String>();
+
+List<?> l1 = ls;
 List<?> l2 = new List<Integer>(1); // List containing Integer
 
 concat(l1, l2); // Error! Would concat two different lists
 \end{lstlisting}
 \end{figure}
 
-To determine the correctness of method calls involving wildcard types Java's typechecker
+To determine the correctness of method calls involving wildcard types Java's typecheck
-makes use of a concept called \textbf{capture conversion}.
+makes use of a concept called \textbf{Capture Conversion}.
 %  was designed to make Java wildcards useful.
 % - without capture conversion 
 % - is used to open wildcard types
 % - 
-One way to formalize this concept is by replacing wildcards with
+This process was formalized for Featherweight Java \cite{FJ} by replacing existential types with wildcards and capture conversion with let statements \cite{WildcardsNeedWitnessProtection}.
-existential types and modeling capture conversion with suitably
+We propose our own Featherweight Java derivative called \TamedFJ{} defined in chapter \ref{sec:tifj}.
-inserted let statements \cite{WildcardsNeedWitnessProtection}. 
+To express the example in listing \ref{lst:wildcardIntro} with our calculus we first have to translate the wildcard types:
-Our Featherweight Java derivative called \TamedFJ{} is modeled after
+\texttt{List<? extends Object>} becomes $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$.
-Bierhoff's calculus \cite{WildcardsNeedWitnessProtection} (see section~\ref{sec:tifj}).
+The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound,
-To express the example in Listing~\ref{lst:wildcardIntro} in our calculus we first translate the wildcard types:
+and a type they are bound to.
-\texttt{List<? extends Object>} becomes
+In this case the name is $\rwildcard{A}$ with the upper bound $\type{Object}$ and it's bound to the the type \texttt{List}.
-$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$,
+Before we can call the \texttt{add} method on this type we have to add a capture conversion via let statement:
-where the existentially bound variable \texttt{A} has a lower bound
-$\bot$ and an upper bound $\type{Object}$.
-Before we can call the \texttt{add} method on this type we perform
-capture conversion by inserting a let statement:
 \begin{lstlisting}
 let v : (*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$@*) = lo in v.<A>add(new Integer(1));
 \end{lstlisting}
-The variable \expr{lo} (from Listing~\ref{lst:wildcardIntro}) is
+\expr{lo} is assigned to a new variable \expr{v} bearing the type $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$,
-assigned to a new immutable variable \expr{v} with type
+but inside the let statement the variable \expr{v} will be treated as $\exptype{List}{\rwildcard{A}}$.
-$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$, 
+The idea is that every Wildcard type is backed by a concrete type.
-but inside the let statement the variable \expr{v} will be treated as
+By assigning \expr{lo} to a immutable variable \expr{v} we unpack the concrete type $\exptype{List}{\rwildcard{A}}$
-$\exptype{List}{\rwildcard{A}}$. 
+that was concealed by \expr{lo}'s existential type.
-Here $\rwildcard{A}$ is a fresh variable or a captured wildcard.
+Here $\rwildcard{A}$ is a fresh variable or a captured wildcard so to say.
-The only information we have about $\rwildcard{A}$ is that it is a
+The only information we have about $\rwildcard{A}$ is that it is any type inbetween the bounds $\bot$ and $\type{Object}$
-supertype of $\bot$ and a subtype of $\type{Object}$
 It is important to give the captured wildcard type $\rwildcard{A}$ an unique name which is used nowhere else.
-This approach also clarifies why the method call to \texttt{concat}
+With this formalization it gets obvious why the method call to \texttt{concat}
-in listing \ref{lst:concatError} is rejected (see Listing~\ref{lst:concatTamedFJ}).
+in listing \ref{lst:concatError} is irregular (see \ref{lst:concatTamedFJ}).
-\begin{figure}[tp]
+
+\begin{figure}
 \begin{lstlisting}[style=TamedFJ,caption=\TamedFJ{} representation of the concat call from listing \ref{lst:concatError}, label=lst:concatTamedFJ]
 let l1' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l1 in
     let l2' : (*@$\wctype{\rwildcard{Y}}{List}{\exptype{List}{\rwildcard{Y}}}$@*) = l2 in