Let statement and capture conversion introduction

introduction.tex

@@ -228,12 +228,32 @@ 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
-are using the same field of type \texttt{List<?>}.
+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,
@@ -252,70 +272,89 @@ Therefore calling the method \texttt{concat} with two wildcard lists in the exam
 List<String> ls = new List<String>();
 
 List<?> l1 = ls;
-List<?> l2 = new List<Integer>(1);
+List<?> l2 = new List<Integer>(1); // List containing Integer
 
-concat(l1, l2); // Error! this would add an Integer to a List of Strings
+concat(l1, l2); // Error! Would concat two different lists
 \end{lstlisting}
-\begin{lstlisting}[style=TamedFJ,caption=\TamedFJ{} representation of the concat call, label=lst:concatTamedFJ]
+\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}
 
-To enable the use of wildcards in argument types of a method invocation
+% % TODO intro to Featherweight Java
-Java uses a process called \textit{Capture Conversion}.
+% is a formal model of the Java programming language reduced to a core set of instructions.
-This behaviour is emulated by our language \TamedFJ{};
+% - We extend this model by existential types and let expressions.
-a Featherweight Java \cite{FJ} derivative with added wildcard support
+% - We copy this from \ref{WildFJ} but make type annotations optional
-and a global type inference feature (syntax definition in section \ref{sec:tifj}).
+% - Our calculus is called \TamedFJ{}
-%\TamedFJ{} is basically the language described by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection} with optional type annotations.
+% - \TamedFJ{} binds every method argument with a let statement.
-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.
+% To enable the use of wildcards in argument types of a method invocation
-%This makes the capture converion explicit.
+% Java uses a process called \textit{Capture Conversion}.
-\begin{lstlisting}
+% This behaviour is emulated by our language \TamedFJ{};
-let v : (*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$@*) = lo in v.<A>add(new Integer(1));
+% a Featherweight Java \cite{FJ} derivative with added wildcard support
-\end{lstlisting}
+% and a global type inference feature (syntax definition in section \ref{sec:tifj}).
-The method call is encased in a \texttt{let} statement and
+% %\TamedFJ{} is basically the language described by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection} with optional type annotations.
-\expr{lo} is assigned to a new variable \expr{v} of \linebreak[2]
+% 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{}:
-\textbf{Existential Type} $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$.
+% %The \texttt{add} call in listing \ref{lst:wildcardIntro} needs to be encased by a \texttt{let} statement in our calculus.
-Our calculus uses existential types \cite{WildFJ} to formalize wildcards:
+% %This makes the capture converion explicit.
-\texttt{List<? extends Object>} is translated to $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$
+% \begin{lstlisting}
-and \texttt{List<? super String>} is expressed as $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
+% let v : (*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$@*) = lo in v.<A>add(new Integer(1));
-The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound,
+% \end{lstlisting}
-and a type they are bound to.
+% The method call is encased in a \texttt{let} statement and
-In this case the name is $\rwildcard{A}$ and it's bound to the the type \texttt{List}.
+% \expr{lo} is assigned to a new variable \expr{v} of \linebreak[2]
-Inside the \texttt{let} statement the variable \expr{v} has the type
+% \textbf{Existential Type} $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$.
-$\exptype{List}{\rwildcard{A}}$.
+% Our calculus uses existential types \cite{WildFJ} to formalize wildcards:
-This is an explicit version of \linebreak[2]
+% \texttt{List<? extends Object>} is translated to $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$
-\textbf{Capture Conversion},
+% and \texttt{List<? super String>} is expressed as $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
-which makes use of the fact that a concrete type must be behind every wildcard type.
+% The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound,
-There is no instantiation of a \texttt{List<?>},
+% and a type they are bound to.
-but there exists some unknown type $\exptype{List}{\rwildcard{A}}$, with $\rwildcard{A}$ inbetween the bounds $\bot$ (bottom type, subtype of all types) and
+% In this case the name is $\rwildcard{A}$ and it's bound to the the type \texttt{List}.
-\texttt{Object}.
+% Inside the \texttt{let} statement the variable \expr{v} has the type
-Inside the body of the let statement \expr{v} is treated as a value with the constant type $\exptype{List}{\rwildcard{A}}$.
+% $\exptype{List}{\rwildcard{A}}$.
-Existential types enable us to formalize \textit{Capture Conversion}.
+% This is an explicit version of \linebreak[2]
-Polymorphic method calls need to be wrapped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}.
+% \textbf{Capture Conversion},
-In Java this is done implicitly in a process called capture conversion (as proposed in Wild FJ \cite{WildFJ}).
+% 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{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}
 
 \section{Global Type Inference Algorithm}
 
@@ -450,6 +489,9 @@ 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.