Add Wildcard introduction

introduction.tex

@@ -4,6 +4,17 @@
 % - Kapitel 1.2 + 1.3 ist noch zu komplex
 % - Constraints und Unifikation erklären, bevor Unifikation erwähnt wird
 
+%Inhalt:
+% Global type inference example (the sameList example)
+% Wildcards are needed because Java has side effects
+% Capture Conversion
+% Explain difference between local and global type inference
+
+someList(){}
+concat(l1, l2){
+    return l1.add(l2)
+}
+
 \section{Motivation}
 Java already uses type inference when it comes to method invocations, local variables or lambda expressions.
 The crucial part for all of this use cases is the surrounding context.
@@ -18,7 +29,7 @@ List<String> ls = emptyList();
 Local type inference is based on matching and not unification \cite{javaTIisBroken}.
 When calling the \texttt{emptyList} method without context its return value will be set to a \texttt{List<Object>}.
 The following Java code snippet is incorrect, because \texttt{emptyList()} returns
-a \texttt{List<Object>} instead of the required \texttt{List<List<String>>}.
+a \texttt{List<Object>} instead of the required $\exptype{List}{\exptype{List}{String}}$.
 \begin{verbatim}
 emptyList().add(new List<String>())
     .get(0)
@@ -281,22 +292,101 @@ List<?> genList() {
 % The type inference algorithm has to find the correct type involving wildcards (\texttt{List<?>}).
 
 \subsection{Java Wildcards}
-Wildcards are expressed by a \texttt{?} in Java and can be used as type parameters.
-Wildcards add variance to Java type parameters.
-Generally Java has invariant subtyping for polymorphic types.
+
+Java has invariant subtyping for polymorphic types
+and incooperates use-site variance via so called wildcard types.
 A \texttt{List<String>} is not a subtype of \texttt{List<Object>} for example
 even though it seems intuitive with \texttt{String} being a subtype of \texttt{Object}.
+Class instances in Java are mutable and passed by reference.
+Subtyping must be invariant otherwise the integrity of data classes like lists could be
+corrupted like shown in listing \ref{lst:invarianceExample},
+where an \texttt{Integer} is added to a list of \texttt{String}.
+
+\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]{java}
+List<String> ls = ...;
+List<? extends Object> lo = ...;
+lo = ls; // correct
+lo.add(new Integer(1)); // error!
+\end{lstlisting}
+\end{minipage}
+
 
 Wildcards can be formalized as existential types \cite{WildFJ}.
-\texttt{List<? extends Object>} and \texttt{List<? super String>} are both wildcard types
-denoted in our syntax by $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$ and
-$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
+A \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}}$.
+
+
+%Passing wildcard types to a polymorphic method call comes with additional challenges.
+% TODO: Here the concat example!
+- Wildcards are not reflexive
+- Wildcards are opaque types. Behind a Java Wildcard is a real type.
+
+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{?}.
+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
+
 
 The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound at the same time,
 and a type they are bound to.
 In this case the name is $\rwildcard{X}$ and it's bound to the the type \texttt{List}.
 
-Those properties are needed to formalize capture conversion.
+Using existential types to express Java's wildcard types enables us to formalize \textit{Capture Conversion}.
 Polymorphic method calls need to be wraped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}.
 In Java this is done implicitly in a process called capture conversion.