Restructure and Cleanup Unify

TIforWildFJ.tex

@@ -1,5 +1,5 @@
 
-\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate]{lipics-v2021}
+\documentclass{llncs}
 %This is a template for producing LIPIcs articles. 
 %See lipics-v2021-authors-guidelines.pdf for further information.
 %for A4 paper format use option "a4paper", for US-letter use option "letterpaper"
@@ -40,6 +40,7 @@
 
 \input{prolog}
 
+\begin{document}
 \bibliographystyle{plainurl}% the mandatory bibstyle
 
 \title{Global Type Inference for Featherweight Java with Wildcards} %TODO Please add
@@ -54,16 +55,16 @@
 
 \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.'
 
-\Copyright{Andreas Stadelmeier and Martin Plümicke and Peter Thiemann} %TODO mandatory, please use full first names. LIPIcs license is "CC-BY";  http://creativecommons.org/licenses/by/3.0/
+%\Copyright{Andreas Stadelmeier and Martin Plümicke and Peter Thiemann} %TODO mandatory, please use full first names. LIPIcs license is "CC-BY";  http://creativecommons.org/licenses/by/3.0/
 
-\ccsdesc[500]{Software and its engineering~Language features}
+%\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
+%\category{} %optional, e.g. invited paper
 
-\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
+%\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
 %\relatedversiondetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93]{Classification (e.g. Full Version, Extended Version, Previous Version}{URL to related version} %linktext and cite are optional
 
 %\supplement{}%optional, e.g. related research data, source code, ... hosted on a repository like zenodo, figshare, GitHub, ...
@@ -77,21 +78,20 @@
 
 
 
-%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\EventEditors{John Q. Open and Joan R. Access}
-\EventNoEds{2}
-\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
-\EventShortTitle{CVIT 2016}
-\EventAcronym{CVIT}
-\EventYear{2016}
-\EventDate{December 24--27, 2016}
-\EventLocation{Little Whinging, United Kingdom}
-\EventLogo{}
-\SeriesVolume{42}
-\ArticleNo{23}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% %Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% \EventEditors{John Q. Open and Joan R. Access}
+% \EventNoEds{2}
+% \EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
+% \EventShortTitle{CVIT 2016}
+% \EventAcronym{CVIT}
+% \EventYear{2016}
+% \EventDate{December 24--27, 2016}
+% \EventLocation{Little Whinging, United Kingdom}
+% \EventLogo{}
+% \SeriesVolume{42}
+% \ArticleNo{23}
+% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\begin{document}
 
 \maketitle
 

conclusion.tex

@@ -1,4 +1,10 @@
 \section{Properties of the Algorithm}
+\begin{itemize}
+    \item Our algorithm is designed for extensibility with the final goal of full support for Java.
+    \unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
+    Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
+    
+\end{itemize}
 
 %TODO: how are the challenges solved: Describe this in the last chapter with examples!
 \section{Soundness}\label{sec:soundness}

constraints.tex

@@ -1,62 +1,71 @@
-\section{Capture Constraints}
+\subsection{Capture Constraints}
 %TODO: General Capture Constraint explanation
 
-The equality relation on Capture constraints is not reflexive.
-A capture constraint is never equal to another capture constraint even when structurally the same
-($\type{T} \lessdotCC \type{S} \neq \type{T} \lessdotCC \type{S}$).
-This is necessary to solve challenge \ref{challenge:1}.
-A capture constraint is bound to a specific let statement.
-For example the statement \lstinline{let x = v in x.get()}
-generates a constraint like $\tv{x} \lessdotCC \exptype{List}{\wtv{a}}$.
-This means that the type variable $\tv{x}$ on the left side of the capture constraint is actually a placeholder
-for a type that is subject to capture conversion.
-It is possible that two syntactically equal capture constraints evolve
-during constraint generation or the \unify{} process.
-Take the two constraints in listing \ref{lst:sameConstraints}
-which originate from the \texttt{concat} method invocation in listing \ref{lst:faultyConcat} for example.
-To illustrate their connection to a let statement each capture constraint is annoted with its respective variable.
-After a capture conversion step the constraints become
-$\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}},
-\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}
-$
-making obvious that this constraint set is unsolvable.
-
-\textit{Note:}
-In the special case \lstinline{let x = v in concat(x,x)} the constraint would look like
-$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}},
-\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
-and we could actually delete one of them without loosing information.
-But this case will never occur in our algorithm, because the let statements for our input programs are generated by a ANF transformation (see \ref{sec:anfTransformation}).
-
-In this paper we do not annotate capture constraint with their source let statement.
-Instead we consider every capture constraint as distinct to other constraints even when syntactically the same,
-because we know that each capture constraint originates from a different let statement.
-\textit{Hint:} An implementation of this algorithm has to consider that seemingly equal capture constraints are actually not the same
-and has to allow doubles in the constraint set.
-
+Capture Constraints are bound to a variable.
+For example a let statement like \lstinline{let x = v in x.get()} will create the capture constraint
+$\tv{x} \lessdotCC_x \exptype{List}{\wtv{a}}$.
+This time we annotated the capture constraint with an $x$ to show its relation to the variable \texttt{x}.
+Let's do the same with the constraints generated by the \texttt{concat} method invocation in listing \ref{lst:faultyConcat},
+creating the constraints \ref{lst:sameConstraints}.
 
 \begin{figure}
-\begin{minipage}[t]{0.49\textwidth}
+  \begin{minipage}[t]{0.49\textwidth}
     \begin{lstlisting}[caption=Faulty Method Call,label=lst:faultyConcat]{tamedfj}
-List<?> v = ...;
+  List<?> v = ...;
   
-let x = v in 
+  let x = v in 
       let y = v in
         concat(x, y) // Error!
     \end{lstlisting}\end{minipage}
     \hfill
     \begin{minipage}[t]{0.49\textwidth}
-\begin{lstlisting}[caption=Annotated constraints,mathescape=true,style=constraints,label=lst:sameConstraints]
-$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
-$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{y} \exptype{List}{\wtv{a}}$
+  \begin{lstlisting}[caption=Annotated constraints,mathescape=true,style=constraints,label=lst:sameConstraints]
+  $\tv{x} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{x}$
+  $\tv{y} \lessdotCC_\texttt{y} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{y}$
     \end{lstlisting}
     \end{minipage}
 \end{figure}
 
-\section{Constraint generation}\label{chapter:constraintGeneration}
-% Our type inference algorithm is split into two parts.
-% A constraint generation step \textbf{TYPE} and a \unify{} step.
 
+During the \unify{} process it could happen that two syntactically equal capture constraints evolve,
+but they are not the same because they are each linked to a different let introduced variable.
+In this example this happens when we substitute $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\tv{x}$ and $\tv{y}$
+resulting in:
+%For example by substituting $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{x}]$ and $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{y}]$:
+\begin{displaymath}
+  \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_x \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_y \exptype{List}{\wtv{a}}
+\end{displaymath}
+Thanks to the original annotations we can still see that those are different constraints.
+After \unify{} uses the \rulename{Capture} rule on those constraints
+it gets obvious that this constraint set is unsolvable:
+\begin{displaymath}
+  \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}},
+\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}
+\end{displaymath}
+
+%In this paper we do not annotate capture constraint with their source let statement.
+The rest of this paper will not annotate capture constraints with variable names.
+Instead we consider every capture constraint as distinct to other capture constraints even when syntactically the same,
+because we know that each of them originates from a different let statement.
+\textit{Hint:} An implementation of this algorithm has to consider that seemingly equal capture constraints are actually not the same
+and has to allow doubles in the constraint set.
+
+% %We see the equality relation on Capture constraints is not reflexive.
+% A capture constraint is never equal to another capture constraint even when structurally the same
+% ($\type{T} \lessdotCC \type{S} \neq \type{T} \lessdotCC \type{S}$).
+% This is necessary to solve challenge \ref{challenge:1}.
+% A capture constraint is bound to a specific let statement.
+
+\textit{Note:}
+In the special case \lstinline{let x = v in concat(x,x)} the constraints would look like
+$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}},
+\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
+and we could actually delete one of them without loosing information.
+But this case will never occur in our algorithm, because the let statements for our input programs are generated by a ANF transformation (see \ref{sec:anfTransformation}).
+
+
+
+\section{Constraint generation}\label{chapter:constraintGeneration}
 % Method names are not unique.
 % It is possible to define the same method in multiple classes.
 % The \TYPE{} algorithm accounts for that by generating Or-Constraints.
@@ -82,9 +91,6 @@ We will focus on those two parts where also the new capture constraints and wild
 %They will be added by an ANF transformation (see chapter \ref{sec:anfTransformation}).
 
 Before generating constraints the input is transformed by an ANF transformation (see section \ref{sec:anfTransformation}).
-Capture conversion is only needed for wildcard types,
-but we don't know which expressions will spawn wildcard types because there are no type annotations yet.
-We preemptively enclose every expression in a let statement before using it as a method argument.
 
 %Constraints are generated on the basis of the program in A-Normal form.
 %After adding the missing type annotations the resulting program is valid under the typing rules in \cite{WildFJ}.
@@ -119,7 +125,7 @@ m(l, v){
     \end{minipage}%
     \hfill
     \begin{minipage}{0.5\textwidth}
-\begin{lstlisting}[style=tfgj,caption=converted to A-Normal form,label=lst:anfoutput]
+\begin{lstlisting}[style=tfgj,caption=A-Normal form,label=lst:anfoutput]
 m(l, v) = 
     let x1 = l in
         let x2 = v in x1.add(x2)
@@ -143,6 +149,7 @@ $\begin{array}{lrcl}
 \end{figure}
 
 \begin{figure}
+  \center
 $
 \begin{array}{lrcl}
 %\hline
@@ -154,15 +161,15 @@ $
 %\hline
 \end{array}
 $
-\caption{A-Normal form}\label{fig:anf-syntax}
+\caption{Syntax of a \TamedFJ{} program in A-Normal Form}\label{fig:anf-syntax}
 \end{figure}
 
 \subsection{Constraint Generation Algorithm}
-Generally subtype constraints for an expression mirror the subtype relations in the premise of the respective type rule introduced in section \ref{sec:tifj}.
-Unknown types at the time of the constraint generation step are replaced with type placeholders.
+% Generally subtype constraints for an expression mirror the subtype relations in the premise of the respective type rule introduced in section \ref{sec:tifj}.
+% Unknown types at the time of the constraint generation step are replaced with type placeholders.
 
-The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
-Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
+% The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
+% Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
 
 The parameter types given to a generic method also affect their return type.
 During constraint generation the algorithm does not know the parameter types yet.
@@ -177,25 +184,12 @@ A normal type placeholder cannot hold types containing free variables.
 Normal type placeholders are assigned types which are also expressible with Java syntax.
 So no types like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ or $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
 
-Type variables declared in the class header are passed to \unify{}.
+It is possible to feed the \unify{} algorithm a set of free variables with predefined bounds.
+This is used for class generics see figure \ref{fig:constraints-for-classes}.
+The \fjtype{} function returns a set of constraints aswell as an initial environment $\Delta$
+containing the generics declared by this class.
 Those type variables count as regular types and can be held by normal type placeholders.
 
-
-There are two different types of constraints:
-\begin{description}
-\item[$\lessdot$] \textit{Example:}
-
-$\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}$
-
-\noindent
-Those two constraints imply that we have to find a type replacement for type variable $\tv{a}$,
-which is a supertype of $\exptype{List}{String}$ aswell as $\exptype{List}{Integer}$.
-This paper describes a \unify{} algorithm to solve these constraints and calculate a type solution $\sigma$.
-For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
-\item[$\lessdotCC$] TODO
-% The \fjtype{} algorithm assumes capture conversions for every method parameter.
-\end{description}
-
 %Why do we need a constraint generation step?
 %% The problem is NP-Hard
 %% a method call, does not know which type it will produce
@@ -203,6 +197,7 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
 
 %NO equals constraints during the constraint generation step!
 \begin{figure}[tp]
+  \center
 \begin{tabular}{lcll}
     $C $ &$::=$ &$\overline{c}$ & Constraint set \\
     $c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \lessdotCC \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
@@ -220,17 +215,19 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
 \begin{figure}[tp]
   \begin{gather*}
     \begin{array}{@{}l@{}l}
-      \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\ol{X} \triangleleft \ol{N}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\
+      \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\overline{\type{X} \triangleleft \type{N}}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\
               & \begin{array}{ll@{}l}
 \textbf{let} & \ol{\methodAssumption} =
                 \set{ \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \mid
                   \set{ \mv{m}(\ol{x}) = \expr{e} } \in \ol{M}, \, \tv{a}, \ol{\tv{a}}\ \text{fresh} } \\
-              \textbf{in} 
-                  & \begin{array}[t]{l}
+              & \Delta = \set{ \overline{\wildcard{X}{\type{N}}{\bot}} } \\
+              & C = \begin{array}[t]{l}
                 \set{ \typeExpr(\mtypeEnvironment \cup \ol{\methodAssumption} \cup \set{\mv{this} :
               \exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}} }, \texttt{e}, \tv{a})
                \\ \quad \quad \quad \quad \mid \set{ \mv{m}(\ol{x}) = \expr{e} }  \in \ol{M},\, \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \in \ol{\methodAssumption}}
-                  \end{array}
+                  \end{array} \\
+              \textbf{in} 
+                  & (\Delta, C)
                 \end{array}
     \end{array}
   \end{gather*}

introduction.tex

@@ -10,7 +10,36 @@
 % 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),
@@ -32,26 +61,29 @@ are infered and inserted by our algorithm.
 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 algorithm presented in this paper is an improved version
-with the biggest change being the added wildcard support.
+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}.
+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 problems shown in chapter \ref{challenges} are handled incorrectly.
-Whereas our type inference algorithm is based on a Featherweight Java calculus \cite{WildFJ} and it's proven sound subtyping rules.
-%But they are all correctly solved by our new type inference algorithm presented in this paper.
+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 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.
+%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}.
@@ -146,11 +178,11 @@ We prove soundness and aim for a good compromise between completeness and time c
 \begin{figure}
 \begin{minipage}{0.43\textwidth}
 \begin{lstlisting}[style=java,label=lst:intro-example-typeless,caption=Missing return type]
-genBox() {
+genList() {
   if( ... ) {
-        return new Box(1);
+    return new List(1);
   } else {
-        return new Box("Str");
+    return new List("Str");
   }
 }
     \end{lstlisting}
@@ -158,11 +190,11 @@ genBox() {
 \hfill
 \begin{minipage}{0.55\textwidth}
 \begin{lstlisting}[style=tfgj,caption=Type inference solution,label=lst:intro-example-typed]
-Box<?> genBox() {
+List<?> genList() {
   if( ... ) {
-        return new Box<Integer>(1);
+    return new List<Integer>(1);
   } else {
-        return new Box<String>("Str");
+    return new List<String>("Str");
   }
 }
     \end{lstlisting}
@@ -196,77 +228,8 @@ 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.
 
-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
-are using the same field of type \texttt{List<?>}.
-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);
-
-concat(l1, l2); // Error! this would add an Integer to a List of Strings
-\end{lstlisting}
-\begin{lstlisting}[style=TamedFJ,caption=\TamedFJ{} representation of the concat call, 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}
-
-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}).
-
-\begin{figure}
-\begin{minipage}{0.4\textwidth}
+\begin{minipage}{0.48\textwidth}
 \begin{lstlisting}[caption=Java Invariance Example,label=lst:invarianceExample]{java}
 List<String> ls = ...;
 List<Object> lo = ...;
@@ -285,72 +248,150 @@ lo.add(new Integer(1)); // error!
 \end{minipage}
 \end{figure}
 
-%show input and a correct letFJ representation
-%TODO: first show local type inference and explain lessdotCC constraints. then show example with global TI
+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) ...
+<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=letfj, caption=\TamedFJ{} representation, label=lst:addExampleLet]
+\begin{lstlisting}[style=tamedfj, caption=\TamedFJ{} representation, label=lst:addExampleLet]
 <A> List<A> add(List<A> l, A v)
-
-let l2 : (*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = l
+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}
 
-In listing \ref{lst:addExample} Java uses local type inference \cite{JavaLocalTI}
-to determine the type parameters to the \texttt{add} method call.
-A \TamedFJ{} representation including all type annotations and an explicit capture conversion via let statement is shown in listing \ref{lst:addExampleLet}.
-%In \letfj{} there is no local type inference and all type parameters for a method call are mandatory (see listing \ref{lst:addExampleLet}).
-%If wildcards are involved the so called capture conversion has to be done manually via let statements.
-%A let statement \emph{opens} an existential type.
-In the body of the let statement the \textit{capture 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 \texttt{<X>add(...)}.
-%This is a valid Java program where the type parameters for the polymorphic method \texttt{add}
-%are determined by local type inference.
-
-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}
-%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.
-
-Example: % This program is not typable with the Type Inference algorithm from Plümicke
-\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}
-
-\section{Global Type Inference Algorithm}
-
 % \begin{description}
 %     \item[input] \tifj{} program
 %     \item[output] type solution
@@ -358,90 +399,65 @@ let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) =
 % \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:
 
-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.
-
-\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}
-%
-Lets have a look at the constraints generated by \fjtype{} for the example in listing \ref{lst:addExample}:
-\begin{constraintset}
-\begin{center}
-$\begin{array}{c}
+\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}
-\\
-\hline
-\textit{Capture Conversion:}\ \wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
-\\
-\hline
-\textit{Solution:}\ \wtv{a} \doteq \rwildcard{Y} \implies \wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}, \, \type{String} \lessdot \rwildcard{Y}
-\end{array}
-$
-\end{center}
-\end{constraintset}
-%
-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})$
-%These constraints are used at places where a capture conversion via let statement can be added.
+}{
+\wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
+}
+\end{displaymath}
 
-%Why do we need the lessdotCC constraints here?
-The type of \texttt{l} can be capture converted by a let statement if needed (see listing \ref{lst:addExampleLet}).
-Therefore we assign the constraint $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$
-which allows \unify{} to do a capture conversion to $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
+%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.
-
-
-\textit{Note:} The constraint $\type{String} \lessdot \rwildcard{Y}$ is satisfied
+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.
 
 
-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}
+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 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}}}$
+% 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}
@@ -473,40 +489,87 @@ exists to satisfy
 $\exptype{List}{\type{A}} <: \exptype{List}{\type{X}},
 \exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$.
 
-% \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>()
+% \textbf{Solution:}
+% Capture Conversion during Unify.
 
-% 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.
+\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>()
 
-\item \textbf{Capture Conversion during \unify{}:}
-The return type of a generic method call depends on its argument types.
-A method like \texttt{String trim(String s)} will always return a \type{String} type.
-However the return type of \texttt{<A> A head(List<A> l)} is a generic variable \texttt{A} and only shows
-its actual type when the type of the argument list \texttt{l} is known.
-The same goes for capture conversion, which can only be applied for a method call
-when the argument types are given.
-At the start of our global type inference algorithm no types are assigned yet.
-During the course of the \unify{} algorithm more and more types emerge.
-As soon as enough type information is given \unify{} can conduct a capture conversion if needed.
-The constraints where this is possible are marked as capture constraints.
+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{Free Variables cannot leaver their scope}:
+\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 following Java program for 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.
@@ -517,31 +580,25 @@ 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}{java}
+\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{constraintset}
-$
-\begin{array}{l}
-\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{array}
-$
-\end{constraintset}
+\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{shuffle(x)}.
+\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}$}
 

tRules.tex

@@ -30,9 +30,6 @@ which by default is also a correct Featherweight Java program (see chapter \ref{
 \begin{itemize}
 \item The calculus does not include method overriding for simplicity reasons.
 Type inference for that is described in \cite{TIforFGJ} and can be added to this algorithm accordingly.
-Our algorithm is designed for extensibility with the final goal of full support for Java.
-\unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
-Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
 %\textit{Note:}
 \item The typing rules for expressions shown in figure \ref{fig:expressionTyping} refrain from restricting polymorphic recursion.
 Type inference for polymorphic recursion is undecidable \cite{wells1999typability} and when proving completeness like in \cite{TIforFGJ} the calculus