Introduction Wildcards

introduction.tex

@@ -16,6 +16,40 @@ The \fjtype{} algorithm calculates constraints based on this intermediate repres
 which are then solved by the \unify{} algorithm
 resulting in a correctly typed program (see figure \ref{fig:nested-list-example-typed}).
 
+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}.
+The algorithm is able find the correct type for the method \texttt{m} in the following example:
+\begin{verbatim}
+    <X> Pair<X,X> make(List<X> l)
+    Boolean compare(Pair<X,X> p)
+
+    List<?> b;
+    Boolean m() = this.compare(this.make(b));
+\end{verbatim}
+
+
+We present a novel approach to deal with existential types and capture conversion during constraint unification.
+The algorithm is split in two parts. A constraint generation step and an unification step.
+
+We proof soundness and aim for a good compromise between completeness and time complexity.
+Our algorithm finds a correct type solution for the following example, where the Java local type inference fails:
+\begin{verbatim}
+class SuperPair<A,B>{
+    A a;
+    B b;
+}
+class Pair<A,B> extends SuperPair<B,A>{
+    A a;
+    B b;
+
+    <X> X choose(X a, X b){ return b; }
+
+    String m(List<? extends Pair<Integer, String>> a, List<? extends Pair<Integer, String>> b){
+        return choose(choose(a,b).value.a,b.value.b);
+    }
+}
+\end{verbatim}
+
 \begin{figure}[tp]
       \begin{subfigure}[t]{\linewidth}
 \begin{lstlisting}[style=fgj]
@@ -126,7 +160,17 @@ List<?> genList() {
 % \texttt{List<Object>} is not a valid return type for the method \texttt{genList}.
 % The type inference algorithm has to find the correct type involving wildcards (\texttt{List<?>}).
 
+\subsection{Global Type Inference}
+A global type inference algorithm works on an input with no type annotations at all.
+%TODO: Describe global type inference and lateron why it is so hard to 
+
 \subsection{Java Wildcards}
+Wildcards are expressed by a \texttt{?} in Java and can be used as parameter types.
+Wildcards can be formalized as existential types \cite{WildFJ}.
+\texttt{List<? extends Object>} and \texttt{List<? super String>} are both wildcard types
+denoted in our syntax by $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$ and
+$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
+
 Wildcards add variance to Java type parameters.
 In Java 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}.
@@ -137,11 +181,66 @@ means \texttt{List<String>} is a subtype of \texttt{List<? extend Object>}.
 The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound at the same time,
 and a type they are bound to.
 In this case the name is $\rwildcard{X}$ and it's bound to the the type \texttt{List}.
+
+Those properties are needed to formalize capture conversion.
+Polymorphic method calls need to be wraped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}.
+In Java this is done implicitly in a process called capture conversion.
+When calling a polymorphic method like \texttt{<X> List<X> m(List<X> l1, List<X> l2)} with a \texttt{List<?>}
+it is not possible to substitute \texttt{?} for \texttt{X}.
+This would lead to the method header \texttt{List<?> m(List<?> l1, List<?> l2)}
+where now a method invocation with \texttt{List<String>} and \texttt{List<Integer>} would be possible,
+because both are subtypes of \texttt{List<?>}.
+Capture conversion solves this problem by generating a fresh type variable for every wildcard.
+Calling \texttt{<X> X head(List<X> l1)} with the type \texttt{List<?>} ($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$)
+creates a fresh type variable $\rwildcard{Y}$ resulting in 
+$\generics{\rwildcard{Y}}\texttt{head}(\exptype{List}{\rwildcard{Y}})$
+with $\rwildcard{Y}$ being used as generic parameter \texttt{X}.
+The $\rwildcard{Y}$ in $\exptype{List}{\rwildcard{Y}}$ is a free variable now.
+
+%TODO: Read taming wildcards and see if we solve some of the problems presented in section 5 and 6
+
 % Additionally they can hold a upper or lower bound restriction like \texttt{List<? super String>}.
 % Our representation of this type is: $\wctype{\wildcard{X}{\type{String}}{\type{Object}}}{List}{\rwildcard{X}}$
 % Every wildcard has a name ($\rwildcard{X}$ in this case) and an upper and lower bound (respectively \texttt{Object} and \texttt{String}).
 
+% \subsection{Extensibility} % NOTE: this thing is useless, because final local variables do not need to contain wildcards
+% In \cite{WildcardsNeedWitnessProtection} capture converson is made explicit with \texttt{let} statements.
+% We chain let statements in a way that emulates Java behaviour. Allowing the example in \cite{aModelForJavaWithWildcards}
+% % TODO: Explain the advantage of constraints and how we control the way capture conversion is executed
+% But it would be also possible to alter the constraint generation step to include additional features.
+% Final variables or effectively final variables could be expressed with a 
+% \begin{verbatim}
+% <X> concat(List<X> l1, List<X> l2){...}
+% \end{verbatim}
+% \begin{minipage}{0.50\textwidth}
+% Java:
+% \begin{verbatim}
+% final List<?> l = ...;
+% concat(l, l);
+% \end{verbatim}
+% \end{minipage}%
+% \begin{minipage}{0.50\textwidth}
+% Featherweight Java:
+% \begin{verbatim}
+% let l : X.List<X> = ... in
+%     concat(l, l)
+% \end{verbatim}
+% \end{minipage}
+
+
+
+
 \subsection{Challenges}\label{challenges}
+%TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
+
+
+One problem is the divergence between denotable and expressable types in Java \cite{semanticWildcardModel}.
+A wildcard in the Java syntax has no name and is bound to its enclosing type.
+\texttt{List<List<?>>} equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
+During type checking intermediate types like $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$
+or $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ can emerge, which have no equivalent in the Java syntax.
+Our type inference algorithm uses existential types internally but spawns type solutions compatible with Java.
+
 
 The introduction of wildcards adds additional challenges.
 % we cannot replace every type variable with a wildcard