Motivation example

introduction.tex

@@ -19,6 +19,57 @@ class Test {
 }
 \end{verbatim}
 
+TypeError:
+\begin{verbatim}
+void test(){
+        var l = new ArrayList<String>();
+        l.add("hi");
+        var  s = l.stream().map(i -> 1).collect(Collectors.toList());
+        var s2 = l.stream().map(i -> "String").collect(Collectors.toList());
+        receive(s, s2);
+    }
+    <A> void receive(List<A> l, List<A> l2){}
+\end{verbatim}
+Correct:
+\begin{verbatim}
+void test(){
+        var l = new ArrayList<String>();
+        l.add("hi");
+        List<Object>  s = l.stream().map(i -> 1).collect(Collectors.toList());
+        List<Object> s2 = l.stream().map(i -> "String").collect(Collectors.toList());
+        receive(s, s2);
+    }
+    <A> void receive(List<A> l, List<A> l2){}
+\end{verbatim}
+
+Error:
+\begin{verbatim}
+rrr(this.emptyBox().set(this.<Integer>emptyBox()).set(this.<String>emptyBox()));
+\end{verbatim}
+Correct:
+\begin{verbatim}
+rrr(this.<Box<?>>emptyBox().set(this.<Integer>emptyBox()).set(this.<String>emptyBox()));
+\end{verbatim}
+
+incorrect:
+\begin{verbatim}
+emptyList().add(emptyList()).head().head()
+\end{verbatim}
+
+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}.
+
+The big difference to local type inference is the ability to have constraints where both sides contain type placeholders.
+As described in \cite{javaTIisBroken} local type inference is able to determine an unifier $\sigma$
+which satisfies $\set{\overline{A <: \sigma(F)}, \sigma(R) <: E }$.
+Note that $A$ and $E$ are already given types.
+$A$ are method arguments and $E$ is the expected return type.
+
+% Are there examples where the expected return type is not given?
+% with global type inference this is easy to produce
+% an example where this is the case for local type inference?
+%   - the val example
+
 \section{Type Inference for Java}
 %The goal is to find a correct typing for a given Java program.
 Type inference for Java has many use cases and could be used to help programmers by inserting correct types for them,

martin.bib

@@ -433,7 +433,7 @@ numpages = {14},
 keywords = {existential types, joins, parametric types, single-instantiation inheritance, subtyping, type inference, wildcards}
 }
 
-@inproceedings{10.1145/1449764.1449804,
+@inproceedings{javaTIisBroken,
 author = {Smith, Daniel and Cartwright, Robert},
 title = {Java type inference is broken: can we fix it?},
 year = {2008},