add shuffle example to wildcard introduction

introduction.tex

@@ -23,6 +23,9 @@ resulting in a correctly typed program (see figure \ref{fig:nested-list-example-
 
 \begin{itemize}
 \item
+We introduce the language \tifj{} (chapter \ref{sec:tifj}).
+A Featherweight Java derivative including Generics, Wildcards and Type Inference.
+\item
 We support capture conversion and Java style method calls.
 This requires existential types in a form which is not denotable by Java syntax \cite{aModelForJavaWithWildcards}.
 \item
@@ -171,8 +174,6 @@ Wildcards can be formalized as existential types \cite{WildFJ}.
 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}}$.
 
-$\exptype{List}{String} <: \wctype{\wildcard{X}{\bot}{\type{Object}}}{List}{\rwildcard{X}}$
-means \texttt{List<String>} is a subtype of \texttt{List<? extend Object>}.
 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}.
@@ -180,17 +181,69 @@ In this case the name is $\rwildcard{X}$ and it's bound to the the type \texttt{
 Those properties are needed to formalize 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.
-% When calling a polymorphic method like \texttt{<X> List<X> m(List<X> l1, List<X> l2)} with a \texttt{List<?>}
-% it is not possible to substitute \texttt{?} for \texttt{X}.
-% This would lead to the method header \texttt{List<?> m(List<?> l1, List<?> l2)}
-% where now a method invocation with \texttt{List<String>} and \texttt{List<Integer>} would be possible,
-% because both are subtypes of \texttt{List<?>}.
-% Capture conversion solves this problem by generating a fresh type variable for every wildcard.
-% Calling \texttt{<X> X head(List<X> l1)} with the type \texttt{List<?>} ($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$)
-% creates a fresh type variable $\rwildcard{Y}$ resulting in 
-% $\generics{\rwildcard{Y}}\texttt{head}(\exptype{List}{\rwildcard{Y}})$
-% with $\rwildcard{Y}$ being used as generic parameter \texttt{X}.
-% The $\rwildcard{Y}$ in $\exptype{List}{\rwildcard{Y}}$ is a free variable now.
+
+One problem is the divergence between denotable and expressable types in Java \cite{semanticWildcardModel}.
+A wildcard in the Java syntax has no name and is bound to its enclosing type.
+$\exptype{List}{\exptype{List}{\type{?}}}$ equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
+During type checking \emph{intermediate types}
+%like $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$
+%or $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$
+can emerge, which have no equivalent in the Java syntax.
+%Our type inference algorithm uses existential types internally but spawns type solutions compatible with Java.
+
+Example: % This program is not typable with the Type Inference algorithm from Plümicke
+\begin{verbatim}
+class List<X> extends Object {...}
+class List2D<X> extends List<List<X>> {...}
+
+<X> void shuffle(List<List<X>> list) {...}
+
+List<List<?>> l = ...;
+List2D<?> l2d = ...;
+
+shuffle(l); // Error
+shuffle(l2d); // Valid
+\end{verbatim}
+Java is using local type inference to allow method invocations which are not describable with regular Java types.
+The \texttt{shuffle} method in this case is invoked with the type $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$
+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]
+let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in <X>shuffle(l2d')
+\end{lstlisting}
+
+The respective constraints are:
+\begin{constraintset}
+\begin{center}
+    $
+    \begin{array}{l}
+    \wctype{\rwildcard{X}}{List2D}{\rwildcard{X}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
+    \\
+    \hline
+    \wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
+    \\
+    \hline
+    \textit{Capture Conversion:}\ 
+    \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\wtv{x}}}
+    \\
+    \hline
+    \textit{Solution:} \wtv{x} \doteq \rwildcard{X} \implies \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\rwildcard{X}}}
+    \end{array}
+    $
+\end{center}
+\end{constraintset}
+
+\texttt{l} however has the type
+$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
+The method call \texttt{shuffle(l)} is not correct, because there is no solution for the subtype constraint:
+
+$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$
+
+
+
+% $\exptype{List}{String} <: \wctype{\wildcard{X}{\bot}{\type{Object}}}{List}{\rwildcard{X}}$
+% means \texttt{List<String>} is a subtype of \texttt{List<? extend Object>}.
 
 \subsection{Global Type Inference}
 % A global type inference algorithm works on an input with no type annotations at all.
@@ -202,20 +255,25 @@ In Java this is done implicitly in a process called capture conversion.
 
 % $\tv{l} \lessdotCC \exptype{List}{\wtv{x}}, \tv{l} \lessdotCC \wtv{x}$
 
-The input to our type inference algorithm is a modified version of the \letfj{} calculus presented in \cite{WildcardsNeedWitnessProtection}.
-\fjtype{} generates constraints from an input program and is the first step of the algorithm.
-Afterwards \unify{} computes a solution for the given constraint set.
+\begin{description}
+    \item[input] \tifj{} program
+    \item[output] type solution
+    \item[postcondition] the type solution applied to the input must yield a valid \letfj{} program
+\end{description}
+
+The input to our type inference algorithm is a modified version of the \letfj{}\cite{WildcardsNeedWitnessProtection} calculus (see chapter \ref{sec:tifj}).
+First \fjtype{} generates constraints
+and afterwards \unify{} computes a solution for the given constraint set.
 Constraints consist out of subtype constraints $(\type{T} \lessdot \type{T})$ and capture constraints $(\type{T} \lessdotCC \type{T})$.
-Additionally to types constraints can also hold type placeholders $\ntv{a}$ and wildcard type placeholders $\wtv{a}$.
+\textit{Note:} a type $\type{T}$ can also be a type placeholders $\ntv{a}$ or a wildcard type placeholder $\wtv{a}$.
 A subtype constraint is satisfied if the left side is a subtype of the right side according to the rules in figure \ref{fig:subtyping}.
-\textit{Example:} $\exptype{List}{\tv{a}} \lessdot \exptype{List}{\type{String}}$ is fulfilled by replacing type placeholder $\tv{a}$ with the type $\type{String}$.
-Subtype constraints and type placeholders act the same as the ones used in \emph{Type Inference for Featherweight Generic Java} \cite{TIforGFJ}.
+\textit{Example:} $\exptype{List}{\ntv{a}} \lessdot \exptype{List}{\type{String}}$ is fulfilled by replacing type placeholder $\ntv{a}$ with the type $\type{String}$.
+Subtype constraints and type placeholders act the same as the ones used in \emph{Type Inference for Featherweight Generic Java} \cite{TIforFGJ}.
 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
-Our algorithm has to find a type solution and a \letfj{} representation for a given input program.
 Let's start with an example where all types are already given:
 \begin{lstlisting}[style=tfgj, caption=Valid Java program, label=lst:addExample]
 <A> List<A> add(List<A> l, A v)
@@ -238,16 +296,18 @@ Our type inference algorithm has to add let statements if necessary, including t
 
 Lets have a look at the constraints generated by \fjtype{} for the example in listing \ref{lst:addExample}:
 \begin{constraintset}
-$\begin{array}{l}
+\begin{center}
+$\begin{array}{c}
 \wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}, \, \type{String} \lessdotCC \wtv{a}
 \\
 \hline
-\text{Capture Conversion:}\ \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
+\textit{Capture Conversion:}\ \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
 \\
 \hline
-\text{Solution:}\ \wtv{a} \doteq \rwildcard{X} \implies \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\rwildcard{X}}, \, \type{String} \lessdot \rwildcard{X}
+\textit{Solution:}\ \wtv{a} \doteq \rwildcard{X} \implies \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\rwildcard{X}}, \, \type{String} \lessdot \rwildcard{X}
 \end{array}
 $
+\end{center}
 \end{constraintset}
 %Why do we need the lessdotCC constraints here?
 The type of \texttt{l} can be capture converted by a let statement if needed (see listing \ref{lst:addExampleLet}).
@@ -307,13 +367,6 @@ List<?> m() = new List<String>() :? new List<Integer>() :? id(m());
 \subsection{Challenges}\label{challenges}
 %TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
 
-One problem is the divergence between denotable and expressable types in Java \cite{semanticWildcardModel}.
-A wildcard in the Java syntax has no name and is bound to its enclosing type.
-$\exptype{List}{\exptype{List}{\type{?}}}$ equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
-During type checking \emph{intermediate types} like $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$
-or $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ can emerge, which have no equivalent in the Java syntax.
-Our type inference algorithm uses existential types internally but spawns type solutions compatible with Java.
-
 
 The introduction of wildcards adds additional challenges.
 % we cannot replace every type variable with a wildcard

prolog.tex

@@ -15,6 +15,7 @@
 \lstdefinestyle{tfgj}{backgroundcolor=\color{lightgray!20}}
 \lstdefinestyle{letfj}{backgroundcolor=\color{lightgray!20}}
 
+\newcommand{\tifj}{\texttt{TamedFJ}}
 
 \newcommand\mv[1]{{\tt #1}}
 \newcommand{\ol}[1]{\overline{\tt #1}}
@@ -113,7 +114,8 @@
 \newcommand{\wtypestore}[3]{\ensuremath{#1 = \wtype{#2}{#3}}}
 %\newcommand{\wtype}[2]{\ensuremath{[#1\ #2]}}
 \newcommand{\wtv}[1]{\ensuremath{\tv{#1}_?}}
-\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
+%\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
+\newcommand{\ntv}[1]{\tv{#1}}
 \newcommand{\wcstore}{\ensuremath{\Delta}}
 
 %\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}_?}}

tRules.tex

@@ -1,4 +1,4 @@
-\section{Syntax and Typing}
+\section{Syntax and Typing}\label{sec:tifj}
 
 The input syntax for our algorithm is shown in figure \ref{fig:syntax}
 and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}.
@@ -8,6 +8,16 @@ The input language is designed to showcase type inference involving existential
 Method call rule T-Call is the most interesting part, because it emulates the behaviour of a Java method call,
 where existential types are implicitly \textit{opened} and \textit{closed}.
 
+Example: %TODO
+\begin{verbatim}
+class List<A> {
+    A head;
+    List<A> tail;
+
+    add(v) = new List(v, this);
+}
+\end{verbatim}
+
 %The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}.
 %and is solely used for examples.
 The calculus does not include method overriding for simplicity reasons.