%TODO:
% -Explain <c
% - Kapitel 1.2 + 1.3 ist noch zu komplex
% - Constraints und Unifikation erklären, bevor Unifikation erwähnt wird

%Inhalt:
% Global type inference example (the sameList example)
% Wildcards are needed because Java has side effects
% Capture Conversion
% Explain difference between local and global type inference


% \begin{recap}\textbf{TI for FGJ without Wildcards:}
% \TFGJ{} generates subtype constraints $(\type{T} \lessdot \type{T})$ consisting of named types and type placeholders.
% For example the method invocation \texttt{concat(l, new Object())} generates the constraints
% $\tv{l} \lessdot \exptype{List}{\tv{a}}, \type{Object} \lessdot \tv{a}$.
% Subtyping without the use of wildcards is invariant \cite{FJ}:
% Therefore the only possible solution for the type placeholder $\tv{a}$ is $\tv{a} \doteq \type{Object}$. % in Java and Featherweight Java.
% The correct type for the variable \texttt{l} is $\exptype{List}{\type{Object}}$ (or a direct subtype).
% %- usually the type of e must be subtypes of the method parameters
% %- in case of a polymorphic method: type placeholders resemble type parameters
% The type inference algorithm for Featherweight Generic Java \cite{TIforFGJ} (called \TFGJ{}) is complete and sound:
% It is able to find a type solution for a Featherweight Generic Java program, which has no type annotations at all,
% if there is any.
% 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)
- keeps source code clean

Java comes with a local type inference algorithm
used for lambda expressions, method calls, and the \texttt{var} keyword.

A type inference algorithm that is able to recreate any type annotation
even when no type information is given at all is called a global type inference algorithm.
The global type inference algorithm presented here is able to deal with all Java types including wildcard types.
It can also be used for regular Java programs.

%The goal is to find a correct typing for a given Java program.
Type inference for Java has many use cases and could be used to help programmers by inserting correct types for them,
finding better type solutions for already typed Java programs (for example more generical ones),
or allowing to write typeless Java code which is then type inferred and thereby type checked by our algorithm.

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}.

%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.

\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}
    \item[Global Type Inference for Featherweight Java] \cite{TIforFGJ} is a predecessor to our algorithm.
The type inference algorithm presented here supports Java Wildcards.
% Proven sound on type rules of Featherweight Java, which are also proven to produce sound programs
% implication rules that follow the subtyping rules directly. Easy to understand soundness proof
% 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}
whereas our type inference algorithm will infer the type solution shown in listing \ref{lst:intro-example-typed}
involving a wildcard type.
\item[Type Unification for Java with Wildcards]
An existing unification algorithm for Java with wildcards \cite{plue09_1} states the same capabilities,
but exposes some errors when it comes to method invocations.
Especially the challenges shown in chapter \ref{challenges} are handled incorrectly.
The main reasons are that Plümickes algorithm only supports types which are expressible in Java syntax
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]
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}

%\textit{Local Type Inference limitations:}
Note that local type inference depends on the type annotation on the left side of the assignment.
When calling the \texttt{emptyList} method without this type context its return value will be set to a \texttt{List<Object>}.
The Java code snippet in \ref{lst:tiLimit} is incorrect, because \texttt{emptyList()} returns
a \texttt{List<Object>} instead of the required $\exptype{List}{\exptype{List}{String}}$.
\begin{lstlisting}[caption=Limitations of Java's Type Inference, label=lst:tiLimit]
emptyList().add(new List<String>())
    .get(0)
    .get(0); //Typing Error
\end{lstlisting}
%List<String> <. A
%List<A> <: List<B>, B <: List<C> 
% B = A and therefore A on the left and right side of constraints.
% this makes matching impossible
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 will correctly replace the type parameter \texttt{T} of the \texttt{emptyList}
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
% $
% \exptype{List}{\tv{a}} \lessdot \tv{b},
% \tv{b} \lessdot \exptype{List}{\tv{c}},
% \tv{c} \lessdot \exptype{List}{\tv{d}}
% $



%\subsection{Conclusion}
% Additions: TODO
% - Global Type Inference Algorithm, no type annotations are needed
% - Soundness Proof 
% - Easy to implement
% - Capture Conversion support
% - Existential Types support
Our contributions are
\begin{itemize}
\item
We introduce the language \tifj{} (chapter \ref{sec:tifj}).
A Featherweight Java derivative including Generics, Wildcards and Type Inference.
\item
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.
\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.
\item
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}
% 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}
\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>}.
% %Wildcards introduce variance by allowing \texttt{List<String>} to be a subtype of \texttt{List<?>}.

% \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<?>}).

\section{Java Wildcards}

Java has invariant subtyping for polymorphic types.
%but it incooperates use-site variance via so called wildcard types.
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}.
To make the type system more expressive Java incooperates use-site variance by allowing wildcards (\texttt{?}) in type annotations.
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
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.

%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 = ...;
List<Object> lo = ...;
lo = ls; // typing error!
lo.add(new Integer(1));
\end{lstlisting}
\end{minipage}
\hfill
\begin{minipage}{0.5\textwidth}
\begin{lstlisting}[caption=Use-Site Variance Example,label=lst:wildcardIntro]{java}
List<String> ls = ...;
List<? extends Object> lo = ...;
lo = ls; // correct
lo.add(new Integer(1)); // error!
\end{lstlisting}
\end{minipage}
\end{figure}

Wildcard types are virtual types.
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>}.
This type can also change at any given time, for example when multiple threads
share a reference to the same field.
A wildcard \texttt{?} must be considered a different type everytime it is accessed.
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>}.
% As shown in listing \ref{lst:concatError} this leads to a inconsistent \texttt{List<String>}
% 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}
\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<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 typecheck
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
% - 
This process was formalized for Featherweight Java \cite{FJ} by replacing existential types with wildcards and capture conversion with let statements \cite{WildcardsNeedWitnessProtection}.
We propose our own Featherweight Java derivative called \TamedFJ{} defined in chapter \ref{sec:tifj}.
To express the example in listing \ref{lst:wildcardIntro} with our calculus we first have to translate the wildcard types:
\texttt{List<? extends Object>} becomes $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$.
The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound,
and a type they are bound to.
In this case the name is $\rwildcard{A}$ with the upper bound $\type{Object}$ and it's bound to the the type \texttt{List}.
Before we can call the \texttt{add} method on this type we have to add a capture conversion via 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}
\expr{lo} is assigned to a new variable \expr{v} bearing the type $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$,
but inside the let statement the variable \expr{v} will be treated as $\exptype{List}{\rwildcard{A}}$.
The idea is that every Wildcard type is backed by a concrete type.
By assigning \expr{lo} to a immutable variable \expr{v} we unpack the concrete type $\exptype{List}{\rwildcard{A}}$
that was concealed by \expr{lo}'s existential type.
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 any type inbetween the bounds $\bot$ and $\type{Object}$
It is important to give the captured wildcard type $\rwildcard{A}$ an unique name which is used nowhere else.
With this formalization it gets obvious why the method call to \texttt{concat}
in listing \ref{lst:concatError} is irregular (see \ref{lst:concatTamedFJ}).

\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
        concat(l1', l2') // Error!
\end{lstlisting}
\end{figure}

% % TODO intro to Featherweight Java
% is a formal model of the Java programming language reduced to a core set of instructions.
% - We extend this model by existential types and let expressions.
% - We copy this from \ref{WildFJ} but make type annotations optional
% - Our calculus is called \TamedFJ{}
% - \TamedFJ{} binds every method argument with a let statement.

% To enable the use of wildcards in argument types of a method invocation
% Java uses a process called \textit{Capture Conversion}.
% This behaviour is emulated by our language \TamedFJ{};
% a Featherweight Java \cite{FJ} derivative with added wildcard support
% and a global type inference feature (syntax definition in section \ref{sec:tifj}).
% %\TamedFJ{} is basically the language described by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection} with optional type annotations.
% Let's have a look at a representation of the \texttt{add} call from the last line in listing \ref{lst:wildcardIntro} with our calculus \TamedFJ{}:
% %The \texttt{add} call in listing \ref{lst:wildcardIntro} needs to be encased by a \texttt{let} statement in our calculus.
% %This makes the capture converion explicit.
% \begin{lstlisting}
% let v : (*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$@*) = lo in v.<A>add(new Integer(1));
% \end{lstlisting}
% The method call is encased in a \texttt{let} statement and
% \expr{lo} is assigned to a new variable \expr{v} of \linebreak[2]
% \textbf{Existential Type} $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$.
% Our calculus uses existential types \cite{WildFJ} to formalize wildcards:
% \texttt{List<? extends Object>} is translated to $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$
% and \texttt{List<? super String>} is expressed as $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
% The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound,
% and a type they are bound to.
% In this case the name is $\rwildcard{A}$ and it's bound to the the type \texttt{List}.
% Inside the \texttt{let} statement the variable \expr{v} has the type
% $\exptype{List}{\rwildcard{A}}$.
% This is an explicit version of \linebreak[2]
% \textbf{Capture Conversion},
% which makes use of the fact that a concrete type must be behind every wildcard type.
% There is no instantiation of a \texttt{List<?>},
% but there exists some unknown type $\exptype{List}{\rwildcard{A}}$, with $\rwildcard{A}$ inbetween the bounds $\bot$ (bottom type, subtype of all types) and
% \texttt{Object}.
% Inside the body of the let statement \expr{v} is treated as a value with the constant type $\exptype{List}{\rwildcard{A}}$.
% Existential types enable us to formalize \textit{Capture Conversion}.
% Polymorphic method calls need to be wrapped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}.
% In Java this is done implicitly in a process called capture conversion (as proposed in Wild FJ \cite{WildFJ}).


\section{Global Type Inference Algorithm}

\begin{figure}[h]
\begin{minipage}{0.49\textwidth}
\begin{lstlisting}[style=tfgj, caption=Valid Java program, label=lst:addExample]
<A> List<A> add(List<A> l, A v)

List<? super String> l = ...;
add(l, "String");
\end{lstlisting}
\end{minipage}\hfill
\begin{minipage}{0.49\textwidth}
\begin{lstlisting}[style=tamedfj, caption=\TamedFJ{} representation, label=lst:addExampleLet]
<A> List<A> add(List<A> l, A v)
List<? super String> l = ...;
let v:(*@$\tv{v}$@*) = l
    in add(v, "String");
\end{lstlisting}
\end{minipage}\\
\begin{minipage}{0.49\textwidth}
\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:addExampleCons]
(*@$\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}} \lessdot \tv{v}$@*)
(*@$\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$@*)
(*@$\type{String} \lessdot \wtv{a}$@*)
\end{lstlisting}
\end{minipage}\hfill
\begin{minipage}{0.49\textwidth}
\begin{lstlisting}[style=letfj, caption=Type solution, label=lst:addExampleSolution]
<A> List<A> add(List<A> l, A v)
List<? super String> l = ...;
let l2:(*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = l
    in <X>add(l2, "String");
\end{lstlisting}
\end{minipage}
\end{figure}

% \begin{description}
%     \item[input] \tifj{} program
%     \item[output] type solution
%     \item[postcondition] the type solution applied to the input must yield a valid \letfj{} program
% \end{description}

%Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
Listings \ref{lst:addExample}, \ref{lst:addExampleLet}, \ref{lst:addExampleCons}, and
\ref{lst:addExampleSolution} showcase our global type inference algorithm step by step.
In this example we know that the type of the variable \texttt{l} is an existential type and has to undergo a capture conversion
before being passed to a method call.
This is done by converting the program to A-Normal form \ref{lst:addExampleLet},
which introduces a let statement defining a new variable \texttt{v}.
Afterwards unknown types are replaced by type placeholders ($\tv{v}$ for the type of \texttt{v}) and constraints are generated (see \ref{lst:addExampleCons}).
These constraints mirror the type rules of our \TamedFJ{} calculus.
% During the constraint generation step the type of the variable \texttt{v} is unknown
% and given the type placeholder $\tv{v}$.
The methodcall to \texttt{add} spawns the constraint $\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$.
Here we introduce a capture constraint ($\lessdotCC$) %a new type of subtype constraint
expressing that the left side of the constraint is subject to a capture conversion.
Now our unification algorithm \unify{} (defined in chapter \ref{sec:unify}) is used to solve these constraints.
In the starting set of constraints no type is assigned to $\tv{v}$ yet.
During the course of \unify{} more and more types emerge.
As soon as a concrete type for $\tv{v}$ is given \unify{} can conduct a capture conversion if needed.
%The constraints where this is possible are marked as capture constraints.
In this example $\tv{v}$ will be set to $\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$ leaving us with the following constraints:

\begin{displaymath}
\prftree[r]{Capture}{
\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}, \, \type{String} \lessdotCC \wtv{a}
}{
\wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
}
\end{displaymath}

%Capture Constraints $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ allow for a capture conversion,
%which converts a constraint of the form $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ to $(\exptype{C}{\rwildcard{X}} \lessdot \type{T})$
The constraint $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$
allows \unify{} to do a capture conversion to $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
The captured wildcard $\rwildcard{X}$ gets a fresh name and is stored in the wildcard environment of the \unify{} algorithm.
Leaving us with the solution $\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$, $\type{String} \lessdot \rwildcard{Y}$
The constraint $\type{String} \lessdot \rwildcard{Y}$ is satisfied
because $\rwildcard{Y}$ has $\type{String}$ as lower bound.


A correct Featherweight Java program including all type annotations and an explicit capture conversion via let statement is shown in listing \ref{lst:addExampleSolution}.
This program can be deducted from the type solution of our \unify{} algorithm presented in chapter \ref{sec:unify}.
In the body of the let statement the type $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$
becomes $\exptype{List}{\rwildcard{X}}$ and the wildcard $\wildcard{X}{\type{Object}}{\type{String}}$ is free and can be used as
a type parameter to method call \texttt{<X>add(v, "String")}.

% The input to our type inference algorithm is a modified version of the calculus in \cite{WildcardsNeedWitnessProtection} (see chapter \ref{sec:tifj}).
% First \fjtype{} (see section \ref{chapter:constraintGeneration}) generates constraints
% and afterwards \unify{} (section \ref{sec:unify}) computes a solution for the given constraint set.
% Constraints consist out of subtype constraints $(\type{T} \lessdot \type{T})$ and capture constraints $(\type{T} \lessdotCC \type{T})$.
% \textit{Note:} a type $\type{T}$ can either be a named type, a type placeholder or a wildcard type placeholder.
% A subtype constraint is satisfied if the left side is a subtype of the right side according to the rules in figure \ref{fig:subtyping}.
% \textit{Example:} $\exptype{List}{\ntv{a}} \lessdot \exptype{List}{\type{String}}$ is fulfilled by replacing type placeholder $\ntv{a}$ with the type $\type{String}$.
% Subtype constraints and type placeholders act the same as the ones used in \emph{Type Inference for Featherweight Generic Java} \cite{TIforFGJ}.
% The novel capture constraints and wildcard placeholders are needed for method invocations involving wildcards.

% The central piece of this type inference algorithm, the \unify{} process, is described with implication rules (chapter \ref{sec:unify}).
% We try to keep the branching at a minimal amount to improve runtime behavior.
% Also the transformation steps of the \unify{} algorithm are directly related to the subtyping rules of our calculus.
% There are no informal parts in our \unify{} algorithm.
% It solely consist out of transformation rules which are bound to simple checks.

\subsection{Challenges}\label{challenges}
%TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}

% Wildcards are not reflexive.
% ( on the equals property ), every wildcard has to be capture converted when leaving its scope

% do not substitute free type variables

Lets have a look at a few challenges:
\begin{itemize}
\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}.
The first one is a valid Java program,
because the type \texttt{List<? super String>} is \textit{capture converted} to a fresh type variable $\rwildcard{X}$
which is used as the generic method parameter for the call to \texttt{add} as shown in listing \ref{lst:addExampleLet}.
Knowing that the type \texttt{String} is a subtype of the free variable $\rwildcard{X}$
it is safe to pass \texttt{"String"} for the first parameter of the function.

The second program shown in listing \ref{lst:concatError} is incorrect.
The method call to \texttt{concat} with two wildcard lists is unsound.
Each list could be of a different kind and therefore the \texttt{concat} cannot succeed.
The problem gets apparent when we try to write the \texttt{concat} method call in our \TamedFJ{} calculus (listing \ref{lst:concatTamedFJ}):
\texttt{l1'} and \texttt{l2'} are two different lists inside the body of the let statements, namely
$\exptype{List}{\rwildcard{X}}$ and $\exptype{List}{\rwildcard{Y}}$.
For the method call \texttt{concat(x1, x2)} no replacement for the generic \texttt{A}
exists to satisfy
$\exptype{List}{\type{A}} <: \exptype{List}{\type{X}},
\exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$.

% \textbf{Solution:}
% Capture Conversion during Unify.

\item 
\unify{} morphs a constraint set into a correct type solution
gradually assigning types to type placeholders during that process.
Solved constraints are removed and never considered again.
In the following example \unify{} solves the constraint generated by the expression
\texttt{l.add(l.head())} first, which results in $\ntv{l} \lessdot \exptype{List}{\wtv{a}}$.
\begin{verbatim}
anyList() = new List<String>() :? new List<Integer>()

add(anyList(), anyList().head());
\end{verbatim}
The type for \texttt{l} can be any kind of list, but it has to be a invariant one.
Assigning a \texttt{List<?>} for \texttt{l} is unsound, because the type list hiding behind
\texttt{List<?>} could be a different one for the \texttt{add} call than the \texttt{head} method call.
An additional constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
is solved by removing the wildcard $\rwildcard{X}$ if possible.

this problem is solved by ANF transformation

\item \textbf{Wildcards as Existential Types:}
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:
$\exptype{List}{\exptype{List}{\type{?}}}$ equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
During type checking \emph{intermediate types}
can emerge, which have no equivalent in the Java syntax.

\begin{lstlisting}[style=java,label=shuffleExample,caption=Intermediate Types Example]
class List<X> extends Object {...}
class List2D<X> extends List<List<X>> {...}

<X> void shuffle(List<List<X>> list) {...}

List<List<?>> l = ...;
List2D<?> l2d = ...;

shuffle(l); // Error
shuffle(l2d); // Valid
\end{lstlisting}
Java is using local type inference to allow method invocations which are not describable with regular Java types.
The \texttt{shuffle} method in this case is invoked with the type $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$
which is a subtype of $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
After capture conversion \texttt{l2d'} has the type $\exptype{List}{\exptype{List}{\rwildcard{X}}}$
and \texttt{shuffle} can be invoked with the type parameter $\rwildcard{X}$:
\begin{lstlisting}[style=TamedFJ]
let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in <X>shuffle(l2d')
\end{lstlisting}

For the example shown in listing \ref{shuffleExample} the method call \texttt{shuffle(l2d)} creates the constraints:
\begin{constraintset}
\begin{center}
    $
    \begin{array}{l}
    \wctype{\rwildcard{X}}{List2D}{\rwildcard{X}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
    \\
    \hline
    \wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
    \\
    \hline
    \textit{Capture Conversion:}\ 
    \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\wtv{x}}}
    \\
    \hline
    \textit{Solution:} \wtv{x} \doteq \rwildcard{X} \implies \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\rwildcard{X}}}
    \end{array}
    $
\end{center}
\end{constraintset}

The method call \texttt{shuffle(l)} is invalid however,
because \texttt{l} has the type
$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
There is no solution for the subtype constraint:
$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$

\item \label{challenge3} \textbf{Free Variables cannot leaver their scope}:

\begin{example}
Take the Java program in listing \ref{lst:mapExample} for example.
It maps every element of a list
$\expr{l} : \exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$
to a polymorphic \texttt{id} method.
We want to use our \unify{} algorithm to determine the correct type for the
variable \expr{l2}.
Although we do not specify constraint generation for language constructs like
lambda expressions used in this example,
we can imagine that the constraints have to look something like this:

\begin{minipage}{0.45\textwidth}
\begin{lstlisting}[caption=List Map Example,label=lst:mapExample]
<X> List<X> id(List<X> l){ ... }
List<List<?>> ls;
l2 = l.map(x -> id(x));
\end{lstlisting}\end{minipage}
\hfill
\begin{minipage}{0.45\textwidth}
\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:mapExampleCons]
(*@$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}}$@*)
(*@$\exptype{List}{\wtv{x}} \lessdot \tv{z},$@*)
(*@$\exptype{List}{\tv{z}} \lessdot \tv{l2}$@*)
\end{lstlisting}
\end{minipage}

The constraints
$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}},
\exptype{List}{\wtv{x}} \lessdot \tv{z}$
stem from the body of the lambda expression
\texttt{id(x)}.
\textit{For clarification:} This method call would be represented as the following expression in \letfj{}:
\texttt{let x1 :$\wctype{\rwildcard{A}}{List}{\rwildcard{A}}$ = x in id(x) :$\tv{z}$}

The T-Let rule prevents us from using free variables created by the method call to \expr{id}
to be used in the return type $\tv{z}$.
But this has to be signaled to the \unify{} algorithm, which does not know about the origin and context of
the constraints.
If we naively substitute $\sigma(\tv{z}) = \exptype{List}{\rwildcard{A}}$
the return type of the \texttt{map} function would be the type $\exptype{List}{\exptype{List}{\rwildcard{A}}}$.
This type solution is unsound.
The type of \expr{l2} is the same as the one of \expr{l}:
$\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$

\textbf{Solution:}
We solve this by distinguishing between wildcard placeholders and normal placeholders.
$\ntv{z}$ is a normal placeholder and is not allowed to contain free variables.

\end{example}

\end{itemize}

%TODO: Move this part. or move the third challenge some underneath.