Restructure challenges

constraints.tex

@@ -43,6 +43,9 @@ We preemptively enclose every expression in a let statement before using it as a
 % This behaviour emulates Java's implicit capture conversion.
 
 
+%TODO: how are the challenges solved:
+The \unify{} algorithm only sees the constraints with no information about the program they originated from.
+
 
 \subsection{ANF transformation}\label{sec:anfTransformation}
 \newcommand{\anf}[1]{\ensuremath{\tau}(#1)}

introduction.tex

@@ -181,8 +181,44 @@ 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.
 
-% Goal: Motivate the TamedFJ language. Why do we need it (Capture Conversion)
+Wildcard types are virtual types.
-This behaviour is emulated by our language \TamedFJ{},
+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=Concat Example,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);
+\end{lstlisting}
+\begin{lstlisting}[style=TamedFJ,caption=\TamedFJ{} representation, 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.
@@ -246,7 +282,7 @@ add(l, "String");
 \end{lstlisting}
 \end{minipage}\hfill
 \begin{minipage}{0.49\textwidth}
-\begin{lstlisting}[style=letfj, caption=\letfj{} representation, label=lst:addExampleLet]
+\begin{lstlisting}[style=letfj, 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
@@ -255,7 +291,7 @@ let l2 : (*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcar
 \end{minipage}
 \end{figure}
 
-The Example in listing \ref{lst:addExample} is a valid Java program. Here Java uses local type inference \cite{JavaLocalTI}
+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}).
@@ -294,7 +330,7 @@ The \texttt{shuffle} method in this case is invoked with the type $\wctype{\rwil
 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=letfj]
+\begin{lstlisting}[style=TamedFJ]
 let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in <X>shuffle(l2d')
 \end{lstlisting}
 
@@ -457,106 +493,24 @@ A problem arises when replacing type variables with wildcards.
 Lets have a look at a few challenges:
 \begin{itemize}
 \item 
-%Passing wildcard types to a polymorphic method call comes with additional challenges.
+One challenge is to design the algorithm in a way that it finds a correct solution for the program shown in listing \ref{lst:addExample}
-% TODO: Here the concat example!
+and rejects the program in listing \ref{lst:concatError}.
-%- Wildcards are not reflexive
+The first one is a valid Java program,
-%- Wildcards are opaque types. Behind a Java Wildcard is a real type.
+because the type \texttt{List<? super String>} is \textit{capture converted} to a fresh type variable $\rwildcard{X}$
-
+which is used as the generic method parameter for the call to \texttt{add} as shown in listing \ref{lst:addExampleLet}.
-Wildcard types are virtual types.
+Knowing that the type \texttt{String} is a subtype of the free variable $\rwildcard{X}$
-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{?}.
-To enable the use of wildcards in argument types of a method invocation
-Java uses a process called \textit{Capture Conversion}.
-
-\begin{lstlisting}[caption=Concat Example,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);
-\end{lstlisting}
-
-
-%Existential types enable us to formalize Java's method call behavior and the so called Capture Conversion.
-\begin{displaymath}
-%TODO: 
-\begin{array}{l}
-        \begin{array}{@{}c}
-            \textit{mtype}(\texttt{concat}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \\
-            \texttt{l1} : \wctype{\rwildcard{A}}{List}{\rwildcard{A}}, \texttt{l2} : \wctype{\rwildcard{B}}{List}{\rwildcard{B}} \\
-            \exptype{List}{\rwildcard{A}} \nless: [{\color{red}?}/\type{X}]\exptype{List}{\type{X}} \quad \quad
-\exptype{List}{\rwildcard{B}} \nless: [{\color{red}?}/\type{X}]\exptype{List}{\type{X}}
-            \\
-            \hline
-        \vspace*{-0.3cm}\\
-            \texttt{concat}(\expr{l1}, \expr{l2}) : {\color{red}\textbf{Errror}}
-        \end{array}
-    \end{array}
-\end{displaymath}
-
-%A method call in Java makes use of the fact that a real type is behind a wildcard type
-
-\item \begin{example} \label{intro-example1}
-The first one is a valid Java program.
-The type \texttt{List<? super String>} is \textit{capture converted} to a fresh type variable $\rwildcard{X}$
-which is used as the generic method parameter \texttt{A}.
-
-Java uses capture conversion to replace the generic \texttt{A} by a capture converted version of the
-\texttt{? super String} wildcard.
-Knowing that the type \texttt{String} is a subtype of any type the wildcard \texttt{? super String} can inherit
 it is safe to pass \texttt{"String"} for the first parameter of the function.
 
-\begin{verbatim}
+The second program shown in listing \ref{lst:concatError} is incorrect.
-<A> List<A> add(List<A> l, A v) {}
-
-List<? super String> list = ...;
-add(list, "String");
-\end{verbatim}
-\end{example}
-
-\item \begin{example}\label{intro-example2}
-This example displays an incorrect Java program.
 The method call to \texttt{concat} with two wildcard lists is unsound.
 Each list could be of a different kind and therefore the \texttt{concat} cannot succeed.
-\begin{verbatim}
+The problem gets apparent when we try to write the \texttt{concat} method call in our \TamedFJ{} calculus (listing \ref{lst:concatTamedFJ}):
-<A> List<A> concat(List<A> l1, List<A> l2) { ... }
+\texttt{l1'} and \texttt{l2'} are two different lists inside the body of the let statements, namely
-List<?> getList() { ... }
+$\exptype{List}{\rwildcard{X}}$ and $\exptype{List}{\rwildcard{Y}}$.
-
-concat(getList(), getList());
-\end{verbatim}
-
-The \letfj{} representation in listing \ref{letfjConcatFail} clarifies this.
-Inside the let statement the variables hold the types
-$\set{ \texttt{x1} : \exptype{List}{\rwildcard{X}}, \texttt{x2} : \exptype{List}{\rwildcard{Y}}}$.
 For the method call \texttt{concat(x1, x2)} no replacement for the generic \texttt{A}
 exists to satisfy
 $\exptype{List}{\type{A}} <: \exptype{List}{\type{X}},
 \exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$.
-\begin{lstlisting}[style=letfj,caption=Incorrect method call,label=letfjConcatFail]
-let x1 : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = getList() in
-  let x2 : (*@$\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}$@*) = getList() in
-    concat(x1, x2)
-\end{lstlisting}
-
-% $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}, \\
-% \wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
-\end{example}
 
 % \item 
 % \unify{} morphs a constraint set into a correct type solution
@@ -649,5 +603,3 @@ $\ntv{z}$ is a normal placeholder and is not allowed to contain free variables.
 \end{itemize}
 
 %TODO: Move this part. or move the third challenge some underneath.
-The \unify{} algorithm only sees the constraints with no information about the program they originated from.
-The main challenge was to find an algorithm which computes $\sigma(\wtv{a}) = \rwildcard{X}$ for example \ref{intro-example1} but not for example \ref{intro-example2}.

relatedwork.tex

@@ -54,7 +54,7 @@ finite set of maximal types (for more details see Section
 refines this approach by moving to a constraint-based algorithm and by
 considering lambda expressions and Scale-like function types.
 
-Pluemicke has a different approach to introduce wildcards in \cite{Plue09_1}. He
+Pluemicke has a different approach to introduce wildcards in \cite{plue09_1}. He
 allows wildcards as any subsitution for type variables and disclaim the
 capture conversion. Instead he extended
 the subtyping ordering such that for $\theta \sub \theta' \sub \theta''$ holds