Add 4 steps of TI introduction

introduction.tex

@@ -32,27 +32,22 @@ 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
+The type inference algorithm presented here supports Java Wildcards.
-with the biggest change being the added wildcard support.
 % 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.
+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.
 
-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.
-
 \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.
@@ -285,39 +280,89 @@ lo.add(new Integer(1)); // error!
 \end{minipage}
 \end{figure}
 
+\section{Global Type Inference Algorithm}
+
+% \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 constraints are generated \ref{lst:addExampleCons}.
+During the constraint generation step the type of the variable \texttt{v} is unknown
+and given the type placeholder $\tv{v}$.
+Due to the call to the method \texttt{add} it is clear that \texttt{v} has to be a subtype of
+any kind of \texttt{List} resulting in 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.
+%Additionally we use a wildcard placeholder $\wtv{a}$ as a type parameter for \texttt{List}.
+
+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.
+
+
 %show input and a correct letFJ representation
 %TODO: first show local type inference and explain lessdotCC constraints. then show example with global TI
 \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)
-
+List<? super String> l = ...;
-let l2 : (*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = 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]
+(*@$\tv{v} \lessdot \wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$@*)
+(*@$\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}}}$.
@@ -349,26 +394,6 @@ and \texttt{shuffle} can be invoked with the type parameter $\rwildcard{X}$:
 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
-%     \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.
-
-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