Java local Type inference intro

introduction.tex

@@ -5,6 +5,26 @@
 % - Constraints und Unifikation erklären, bevor Unifikation erwähnt wird
 
 \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.
+The invocation of \texttt{emptyList} missing type parameters can be added by Java's local type inference
+because the expected return type is known. \texttt{List<String>} in this case.
+\begin{lstlisting}[caption=Extract of a valid Java program]
+<T> List<T> emptyList() { ... }
+
+List<String> ls = emptyList();
+\end{lstlisting}
+
+Local type inference \cite{javaTIisBroken} is able to find a type substitution $\sigma$ satisfying
+$\overline{\type{A} <: \sigma(\type{F}) }, \sigma(\type{R}) <: \type{E}$.
+
+The type parameters are not allowed on the left side of $A <: F$
+We can generate method calls where this is the case. The second call to \texttt{get}.
+
+\begin{verbatim}
+emptyList().get(0).get(0);
+\end{verbatim}
+
 \begin{verbatim}
 import java.util.ArrayList;
 import java.util.stream.*;
@@ -59,6 +79,7 @@ emptyList().add(emptyList()).head().head()
 In this example the return type of \texttt{emptyList} needs to consider that it should contain a list of a list.
 This is a limitation of local type inference as presented here \cite{javaTIisBroken}.
 
+
 % \begin{recap}{Java Local Type Inference}
 % Local type inference is able to solve constraints of the form 
 % T <. b, b <. T where T are given types