Global Type Inference Intro

introduction.tex

@@ -282,6 +282,40 @@ lo.add(new Integer(1)); // error!
 
 \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
@@ -298,11 +332,32 @@ 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
+The methodcall to \texttt{add} spawns the constraint $\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$.
-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}.
+At the start of our global type inference algorithm no types are assigned yet.
+During the course of \unify{} - our unification algorithm used to solve the generated constraint set (see chapter \ref{sec: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}.
@@ -326,43 +381,6 @@ a type parameter to method call \texttt{<X>add(v, "String")}.
 % 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)
-
-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]
-(*@$\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}
-
 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}}}$.
@@ -409,36 +427,6 @@ 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}
-\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.
-
-%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}}$.
-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
-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}
@@ -516,17 +504,10 @@ $\exptype{List}{\type{A}} <: \exptype{List}{\type{X}},
 % is solved by removing the wildcard $\rwildcard{X}$ if possible.
 
 \item \textbf{Capture Conversion during \unify{}:}
-The return type of a generic method call depends on its argument types.
+The example in \ref{lst:addExample} needs to be solvable.
-A method like \texttt{String trim(String s)} will always return a \type{String} type.
+Here a capture conversion during the unification step of our algorithm has to be conducted.
-However the return type of \texttt{<A> A head(List<A> l)} is a generic variable \texttt{A} and only shows
+Otherwise the \texttt{add} method is not callable with the existential type
-its actual type when the type of the argument list \texttt{l} is known.
+$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
-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.
-
 
 \item \textbf{Free Variables cannot leaver their scope}: