Intro to Challenges

TIforWildFJ.tex

@@ -47,11 +47,11 @@
 
 %\titlerunning{Dummy short title} %TODO optional, please use if title is longer than one line
 
-\author{Andreas Stadelmeier}{DHBW Stuttgart, Campus Horb, Germany}{a.stadelmeier@hb.dhbw-stuttgart.de}{}{}%TODO mandatory, please use full name; only 1 author per \author macro; first two parameters are mandatory, other parameters can be empty. Please provide at least the name of the affiliation and the country. The full address is optional. Use additional curly braces to indicate the correct name splitting when the last name consists of multiple name parts.
-
-\author{Martin Plümicke}{DHBW Stuttgart, Campus Horb, Germany}{pl@dhbw.de}{}{}
-
-\author{Peter Thiemann}{Universität Freiburg, Institut für Informatik, Germany}{thiemann@informatik.uni-freiburg.de}{}{}
+\author{Andreas Stadelmeier\inst{1}, Martin Plümicke\inst{1}, Peter Thiemann\inst{2}}%TODO mandatory, please use full name; only 1 author per \author macro; first two parameters are mandatory, other parameters can be empty. Please provide at least the name of the affiliation and the country. The full address is optional. Use additional curly braces to indicate the correct name splitting when the last name consists of multiple name parts.
+\institute{DHBW Stuttgart, Campus Horb, Germany\\
+\email{a.stadelmeier@hb.dhbw-stuttgart.de} \and
+Universität Freiburg, Institut für Informatik, Germany\\
+\email{thiemann@informatik.uni-freiburg.de}}
 
 \authorrunning{A. Stadelmeier and M. Plümicke and P. Thiemann} %TODO mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et al.'
 
@@ -60,7 +60,6 @@
 %\ccsdesc[500]{Software and its engineering~Language features}
 %\ccsdesc[300]{Software and its engineering~Syntax}
 
-\keywords{type inference, Java, subtyping, generics} %TODO mandatory; please add comma-separated list of keywords
 
 %\category{} %optional, e.g. invited paper
 
@@ -99,6 +98,7 @@
 \begin{abstract}
 TODO: Abstract
 \end{abstract}
+\keywords{type inference, Java, subtyping, generics} %TODO mandatory; please add comma-separated list of keywords
 
 \input{introduction}
 

introduction.tex

@@ -26,7 +26,6 @@
 % It's only restriction is that no polymorphic recursion is allowed.
 % \end{recap}
 
-
 \section{Type Inference for Java}
 - Type inference helps rapid development
 - used in Java already (var keyword)
@@ -57,6 +56,34 @@ are infered and inserted by our algorithm.
 %This paper extends a type inference algorithm for Featherweight Java \cite{TIforFGJ} by adding wildcards.
 %The last step to create a type inference algorithm compatible to the Java type system.
 
+
+\begin{figure}
+\begin{minipage}{0.43\textwidth}
+\begin{lstlisting}[style=java,label=lst:intro-example-typeless,caption=Missing return type]
+genList() {
+  if( ... ) {
+    return new List(1);
+  } else {
+    return new List("Str");
+  }
+}
+    \end{lstlisting}
+\end{minipage}%
+\hfill
+\begin{minipage}{0.55\textwidth}
+\begin{lstlisting}[style=tfgj,caption=Type inference solution,label=lst:intro-example-typed]
+List<?> genList() {
+  if( ... ) {
+    return new List<Integer>(1);
+  } else {
+    return new List<String>("Str");
+  }
+}
+    \end{lstlisting}
+\end{minipage}
+\end{figure}
+  
+
 \subsection{Comparision to similar Type Inference Algorithms}
 To outline the contributions in this paper we will list the advantages and improvements to smiliar type inference algorithms:
 \begin{description}
@@ -175,32 +202,6 @@ We prove soundness and aim for a good compromise between completeness and time c
 % \end{verbatim}
 
 
-\begin{figure}
-\begin{minipage}{0.43\textwidth}
-\begin{lstlisting}[style=java,label=lst:intro-example-typeless,caption=Missing return type]
-genList() {
-  if( ... ) {
-    return new List(1);
-  } else {
-    return new List("Str");
-  }
-}
-    \end{lstlisting}
-\end{minipage}%
-\hfill
-\begin{minipage}{0.55\textwidth}
-\begin{lstlisting}[style=tfgj,caption=Type inference solution,label=lst:intro-example-typed]
-List<?> genList() {
-  if( ... ) {
-    return new List<Integer>(1);
-  } else {
-    return new List<String>("Str");
-  }
-}
-    \end{lstlisting}
-\end{minipage}
-\end{figure}
-
 % \subsection{Wildcards}
 % Java subtyping involving generics is invariant.
 % For example \texttt{List<String>} is not a subtype of \texttt{List<Object>}.
@@ -467,8 +468,19 @@ a type parameter to method call \texttt{<X>add(v, "String")}.
 
 % do not substitute free type variables
 
-Lets have a look at a few challenges:
-\begin{itemize}
+Global Type inference for Featherweight Java with generics but without wildcards is solved already.
+But adding Wildcards to the calculus creates new problems we did not foresee
+and which have not been recognized by an existing type unification algorithm for Java with wildcards \ref{plue09_1}.
+% what is the problem?
+% Java does invisible capture conversion steps 
+Java Wildcard types are represented as existential types and have to be opened before they can be used.
+This can either be done implicitly (\cite{aModelForJavaWithWildcards}, \cite{javaTIisBroken}) or explicitly via let statements (\cite{WildcardsNeedWitnessProtection}).
+For all of those variations it is vital to know the argument types with which a method is called.
+But our input program does not contain any type annotations.
+We do not know where an existential type will emerge and where a capture conversion is necessary.
+This has to be figured out during the type inference algorithm.
+We detected three main challenges related to Java Wildcards and Global Type Inference:
+\begin{enumerate}
 \item \label{challenge:1}
 One challenge is to design the algorithm in a way that it finds a correct solution for the program shown in listing \ref{lst:addExample}
 and rejects the program in listing \ref{lst:concatError}.
@@ -618,6 +630,6 @@ $\ntv{z}$ is a normal placeholder and is not allowed to contain free variables.
 
 \end{example}
 
-\end{itemize}
+\end{enumerate}
 
 %TODO: Move this part. or move the third challenge some underneath.