Add Recap in introduction

TIforWildFJ.tex

@@ -36,6 +36,7 @@
 \usepackage{cancel}
 \usepackage{tcolorbox}
 \usepackage{arydshln}
+\usepackage{dashbox}
 
 \input{prolog}
 

introduction.tex

@@ -242,12 +242,13 @@ $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype
 
 \section{Type Inference for Capture Conversion}
 why do we need a lessdotCC constraint
-
+\dbox{Eine dashbox!}
 input is e.m(e);
-Recap: TI for FGJ without Wildcards
+\begin{recap}\textbf{TI for FGJ without Wildcards:}
 - usually the type of e must be subtypes of the method parameters
 - in case of a polymorphic method: type placeholders resemble type parameters
-
+\end{itemize}
+\end{recap}
 involving wildcards:
 - depending on the type of e a capture conversion must be applied first
 - the captured type N must be a subtype of the method parameters
@@ -287,21 +288,33 @@ Subtype constraints and type placeholders act the same as the ones used in \emph
 The novel capture constraints and wildcard placeholders are needed for method invocations involving wildcards.
 
 %show input and a correct letFJ representation
-Even in a full typed program local type inference can be necessary.
 %TODO: first show local type inference and explain lessdotCC constraints. then show example with global TI
-Let's start with an example where all types are already given:
+\begin{figure}[h]
+\begin{subfigure}[t]{0.47\textwidth}
+\centering
 \begin{lstlisting}[style=tfgj, caption=Valid Java program, label=lst:addExample]
-<A> List<A> add(List<A> l, A v)
+<A> List<A> add(List<A> l, A v) ...
 
 List<? super String> l = ...;
 add(l, "String");
 \end{lstlisting}
-\begin{lstlisting}[style=letfj, caption=\letfj{} representation of \texttt{add(l, "String")}, label=lst:addExampleLet]
-    let l2 : (*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = l in <X>add(l2, "String");
+\end{subfigure}\hfill
+\begin{subfigure}[t]{0.47\textwidth}
+\centering
+\begin{lstlisting}[style=letfj, caption=\letfj{} 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
+    in <X>add(l2, "String");
 \end{lstlisting}
-In \letfj{} there is no local type inference and all type parameters for a method call are mandatory.
+\end{subfigure}
+\end{figure}
+
+The Example in listing \ref{lst:addExample} is a valid Java program. Here Java uses local type inference \cite{JavaLocalTI}
+to determine the type parameters to the \texttt{add} method call.
+In \letfj{} there is no local type inference and all type parameters for a method call are mandatory (see listing \ref{lst:addExampleLet}).
 If wildcards are involved the so called capture conversion has to be done manually via let statements.
-A let statement \emph{opens} an existential type.
+%A let statement \emph{opens} an existential type.
 In the body of the let statement the \textit{capture type} $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$
 becomes $\exptype{List}{\rwildcard{X}}$ and the wildcard $\wildcard{X}{\type{Object}}{\type{String}}$ is free and can be used as
 a type parameter to \texttt{<X>add(...)}.

martin.bib

@@ -388,4 +388,43 @@ numpages = {14},
 keywords = {existential types, joins, parametric types, single-instantiation inheritance, subtyping, type inference, wildcards}
 }
 
+@inproceedings{10.1145/1449764.1449804,
+author = {Smith, Daniel and Cartwright, Robert},
+title = {Java type inference is broken: can we fix it?},
+year = {2008},
+isbn = {9781605582153},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+url = {https://doi.org/10.1145/1449764.1449804},
+doi = {10.1145/1449764.1449804},
+abstract = {Java 5, the most recent major update to the Java Programming Language, introduced a number of sophisticated features, including a major extension to the type system. While the technical details of these new features are complex, much of this complexity is hidden from the typical Java developer by an ambitious type inference mechanism. Unfortunately, the extensions to the Java 5 type system were so novel that their technical details had not yet been thoroughly investigated in the research literature. As a result, the Java 5 compiler includes a pragmatic but flawed type inference algorithm that is, by design, neither sound nor locally complete. The language specification points out that neither of these failures is catastrophic: the correctness of potentially-unsound results must be verified during type checking; and incompleteness can usually be worked around by manually providing the method type parameter bindings for a given call site.This paper dissects the type inference algorithm of Java 5 and proposes a signficant revision that is sound and able to calculate correct results where the Java 5 algorithm fails. The new algorithm is locally complete with the exception of a difficult corner case. Moreover, the new algorithm demonstrates that several arbitrary restrictions in the Java type system---most notably the ban on lower-bounded type parameter declarations and the limited expressibility of intersection types---are unnecessary. We hope that this work will spur the evolution of a more coherent, more comprehensive generic type system for Java.},
+booktitle = {Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications},
+pages = {505–524},
+numpages = {20},
+keywords = {bounded quantification, generics, intersection types, parameterized types, polymorphic methods, subtyping, type argument inference, type inference, union types, wildcards},
+location = {Nashville, TN, USA},
+series = {OOPSLA '08}
+}
+
+  
+
+@article{JavaLocalTI,
+author = {Smith, Daniel and Cartwright, Robert},
+title = {Java type inference is broken: can we fix it?},
+year = {2008},
+issue_date = {September 2008},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {43},
+number = {10},
+issn = {0362-1340},
+url = {https://doi.org/10.1145/1449955.1449804},
+doi = {10.1145/1449955.1449804},
+abstract = {Java 5, the most recent major update to the Java Programming Language, introduced a number of sophisticated features, including a major extension to the type system. While the technical details of these new features are complex, much of this complexity is hidden from the typical Java developer by an ambitious type inference mechanism. Unfortunately, the extensions to the Java 5 type system were so novel that their technical details had not yet been thoroughly investigated in the research literature. As a result, the Java 5 compiler includes a pragmatic but flawed type inference algorithm that is, by design, neither sound nor locally complete. The language specification points out that neither of these failures is catastrophic: the correctness of potentially-unsound results must be verified during type checking; and incompleteness can usually be worked around by manually providing the method type parameter bindings for a given call site.This paper dissects the type inference algorithm of Java 5 and proposes a signficant revision that is sound and able to calculate correct results where the Java 5 algorithm fails. The new algorithm is locally complete with the exception of a difficult corner case. Moreover, the new algorithm demonstrates that several arbitrary restrictions in the Java type system---most notably the ban on lower-bounded type parameter declarations and the limited expressibility of intersection types---are unnecessary. We hope that this work will spur the evolution of a more coherent, more comprehensive generic type system for Java.},
+journal = {SIGPLAN Not.},
+month = {oct},
+pages = {505–524},
+numpages = {20},
+keywords = {wildcards, union types, type inference, type argument inference, subtyping, polymorphic methods, parameterized types, intersection types, generics, bounded quantification}
+}
 

prolog.tex

@@ -4,17 +4,19 @@
 \lstset{language=Java,
   showspaces=false,
   showtabs=false,
-  breaklines=true,
+  %breaklines=true,
   showstringspaces=false,
-  breakatwhitespace=true,
+  %breakatwhitespace=true,
   basicstyle=\ttfamily\fontsize{8}{9.6}\selectfont, %\footnotesize
   escapeinside={(*@}{@*)},
-  captionpos=b,
+  captionpos=t,float,abovecaptionskip=-\medskipamount
 }
 \lstdefinestyle{fgj}{backgroundcolor=\color{lime!20}}
 \lstdefinestyle{tfgj}{backgroundcolor=\color{lightgray!20}}
 \lstdefinestyle{letfj}{backgroundcolor=\color{lightgray!20}}
 
+\newtheorem{recap}[note]{Recap}
+
 \newcommand{\tifj}{\texttt{TamedFJ}}
 
 \newcommand\mv[1]{{\tt #1}}