From c714d49677d8441b358e8d58da24240451a81079 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Tue, 28 May 2024 16:15:22 +0200
Subject: [PATCH] Intro to Challenges

---
 introduction.tex | 72 ++++++++++++++++++++++++++++--------------------
 1 file changed, 42 insertions(+), 30 deletions(-)

diff --git a/introduction.tex b/introduction.tex
index 4aa929b..f689f3f 100644
--- a/introduction.tex
+++ b/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.