Merge branch 'master' of ssh://gitea.hb.dhbw-stuttgart.de:2222/stan/Ecoop2024_TIforWildFJ

modified:   relatedwork.tex

.gitignore

@@ -0,0 +1,23 @@
+## Core latex/pdflatex auxiliary files:
+*.aux
+*.lof
+*.log
+*.lot
+*.fls
+*.out
+*.toc
+*.fmt
+*.fot
+*.cb
+*.cb2
+.*.lb
+*.bbl
+*.bcf
+*.blg
+*-blx.aux
+*-blx.bib
+*.run.xml
+*.vtc
+*.synctex.gz
+auto
+_region_.tex

TIforWildFJ.tex

@@ -1,5 +1,5 @@
 
-\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate]{lipics-v2021}
+\documentclass[anonymous,USenglish]{llncs}
 %This is a template for producing LIPIcs articles. 
 %See lipics-v2021-authors-guidelines.pdf for further information.
 %for A4 paper format use option "a4paper", for US-letter use option "letterpaper"
@@ -40,30 +40,28 @@
 
 \input{prolog}
 
+\begin{document}
 \bibliographystyle{plainurl}% the mandatory bibstyle
 
 \title{Global Type Inference for Featherweight Java with Wildcards} %TODO Please add
 
-%\titlerunning{Dummy short title} %TODO optional, please use if title is longer than one line
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% ANON
 
-\author{Andreas Stadelmeier}{DHBW Stuttgart, Campus Horb, Germany}{a.stadelmeier@hb.dhbw-stuttgart.de}{}{}%TODO mandatory, please use full name; only 1 author per \author macro; first two parameters are mandatory, other parameters can be empty. Please provide at least the name of the affiliation and the country. The full address is optional. Use additional curly braces to indicate the correct name splitting when the last name consists of multiple name parts.
+% \author{Andreas Stadelmeier\inst{1}, Martin Plümicke\inst{1}, Peter Thiemann\inst{2}}
+% \institute{DHBW Stuttgart, Campus Horb, Germany\\
+% \email{a.stadelmeier@hb.dhbw-stuttgart.de} \and
+% Universität Freiburg, Institut für Informatik, Germany\\
+% \email{thiemann@informatik.uni-freiburg.de}}
 
-\author{Martin Plümicke}{DHBW Stuttgart, Campus Horb, Germany}{pl@dhbw.de}{}{}
+% \authorrunning{A. Stadelmeier and M. Plümicke and P. Thiemann}
 
-\author{Peter Thiemann}{Universität Freiburg, Institut für Informatik, Germany}{thiemann@informatik.uni-freiburg.de}{}{}
+%% END ANON
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\authorrunning{A. Stadelmeier and M. Plümicke and P. Thiemann} %TODO mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et al.'
+%\category{} %optional, e.g. invited paper
 
-\Copyright{Andreas Stadelmeier and Martin Plümicke and Peter Thiemann} %TODO mandatory, please use full first names. LIPIcs license is "CC-BY";  http://creativecommons.org/licenses/by/3.0/
+%\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
-
-\ccsdesc[500]{Software and its engineering~Language features}
-%\ccsdesc[300]{Software and its engineering~Syntax}
-
-\keywords{type inference, Java, subtyping, generics} %TODO mandatory; please add comma-separated list of keywords
-
-\category{} %optional, e.g. invited paper
-
-\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
 %\relatedversiondetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93]{Classification (e.g. Full Version, Extended Version, Previous Version}{URL to related version} %linktext and cite are optional
 
 %\supplement{}%optional, e.g. related research data, source code, ... hosted on a repository like zenodo, figshare, GitHub, ...
@@ -77,28 +75,36 @@
 
 
 
-%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% %Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\EventEditors{John Q. Open and Joan R. Access}
+% \EventEditors{John Q. Open and Joan R. Access}
-\EventNoEds{2}
+% \EventNoEds{2}
-\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
+% \EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
-\EventShortTitle{CVIT 2016}
+% \EventShortTitle{CVIT 2016}
-\EventAcronym{CVIT}
+% \EventAcronym{CVIT}
-\EventYear{2016}
+% \EventYear{2016}
-\EventDate{December 24--27, 2016}
+% \EventDate{December 24--27, 2016}
-\EventLocation{Little Whinging, United Kingdom}
+% \EventLocation{Little Whinging, United Kingdom}
-\EventLogo{}
+% \EventLogo{}
-\SeriesVolume{42}
+% \SeriesVolume{42}
-\ArticleNo{23}
+% \ArticleNo{23}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\begin{document}
 
 \maketitle
 
 %TODO mandatory: add short abstract of the document
 \begin{abstract}
-TODO: Abstract
+  Type inference is a hallmark of functional programming. Its use in
+  object-oriented programming is often restricted to type inference
+  for local variables and the instantiation of generic type
+  parameters.
+
+  Global type inference for Featherweight Generic Java is a
+  whole-program analysis that infers omitted method signatures.
+  Compared to previous work, its results are more general as it infers
+  types with wildcards. Global type inference is proved sound.
 \end{abstract}
+\keywords{type inference, Java, subtyping, generics} %TODO mandatory; please add comma-separated list of keywords
 
 \input{introduction}
 
@@ -106,50 +112,26 @@ TODO: Abstract
 
 \input{tRules}
 
+\input{typeinference}
+
 %\input{tiRules}
 
 \input{constraints}
 
 \input{Unify}
 
-\section{Limitations}
+\include{relatedwork}
-
-This example does not work:
-
-\begin{minipage}{0.35\textwidth}
-  \begin{verbatim}
-class Example{
-<A> Pair<A,A> make(List<A> l){...}
-<A> bool compare(Pair<A,A> p){...}
-
-  bool test(List<?> l){
-    return compare(make(l));
-  }
-}
-\end{verbatim}
-  \end{minipage}%
-  \hfill
-  \begin{minipage}{0.55\textwidth}
-\begin{constraintset}
-    \textbf{Constraints:}\\
-    $
-  \wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{x}}, \\
-  \exptype{Pair}{\wtv{x},\wtv{x}} \lessdot \tv{r}, \\
-  \tv{r} \lessdot \exptype{Pair}{\tv{z}, \tv{z}}%,\\
-  %\tv{y} \lessdot \tv{m}
-    $\\
-\end{constraintset}
-  \end{minipage}
-
 
 \input{conclusion}
 
-\include{soundness}
 %\include{termination}
 
 \bibliography{martin}
 
 \appendix
+
+\include{soundness}
+\include{helpers}
 %\include{examples}
 %\input{exampleWildcardParameter}
 %\input{commonPatternsProof}

conclusion.tex

@@ -1,11 +1,138 @@
+%TODO: how are the challenges solved: Describe this in the last chapter with examples!
+\section{Discussion}\label{sec:completeness}
+We couldn't verify it with an implementation yet, but we assume atleast the same functionality
+as the global type inference algorithm for Featherweight Java without Wildcards \cite{TIforFGJ}.
+
+When it comes to wildcards there is a limitation we couldn't find a good workaround:
+\begin{example} This example does not work:
+
+\noindent
+\begin{minipage}{0.51\textwidth}
+  \begin{lstlisting}[style=java]
+class Example{
+<A> Pair<A,A> make(List<A> l){...}
+<A> bool compare(Pair<A,A> p){...}
+
+  bool test(List<?> l){
+    return compare(make(l));
+  }
+}
+\end{lstlisting}
+  \end{minipage}%
+  \hfill
+  \begin{minipage}{0.48\textwidth}
+\begin{lstlisting}[style=constraints]
+(*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{x}}$@*),
+(*@$\exptype{Pair}{\wtv{x},\wtv{x}} \lessdot \ntv{r}$@*),
+(*@$\ntv{r} \lessdot \exptype{Pair}{\wtv{z}, \wtv{z}}$@*)
+\end{lstlisting}
+  \end{minipage}
+\end{example}
+
+%The algorithm can find a solution to every program which the Unify by Plümicke finds
+%a correct solution aswell.
+We will not infer intermediat types like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X},\rwildcard{X}}$
+for a normal type placeholder.
+$\ntv{r}$ will get the type $\wctype{\rwildcard{X},\rwildcard{Y}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$
+which renders the constraint set unsolvable.
+
+% This is our result:
+% \begin{verbatim}
+% class List<X> {
+%     <Y extends X> void addTo(List<Y> l){
+%         l.add(this.get());
+%     }
+% }
+% \end{verbatim}
+% $
+% \tv{l} \lessdotCC \exptype{List}{\wtv{y}},
+% \type{X} \lessdot \wtv{y}
+% $
+% But the most general type would be:
+% \begin{verbatim}
+% class List<X> {
+%     void addTo(List<? super X> l){
+%         l.add(this.get());
+%     }
+% }
+% \end{verbatim}
+
+
+$\ntv{x}$ will get the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and
+from the constraint
+$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
+\unify{} deducts $\wtv{a} \doteq \rwildcard{X}$ leading to 
+$\exptype{Pair}{\rwildcard{X}, \rwildcard{X}} \lessdot \ntv{m}$.
+
+Finding a supertype to $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ is the crucial part.
+The correct substition for $\ntv{r}$ would be $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$.
+But this leads to additional branching inside the \unify{} algorithm and increases runtime.
+%We refrain from using that type, because it is not denotable with Java syntax.
+%Types used for normal type placeholders should be expressable Java types. % They are not!
+This also just solves this specific issue and not the problem in general.
+
+
+% The prefered way of dealing with this example in our opinion would be the addition of a multi-let statement to the syntax.
+
+% \begin{lstlisting}[style=letfj]
+% let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = l, m = make(x) in compare(make(x))
+% \end{lstlisting}
+
+% We can make it work with a special rule in the \unify{}.
+% But this will only help in this specific example and not generally solve the issue.
+% A type $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ has atleast two immediate supertypes:
+% $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ and
+% $\wctype{\rwildcard{X}, \rwildcard{Y}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$.
+% Imagine a type $\exptype{Triple}{\rwildcard{X},\rwildcard{X},\rwildcard{X}}$ already has 
+% % TODO: how many supertypes are there?
+% %X.Triple<X,X,X> <: X,Y.Triple<X,Y,X> <: 
+% %X,Y,Z.Triple<X,Y,Z>
+
+% % TODO example:
+% \begin{lstlisting}[style=java]
+% <X> Triple<X,X,X> sameL(List<X> l)
+% <X,Y> Triple<X,Y,Y> sameP(Pair<X,Y> l)
+% <X,Y> void triple(Triple<X,Y,Y> tr){}
+
+% Pair<?,?> p ...
+% List<?> l ...
+
+% make(t) { return t; }
+% triple(make(sameP(p)));
+% triple(make(sameL(l)));
+% \end{lstlisting}
+
+% \begin{constraintset}
+% $
+% \exptype{Triple}{\rwildcard{X}, \rwildcard{X}, \rwildcard{X}} \lessdot \ntv{t},
+% \ntv{t} \lessdotCC \exptype{Triple}{\wtv{a}, \wtv{b}, \wtv{b}}, \\
+% (\textit{This constraint is added later: } \exptype{Triple}{\rwildcard{X}, \rwildcard{Y}, \rwildcard{Y}} \lessdot \ntv{t})
+% $
+% % Triple<X,X,X> <. t
+% % ( Triple<X,Y,Y> <. t ) <- this constraint is added later
+% % t <. Triple<a?, b?, b?>
+
+% % t =. x.Triple<X,X,X>
+% \end{constraintset}
+
+
 \section{Conclusion and Further Work}
 % we solved the problems given in the introduction (see examples TODO give names to examples)
-The problems introduced in the openening \ref{challenges} can be solved via our \unify{} algorithm (see examples \ref{example1} and \ref{example2}).
+The problems introduced in the openening \ref{challenges} can be solved via our \unify{} algorithm. %(see examples \ref{example1} and \ref{example2}).
-As you can see by the given examples our type inference algorithm can calculate
+Additionally we could prove that type solutions generated by our type inference algorithm are correct respective to \TamedFJ{}'s type rules.
-type solutions for programs involving wildcards.
+The important parts are lemma \ref{lemma:soundness} and \ref{lemma:unifySoundness}.
+They prove that the \unify{} algorithm solves a constraint set according to our subtyping rules
+and that the generated constraints match \TamedFJ{}'s type system.
+%As you can see by the given examples our type inference algorithm can calculate
+%type solutions for programs involving wildcards.
 
-Going further we try to proof soundness and completeness for \unify{}.
+The crucial parts introduced in this paper are capture constraints, wildcard placeholders and existential types.
+Those data structures allow us to solve the problems introduced in chapter \ref{challenges}.
 
+%Going further we try to prove soundness and completeness for \unify{}.
+Our algorithm is designed for extensibility with the final goal of full support for Java.
+\unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
+Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
 
 % The tricks are:
 % \begin{itemize}

constraints.tex

@@ -1,7 +1,5 @@
-\section{Constraint generation}\label{chapter:constraintGeneration}
-% Our type inference algorithm is split into two parts.
-% A constraint generation step \textbf{TYPE} and a \unify{} step.
 
+\section{Constraint generation}\label{chapter:constraintGeneration}
 % Method names are not unique.
 % It is possible to define the same method in multiple classes.
 % The \TYPE{} algorithm accounts for that by generating Or-Constraints.
@@ -9,22 +7,104 @@
 
 %\subsection{Well-Formedness}
 
-Constraint generation step is the same as in \cite{TIforFGJ} except for field access and method invocation.
-Here \fjtype{} generates capture constraints instead of normal subtype constraints.
 
-Subtype constraints are created according to the type rules defined in section \ref{sec:tifj}.
+% But it can be easily adapted to Featherweight Java or Java.
-The \typeExpr{} function creates constraints for a given expression.
+% We add T <. a for every return of an expression anyway. If anything returns a Generic like X it is not directly used in a method call like X <c T
 
-$\begin{array}{c}
+The constraint generation works on the \TamedFJ{} language.
-\typeExpr(\texttt{t}_1, \ntv{b}) = C_l \quad \quad \typeExpr(\texttt{t}_2, \ntv{c}) = C_l \quad \quad \ntv{b}, \ntv{c} \ \text{fresh}
+This step is mostly the same as in \cite{TIforFGJ} except for field access and method invocation.
-\\
+We will focus on those two parts where also the new capture constraints and wildcard type placeholders are introduced.
-\hline
+
-\typeExpr(\texttt{t}_1 \texttt{?:} \texttt{t}_2, \tv{a}) = C_l \cup C_r \cup \set{\ntv{b} \lessdot \tv{a}, \ntv{c} \lessdot \tv{a}}
+%In \TamedFJ{} capture conversion is implicit.
+%To emulate Java's behaviour we assume the input program not to contain any let statements.
+%They will be added by an ANF transformation (see chapter \ref{sec:anfTransformation}).
+
+Before generating constraints the input is transformed by an ANF transformation (see section \ref{sec:anfTransformation}).
+
+%Constraints are generated on the basis of the program in A-Normal form.
+%After adding the missing type annotations the resulting program is valid under the typing rules in \cite{WildFJ}.
+
+%This is shown in chapter \ref{sec:soundness}
+
+%\section{\TamedFJ{}: Syntax and Typing}\label{sec:tifj}
+
+% The syntax forces every expression to undergo a capture conversion before it can be used as a method argument.
+% Even variables have to be catched by a let statement first.
+% This behaviour emulates Java's implicit capture conversion.
+
+\subsection{ANF transformation}\label{sec:anfTransformation}
+\newcommand{\anf}[1]{\ensuremath{\tau}(#1)}
+%https://en.wikipedia.org/wiki/A-normal_form)
+Featherweight Java's syntax involves no \texttt{let} statement
+and terms can be nested freely similar to Java's syntax.
+Our calculus \TamedFJ{} uses let statements to explicitly apply capture conversion to wildcard types,
+but we don't know which expressions will spawn wildcard types because there are no type annotations yet.
+To emulate Java's behaviour we have to preemptively add capture conversion in every suitable place.
+%To convert it to \TamedFJ{} additional let statements have to be added.
+This is done by a \textit{A-Normal Form} \cite{aNormalForm} transformation shown in figure \ref{fig:anfTransformation}.
+After this transformation every method invocation is preceded by let statements which perform capture conversion on every argument before passing them to the method.
+See the example in listings \ref{lst:anfinput} and \ref{lst:anfoutput}.
+\begin{figure}
+\begin{minipage}{0.45\textwidth}
+\begin{lstlisting}[style=fgj,caption=\TamedFJ{} example,label=lst:anfinput]
+m(l, v){
+    return l.add(v);
+}
+\end{lstlisting}
+    \end{minipage}%
+    \hfill
+    \begin{minipage}{0.5\textwidth}
+\begin{lstlisting}[style=tfgj,caption=A-Normal form,label=lst:anfoutput]
+m(l, v) = 
+    let x1 = l in
+        let x2 = v in x1.add(x2)
+\end{lstlisting}
+\end{minipage}
+\end{figure}
+
+\begin{figure}
+    \begin{center}
+$\begin{array}{lrcl}
+%\text{ANF}
+& \anf{\expr{x}} & = & \expr{x} \\
+& \anf{\texttt{new} \ \type{C}(\overline{t})} & = & \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}}) \\
+& \anf{t.f} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \expr{x}.f \\
+& \anf{t.\texttt{m}(\overline{t})} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \expr{x}.\texttt{m}(\overline{\expr{x}}) \\
+& \anf{t_1 \elvis{} t_2} & = & \anf{t_1} \elvis{} \anf{t_2} \\
+& \anf{\texttt{let}\ x = \expr{t}_1 \ \texttt{in}\ \expr{t}_2} & = & \texttt{let}\ x = \anf{\expr{t}_1} \ \texttt{in}\ \anf{\expr{t}_2} 
+\end{array}$
+\end{center}
+\caption{ANF Transformation $\tau$}\label{fig:anfTransformation}
+\end{figure}
+
+\begin{figure}
+  \center
+$
+\begin{array}{lrcl}
+%\hline
+\text{Terms} & t & ::= & \expr{x} \\
+& & \ \ | &  \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}_c}) \\
+& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \expr{x}_c.f \\
+& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \expr{x}_c.\texttt{m}(\overline{\expr{x}_c}) \\
+& & \ \ | & t \elvis{} t \\
+%\hline
 \end{array}
 $
+\caption{Syntax of a \TamedFJ{} program in A-Normal Form}\label{fig:anf-syntax}
+\end{figure}
 
-The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
+\subsection{Constraint Generation Algorithm}
-Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
+% Generally subtype constraints for an expression mirror the subtype relations in the premise of the respective type rule introduced in section \ref{sec:tifj}.
+% Unknown types at the time of the constraint generation step are replaced with type placeholders.
+
+% The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
+% Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
+
+The parameter types given to a generic method also affect their return type.
+During constraint generation the algorithm does not know the parameter types yet.
+We generate $\lessdotCC$ constraints and let \unify{} do the capture conversion.
+$\lessdotCC$ constraints are kept until they reach the form $\type{G} \lessdotCC \type{G}$ and a capture conversion is possible.
+% TODO: Challenge examples!
 
 At points where a well-formed type is needed we use a normal type placeholder.
 Inside a method call expression sub expressions (receiver, parameter) wildcard placeholders are used.
@@ -33,25 +113,12 @@ A normal type placeholder cannot hold types containing free variables.
 Normal type placeholders are assigned types which are also expressible with Java syntax.
 So no types like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ or $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
 
-Type variables declared in the class header are passed to \unify{}.
+It is possible to feed the \unify{} algorithm a set of free variables with predefined bounds.
+This is used for class generics see figure \ref{fig:constraints-for-classes}.
+The \fjtype{} function returns a set of constraints aswell as an initial environment $\Delta$
+containing the generics declared by this class.
 Those type variables count as regular types and can be held by normal type placeholders.
 
-
-There are two different types of constraints:
-\begin{description}
-\item[$\lessdot$] \textit{Example:}
-
-$\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}$
-
-\noindent
-Those two constraints imply that we have to find a type replacement for type variable $\tv{a}$,
-which is a supertype of $\exptype{List}{String}$ aswell as $\exptype{List}{Integer}$.
-This paper describes a \unify{} algorithm to solve these constraints and calculate a type solution $\sigma$.
-For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
-\item[$\lessdotCC$] TODO
-% The \fjtype{} algorithm assumes capture conversions for every method parameter.
-\end{description}
-
 %Why do we need a constraint generation step?
 %% The problem is NP-Hard
 %% a method call, does not know which type it will produce
@@ -59,48 +126,37 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
 
 %NO equals constraints during the constraint generation step!
 \begin{figure}[tp]
-  \begin{align*}
+  \center
-    % Type
+\begin{tabular}{lcll}
-    \type{T}, \type{U} &::= \tv{a} \mid \wtv{a} \mid \mv{X} \mid {\wcNtype{\Delta}{N}} && \text{types and type placeholders}\\
+    $C $ &$::=$ &$\overline{c}$ & Constraint set \\
-    \type{N} &::= \exptype{C}{\il{T}} && \text{class type (with type variables)} \\
+    $c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \lessdotCC \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
-    % Constraints
+    $\type{T}, \type{U}, \type{L} $ & $::=$ & $\tv{a} \mid \gtype{G}$ & Type placeholder or Type \\
-    \simpleCons &::= \type{T} \lessdot \type{U} && \text{subtype constraint}\\
+    $\tv{a}$ & $::=$ & $\ntv{a} \mid \wtv{a}$ & Normal and wildcard type placeholder \\
-    \orCons{} &::= \set{\set{\overline{\simpleCons_1}}, \ldots, \set{\overline{\simpleCons_n}}} && \text{or-constraint}\\
+    $\gtype{G}$ & $::=$ & $\type{X} \mid \ntype{N}$ & Wildcard, or Class Type \\
-    \constraint &::= \simpleCons \mid \orCons && \text{constraint}\\
+    $\ntype{N}, \ntype{S}$ & $::=$ & $\wctype{\triangle}{C}{\ol{T}} $ & Class Type \\
-    \consSet &::= \set{\constraints} && \text{constraint set}\\
+    $\triangle$ & $::=$ & $\overline{\wtype{W}}$ & Wildcard Environment \\
-    % Method assumptions:
+    $\wtype{W}$ & $::=$ & $\wildcard{X}{U}{L}$ & Wildcard \\
-    \methodAssumption &::= \exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \exptype{}{\ol{Y}
+\end{tabular}
-                        \triangleleft \ol{P}}\ \ol{\type{T}} \to \type{T}  &&
+  \caption{Syntax of types and constraints used by \fjtype{} and \unify{}}
-                                                                \text{method
-                                                                type assumption}\\
-    \localVarAssumption &::= \texttt{x} : \itype{T} && \text{parameter
-                                                       assumption}\\
-    \mtypeEnvironment & ::= \overline{\methodAssumption} &
-                & \text{method type environment} \\
-    \typeAssumptionsSymbol &::= ({\mtypeEnvironment} ; \overline{\localVarAssumption}) 
-  \end{align*}
-  \caption{Syntax of constraints and type assumptions.}
   \label{fig:syntax-constraints}
 \end{figure}
 
 \begin{figure}[tp]
   \begin{gather*}
     \begin{array}{@{}l@{}l}
-      \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\ol{X} \triangleleft \ol{N}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, K \, \overline{M} \}}) =\\
+      \fjtype & ({\mtypeEnvironment }, \mathtt{class } \ \exptype{C}{\overline{\type{X} \triangleleft \type{N}}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\
               & \begin{array}{ll@{}l}
-\textbf{let} & \forall \texttt{m} \in \ol{M}: \tv{a}_\texttt{m}, \ol{\tv{a}_m} \ \text{fresh} \\
+\textbf{let} & \ol{\methodAssumption} =
-             & \ol{\methodAssumption} = \begin{array}[t]{l}
+                \set{ \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \mid
-                \set{ \mv{m'} : (\exptype{C}{\ol{X} \triangleleft \ol{N}} \to \ol{\tv{a}} \to \tv{a}) \mid
+                  \set{ \mv{m}(\ol{x}) = \expr{e} } \in \ol{M}, \, \tv{a}, \ol{\tv{a}}\ \text{fresh} } \\
-                  \mv{m'} \in \ol{M} \setminus \set{\mv{m}}, \, \tv{a}\, \ol{\tv{a}}\ \text{fresh} } \\
+              & \Delta = \set{ \overline{\wildcard{X}{\type{N}}{\bot}} } \\
-\ \cup \, \set{\mv{m} : (\exptype{C}{\ol{X} \triangleleft \ol{N}} \to \ol{\tv{a}_m} \to \tv{a}_\mv{m})}
+              & C = \begin{array}[t]{l}
-\end{array}
+                \set{ \typeExpr(\mtypeEnvironment \cup \ol{\methodAssumption} \cup \set{\mv{this} :
- \\
+              \exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}} }, \texttt{e}, \tv{a})
-              & C_m = \typeExpr(\mtypeEnvironment \cup \set{\mv{this} :
+               \\ \quad \quad \quad \quad \mid \set{ \mv{m}(\ol{x}) = \expr{e} }  \in \ol{M},\, \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \in \ol{\methodAssumption}}
-                \exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}_m} }, \texttt{e}, \tv{a}_\texttt{m}) \\
+                  \end{array} \\
               \textbf{in} 
-              & { ( \mtypeEnvironment \cup \ol{\methodAssumption}, \,
+                  & (\Delta, C)
-                \bigcup_{\texttt{m} \in \ol{M}} C_m )
-                } 
                 \end{array}
     \end{array}
   \end{gather*}
@@ -108,51 +164,18 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
   \label{fig:constraints-for-classes}
 \end{figure}
 
-% \textbf{Method Assumptions}
-
-% %$\Pi$ is a set of method assumptions used by the $\fjtype{}$ algorithm.
-
-% % \begin{verbatim}
-% % class Example<X> {
-% %   <Y> Y m(Example<Y> p){ ... }
-% % }
-% % \end{verbatim}
-
-% In Featherweight Java a method type is bound to a specific class.
-% The class \texttt{Example} shown above contains one method \texttt{m}:
-
-% \begin{displaymath}
-% \textit{mtype}({\texttt{m}, \exptype{Example}{\type{X}}}) = \generics{\type{Y}} \ \exptype{Example}{\type{Y}} \to \type{Y}
-% \end{displaymath}
-
-% $\Pi$ is a set of method assumptions used by the $\fjtype{}$ algorithm.
-% It's a map of method types to method names.
-% Every method name has a set of possible types,
-% because there could be more than one method with the same name in a program consisting out of multiple classes.
-% To simplify the syntax of method assumptions, we add the inheriting class type to the parameter list:
-
-% \begin{displaymath}
-% \Pi = \set{ \texttt{m} : \generics{\type{X}, \type{Y}} \ (\exptype{Example}{\type{X}}, \exptype{Example}{\type{Y}}) \to \type{Y}}
-% \end{displaymath}
-
-% \begin{verbatim}
-% class Example<X> { }
-
-% <X, Y> Y m(Example<X> this, Example<Y> p){ ... }
-% \end{verbatim}
-
 \begin{displaymath}
   \begin{array}{@{}l@{}l}
-    \typeExpr{} &({\mtypeEnvironment} , \texttt{e}.\texttt{f}, \tv{a}) = \\
+    \typeExpr{} &({\mtypeEnvironment}, \Gamma , \texttt{e}.\texttt{f}, \tv{a}) = \\
                 & \begin{array}{ll}
                     \textbf{let} 
                     & \tv{r} \ \text{fresh} \\
-                    & \consSet_R = \typeExpr({\mtypeEnvironment}, \texttt{e}, \tv{r})\\
+                    & \consSet_R = \typeExpr({\mtypeEnvironment}, \Gamma, \texttt{e}, \tv{r})\\
                     & \constraint = \begin{array}[t]{@{}l@{}l}
                       \orCons\set{
                       \set{ &
                       \tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}} ,
-                      [\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} ,
+                      \tv{a} \doteq [\overline{\wtv{a}}/\ol{X}]\type{T},
                       \ol{\wtv{a}} \lessdot [\overline{\wtv{a}}/\ol{X}]\ol{N}
                       } \\
                       & \quad \mid \mv{T}\ \mv{f} \in \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}
@@ -164,139 +187,51 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
   \end{array}
 \end{displaymath}
 
-The set of method assumptions returned by the \textit{mtypes} function is used to generate the constraints for a method call expression:
+\begin{displaymath}
-
+  \begin{array}{@{}l@{}l}
-There are two kinds of method calls.
+    \typeExpr{} &({\mtypeEnvironment}, \Gamma , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2, \tv{a}) = \\
-The ones to already typed methods and calls to untyped methods.
+                & \begin{array}{ll}
+                    \textbf{let} 
+                    & \tv{e}_1, \tv{e}_2, \tv{x} \ \text{fresh} \\
+                    & \consSet_1 = \typeExpr({\mtypeEnvironment}, \Gamma, \expr{e}_1, \tv{e}_1)\\
+                    & \consSet_2 = \typeExpr({\mtypeEnvironment } \cup \set{\expr{x} : \tv{x}}, \expr{e}_2, \tv{e}_2)\\
+                    & \constraint =
+                      \set{
+                      \tv{e}_1 \lessdot \tv{x}, \tv{e}_2 \lessdot \tv{a}
+                      }\\
+                    {\mathbf{in}} & {
+                      \consSet_1 \cup \consSet_2 \cup \set{\constraint}}
+                  \end{array} 
+  \end{array}
+\end{displaymath}
 
 \begin{displaymath}
   \begin{array}{@{}l@{}l}
-      \typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a}) = \\
+      \typeExpr{} & ({\mtypeEnvironment}, \Gamma , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\
       & \begin{array}{ll}
       \textbf{let}
       & \tv{r}, \ol{\tv{r}} \text{ fresh} \\
-      & \consSet_R = \typeExpr(({\mtypeEnvironment} ;
+      & \constraint = [\overline{\wtv{b}}/\ol{Y}]\set{
-        \overline{\localVarAssumption}), \texttt{e}, \tv{r})\\
+                    \ol{S} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a}, 
-      & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \ol{e}, \ol{\tv{r}})  \\
+                    \ol{Y} \lessdot \ol{N} }\\
-      & \begin{array}{@{}l@{}l}
+      \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T}) \\
-        \constraint = \orCons\set{ & 
+      & \mathbf{where}\ \begin{array}[t]{l}
-                  \begin{array}[t]{l}
+        \expr{v}, \ol{v} : \ol{S} \in \localVarAssumption \\
-                    [\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdotCC \exptype{C}{\ol{X}},
+        \texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T} \in {\mtypeEnvironment }
-                    \overline{\tv{r}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a}, 
+      \end{array}
-                    \ol{Y} \lessdot \ol{N} \}
+                    
-                  \end{array}\\
-            & \ |\ 
-            (\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T}) \in 
-                {\mtypeEnvironment} %, \, |\ol{T}| = |\ol{e}|
-            , \, \overline{\wtv{a}} \text{ fresh}}
-        \end{array}\\
-      \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T})
       \end{array}
       \end{array}
   \end{displaymath}
-\\[1em]
-\noindent
-\textbf{Example:}
-\begin{verbatim}
-class Class1{
-  <X> X m(List<X> lx, List<? extends X> lt){ ... }
-  List<? extends String> wGet(){ ... }
-  List<String> get() { ... }
-}
-
-class Class2{
-  example(c1){
-    return c1.m(c1.get(), c1.wGet());
-  }
-}
-\end{verbatim}
-%This example comes with predefined type annotations.
-We assume the class \texttt{Class1} has already been processed by our type inference algorithm,
-which has lead to the given type annotations for \texttt{Class1}.
-Now we call the $\fjtype{}$ function with the class \texttt{Class2} and the method assumptions for the preceeding class:
-\begin{displaymath}
-\mtypeEnvironment =  \left\{\begin{array}{l}
-    \type{Class1}.\texttt{m}: \generics{\type{X} \triangleleft \type{Object}} \ 
-      (\exptype{List}{\type{X}}, \, \wctype{\wildcard{A}{\type{X}}{\bot}}{List}{\wildcard{A}{\type{X}}{\bot}}) \to \type{X}, \\
-     \type{Class1}.\texttt{wGet}: () \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\wildcard{A}{\type{Object}}{\type{String}}}, \\
-     \type{Class1}.\texttt{get}: () \to \exptype{List}{\type{String}}
-\end{array} \right\} 
-\end{displaymath}
-
-The result of the $\typeExpr{}$ function is the constraint set
-\begin{displaymath}
-C = \left\{ \begin{array}{l}
-\tv{c1} \lessdot \type{Class1}, \\
-\tv{p1} \lessdot \exptype{List}{\wtv{x}}, \\
-\exptype{List}{\type{String}} \lessdot \tv{p1}, \\
-\tv{p2} \lessdot \wctype{\wildcard{A}{\wtv{x}}{\bot}}{List}{\rwildcard{A}}, \\
-\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{p2} 
-\end{array} \right\}
-\end{displaymath}
-
-
-The first parameter of a method assumption is the receiver type $\type{T}_r$.
-\texttt{Class1} for this example.
-Therefore the $(\tv{c1} \lessdot \type{Class1})$ constraint.
-The type variable $\tv{c1}$ is assigned to the parameter \texttt{c1} of the \texttt{example} method.
-
-or a simplified version:
-
-\begin{displaymath}
-C = \left\{ \begin{array}{l}
-\tv{c1} \lessdot \type{Class1}, \\
-\exptype{List}{\type{String}} 
- \lessdot \exptype{List}{\wtv{x}}, \\
-\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}
- \lessdot \wctype{\wildcard{A}{\wtv{x}}{\bot}}{List}{\rwildcard{A}}
-\end{array} \right\}
-\end{displaymath}
-
-
-$\wtv{x}$ is a type variable we use for the generic $\type{X}$. It is flagged as a free type variable.
-%TODO: Do an example where wildcards are inserted and we need capture conversion
-
-\unify{} returns the solution $(\sigma = \set{ \tv{x} \to \type{String} })$
-
-% \\[1em]
-% \noindent
-% \textbf{Example:}
-% \begin{verbatim}
-% class Class1 {
-%   <X> Pair<X, X> make(List<X> l){ ... }
-%   <Y> boolean compare(Pair<Y,Y> p) { ... }
-
-%   example(l){
-%     return compare(make(l));
-%   }
-% }
-% \end{verbatim}
-
-% The method call \texttt{make(l)} generates the constraints
-% \begin{displaymath}
-%   \tv{l} \lessdot \exptype{List}{\tv{x}}, \exptype{Pair}{\tv{x}, \tv{x}} \lessdot \tv{m}
-% \end{displaymath}
-% with $\tv{l}$ being the type placeholder for the variable \texttt{l}
-% and $\tv{m}$ is the type variable for the return type of the method call.
-% $\tv{m}$ is then used as the parameter for the \texttt{compare} method:
-% \begin{displaymath}
-%   \tv{m} \lessdot \exptype{Pair}{\tv{y}, \tv{y}}
-% \end{displaymath}
-% Note the conversion of the generic parameters \texttt{X} and \texttt{Y} to type variables $\tv{x}$ and $\tv{y}$.
-
-
-
-% Step 3 of the \unify{} algorithm has to look for every possible supertype of $\exptype{Pair}{\tv{x}, \tv{x}}$,
-% when processing the $\exptype{Pair}{\tv{x}, \tv{x}} \lessdot \tv{m}$ constraint.
 
 \begin{displaymath}
   \begin{array}{@{}l@{}l}
-    \typeExpr{} &({\mtypeEnvironment} , e_1 \elvis{} e_2, \tv{a}) = \\
+    \typeExpr{} &({\mtypeEnvironment}, \Gamma , e_1 \elvis{} e_2, \tv{a}) = \\
                 & \begin{array}{ll}
                     \textbf{let} 
                     & \tv{r}_1, \tv{r}_2 \ \text{fresh} \\
-                    & \consSet_1 = \typeExpr({\mtypeEnvironment}, e_1, \tv{r}_2)\\
+                    & \consSet_1 = \typeExpr({\mtypeEnvironment}, \Gamma, e_1, \tv{r}_2)\\
-                    & \consSet_2 = \typeExpr({\mtypeEnvironment}, e_2, \tv{r}_2)\\
+                    & \consSet_2 = \typeExpr({\mtypeEnvironment}, \Gamma, e_2, \tv{r}_2)\\
                     {\mathbf{in}} & {
                     \consSet_1 \cup \consSet_2 \cup
                         \set{\tv{r}_1 \lessdot \tv{a}, \tv{r}_2 \lessdot \tv{a}}}
@@ -307,25 +242,289 @@ $\wtv{x}$ is a type variable we use for the generic $\type{X}$. It is flagged as
 %We could skip wfresh here:
 \begin{displaymath}
   \begin{array}{@{}l@{}l}
-    \typeExpr{} &({\mtypeEnvironment} , x, \tv{a}) = 
+    \typeExpr{} &({\mtypeEnvironment}, \Gamma , x, \tv{a}) = 
     \mtypeEnvironment(x)
   \end{array}
 \end{displaymath}
 
 \begin{displaymath}
   \begin{array}{@{}l@{}l}
-    \typeExpr{} &({\mtypeEnvironment} , \texttt{new}\ \type{C}(\overline{e}), \tv{a}) = \\
+    \typeExpr{} &({\mtypeEnvironment}, \Gamma , \texttt{new}\ \type{C}(\overline{e}), \tv{a}) = \\
                 & \begin{array}{ll}
                     \textbf{let} 
-                    & \ol{\tv{r}} \ \text{fresh} \\
+                    & \ol{\ntv{r}}, \ol{\ntv{a}} \ \text{fresh} \\
-                    & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \overline{e}, \ol{\tv{r}}) \\
+                    & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \Gamma, \overline{e}, \ol{\ntv{r}}) \\
-                    & C = \set{\ol{\tv{r}} \lessdot [\ol{\tv{a}}/\ol{X}]\ol{T}, \ol{\tv{a}} \lessdot \ol{N} \mid \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}} \\
+                    & C = \set{\ol{\ntv{r}} \lessdot [\ol{\ntv{a}}/\ol{X}]\ol{T}, \ol{\ntv{a}} \lessdot \ol{N} \mid \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}} \\
                     {\mathbf{in}} & {
                     \overline{\consSet} \cup
-                        \set{\tv{a} \doteq \exptype{C}{\ol{a}}}}
+                        \set{\tv{a} \doteq \exptype{C}{\ol{\ntv{a}}}}}
                   \end{array} 
   \end{array}
 \end{displaymath}
+\\[1em]
+\noindent
+\begin{example}
+Given the following input program missing type annotations for the \texttt{example} method:
+\begin{lstlisting}[style=java]
+class Class1{
+  <A> A head(List<X> l){ ... }
+  List<? extends String> get() { ... }
+}
+
+class Class2{
+  example(c1){
+    return c1.head(c1.get());
+  }
+}
+\end{lstlisting}
+%This example comes with predefined type annotations.
+We assume the class \texttt{Class1} has already been processed by our type inference algorithm
+leading to the following type annotations:
+%Now we call the $\fjtype{}$ function with the class \texttt{Class2} and the method assumptions for the preceeding class:
+\begin{displaymath}
+\mtypeEnvironment =  \left\{\begin{array}{l}
+    \texttt{m}: \generics{\type{A} \triangleleft \type{Object}} \ 
+      (\type{Class1},\, \exptype{List}{\type{A}}) \to \type{X}, \\
+     \texttt{get}: (\type{Class1}) \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\rwildcard{A}}
+\end{array} \right\} 
+\end{displaymath}
+
+At first we have to convert the example method to a syntactically correct \TamedFJ{} program.
+Afterwards the the \fjtype{} algorithm is able to generate constraints.
+
+\noindent
+\begin{minipage}{0.52\textwidth}
+  \begin{lstlisting}[style=tamedfj]
+class Class2 {
+  example(c1) = let x = c1 in
+    let xp = x.get() in x.m(xp);
+}
+\end{lstlisting}
+      \end{minipage}%
+      \hfill
+      \begin{minipage}{0.46\textwidth}
+\begin{lstlisting}[style=constraints]
+(*@$\ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}$@*),
+(*@$\ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}$@*),
+(*@$\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{xp}$@*),
+(*@$\tv{xp} \lessdotCC \exptype{List}{\wtv{a}}$@*)
+\end{lstlisting}
+\end{minipage}
+
+Following is a possible solution for the given constraint set:
+
+\noindent
+\begin{minipage}{0.55\textwidth}
+  \begin{lstlisting}[style=tamedfj]
+class Class2 {
+ example(c1) = let x :Class1 = c1 in
+  let xp :(*@$\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*) = x.get()
+   in x.m(xp);
+}
+\end{lstlisting}
+      \end{minipage}%
+      \hfill
+      \begin{minipage}{0.43\textwidth}
+\begin{lstlisting}[style=constraints]
+(*@$\sigma(\ntv{x}) = \type{Class1}$@*),
+(*@$\sigma(\tv{xp}) = \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*)
+  \end{lstlisting}
+\end{minipage}
+
+For $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$ to be a correct solution for $\tv{xp}$
+the constraint $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{a}}$
+must be satisfied.
+This is possible, because we deal with a capture constraint.
+The $\lessdotCC$ constraint allows the left side to undergo a capture conversion
+which leads to $\exptype{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{a}}$.
+Now a substitution of the wildcard placeholder $\wtv{a}$ with $\rwildcard{A}$ leads to a satisfied constraint set.
+\end{example}
+
+The wildcard placeholders are not used as parameter or return types of methods.
+Or as types for variables introduced by let statements.
+They are only used for generic method parameters during a method invocation.
+Type placeholders which are not flagged as wildcard placeholders ($\wtv{a}$) can never hold a free variable or a type containing free variables.
+This practice hinders free variables to leave their scope.
+The free variable $\rwildcard{A}$ generated by the capture conversion on the type $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$
+cannot be used anywhere else then inside the constraints generated by the method call \texttt{x.m(xp)}.
+
+\subsection{Constraint Generation}
+The constraint generation is defined on a subset of Java displayed in figure \ref{fig:miniJavaSyntax}.
+The input language includes only a small set of expressions like method calls, field access and a elvis operator $\elvis$
+which acts as a replacement for if-else expressions.
+\begin{figure}
+\par\noindent\rule{\textwidth}{0.4pt}
+\center
+$
+\begin{array}{lrcl}
+%\hline
+\text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
+\text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
+\text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
+\text{Type variable contexts} &  \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
+\text{Class declarations} &  D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\
+\text{Method declarations} &  \texttt{M} & ::= & \highlight{\generics{\overline{\type{X} \triangleleft \type{N}}}}\ \highlight{\type{T}}\ \texttt{m}(\overline{\highlight{\type{T}}\ \expr{x}}) \{ \texttt{return} \ \expr{e}; \} \\
+\text{Terms} & \expr{e} & ::= & \expr{x} \\
+& & \ \ | & \texttt{new} \ \type{C}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
+& & \ \ | & \expr{e}.f\\
+& & \ \ | & \expr{e}.\texttt{m}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
+& & \ \ | & \expr{e} \elvis{} \expr{e}\\
+\text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
+\text{Method type environment} & \mathrm{\Pi} & ::= & \overline{ \texttt{m} : \generics{\ol{X \triangleleft N}}\ \ol{T} \to \type{T}}
+%\hline
+\end{array}
+$
+\par\noindent\rule{\textwidth}{0.4pt}
+\caption{Input Syntax with optional type annotations}\label{fig:miniJavaSyntax}
+\end{figure}
+
+We explain the process using the following example input.
+The classes \texttt{List} and \texttt{Id} are already fully typed and we want to create constraints for the class
+\texttt{CExample} now.
+
+\begin{lstlisting}{java}
+class Id{
+  <X> X id(X x){ return x; }
+}
+
+class List<X> {
+  <Y extends X> List<X> concat(List<Y> l){ ... }
+}
+
+class CExample{
+  example(p1, p2) {
+    return p1.id(p2).concat(p2);
+  }
+}
+\end{lstlisting}
+
+The first step of constraint generation is to assign type placeholders to every expression in the input program.
+Type placeholders also fill in for missing type annotations in method headers.
+
+\begin{lstlisting}{java}
+class CExample{
+  example(p1, p2) {
+    return p1.id(p2).concat(p2);
+  }
+}
+\end{lstlisting}  
+\begin{lstlisting}{java}
+class CExample{
+  (*@$\tv{a}$@*) example((*@$\tv{b}$@*) p1, (*@$\tv{c}$@*) p2) {
+    return ((p1:(*@$\tv{b}$@*)).id(p2:(*@$\tv{c}$@*)):(*@$\tv{d}$@*)).concat(p2:(*@$\tv{c}$@*)) : (*@$\tv{e}$@*);
+  }
+}
+\end{lstlisting}  
+
+The placeholders $\tv{a}-\tv{e}$ are freshly created in this example and added to every expression.
+The type of local variable expressions like \expr{p1} and \expr{p2} is already known and can be assigned directly.
+$\expr{p1}:\tv{b}$ and $\expr{p2}:\tv{c}$ in this case.
+The method call to \texttt{id} gets the fresh type placeholder $\tv{d}$ as type and the method call to \texttt{concat} is assigned the placeholder $\tv{e}$.
+
+Afterwards we create a method type environment $\mtypeEnvironment$ containing all method declarations.
+Each entry has the form $\texttt{m} : \generics{\ol{X \triangleleft N}} \ol{T} \to \type{T}$.
+The type arguments of the surrounding class and the type arguments of each method are merged together
+leading to the list $\generics{\type{X}, \type{Y} \triangleleft \type{X}}$ for the \texttt{concat} method
+($\triangleleft$ is short for \texttt{extends}).
+Also the type of the surrounding class is added to the parameter list of the method.
+This leads to the \texttt{id} method having two arguments.
+One is the \texttt{Id} class itself and the second one is the actual arguemnt of the method.
+
+$\mtypeEnvironment{} = \left\{ \begin{array}{l}
+\texttt{id} : \generics{\type{X}}\type{Id},\type{X} \to \type{X}, \\
+\texttt{concat} : \generics{\type{X}, \type{Y} \triangleleft \type{X}}\exptype{List}{\type{X}},\exptype{List}{\type{Y}} \to \exptype{List}{\type{X}}, \\
+\texttt{example} : \type{CExample},\tv{b},\tv{c} \to \tv{a}, \\
+\end{array} \right\} 
+$
+
+Note: type placeholders are used for the \texttt{example} method.
+
+Our constraint generation rules have the form:
+$\mtypeEnvironment \vdash \expr{e} : \tv{a} \implies C$,
+that given a method environment $\mtypeEnvironment$ and an expression $\expr{e}$ with type $\tv{a}$ generates the constraint set $C$.
+
+%Inference-rule in the style of: https://dl.acm.org/doi/pdf/10.1145/345099.345100
+\begin{mathpar}
+  \inferrule[Method-Cons]{
+      \mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C \\
+      \overline{\mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C} \\
+      \texttt{m} : \generics{\ol{Y \triangleleft N}}\type{T}_r, \overline{\type{T}} \to \type{T} \in { \mtypeEnvironment }\\
+      \overline{\wtv{b}}, \tv{x}, \overline{\tv{x}} \ \text{fresh} \\
+      C_m = \set{\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}}} \cup
+      [\overline{\wtv{b}}/\ol{Y}]\set{ \tv{x} \lessdotCC \type{T}_r, \overline{\tv{x} \lessdotCC \type{T}}, \type{T} \lessdot \tv{a}, \overline{Y \lessdot N} } 
+  }{
+      \mtypeEnvironment \vdash \expr{e}.\texttt{m}(\overline{\expr{e}}) : \tv{a} \implies C \cup \overline{C} \cup C_m
+  }
+  \and
+%  \inferrule[Field-Cons]{
+%    \mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C \\
+%    C_f = \set{}
+%  }{
+%    \mtypeEnvironment \vdash \expr{e}.\texttt{f} : \tv{a} \implies C \cup C_f \\
+%  }
+%  \and
+  \inferrule[Var-Cons]{
+  }{
+    \mtypeEnvironment \vdash \expr{x} : \tv{a} \implies \emptyset
+  }
+  \and
+  \inferrule[Elvis-Cons]{
+    \mtypeEnvironment \vdash \expr{e}_1 : \tv{e}_1 \implies C_1 \\
+    \mtypeEnvironment \vdash \expr{e}_2 : \tv{e}_2 \implies C_2
+  }{
+    \mtypeEnvironment \vdash \expr{e}_1 \elvis{} \expr{e}_2 : \tv{a} \implies C_1 \cup C_2 \cup \set{\tv{e}_1 \lessdot \tv{a}, \tv{e}_2 \lessdot \tv{a}}
+  }
+  \and
+  \inferrule[New-Cons]{
+      \overline{\mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C} \\
+      \texttt{class} \ \exptype{D}{\ol{X \triangleleft N}} \set{ \ol{T\ f}; \ldots }
+  }{
+    \mtypeEnvironment \vdash \texttt{new}\ \type{D}(\ol{e}) : \tv{a} \implies \overline{C} \cup [\ol{\wtv{b}}/\ol{X}]\set{ \overline{\tv{e} \lessdot \type{T}}, \exptype{D}{\ol{X}} \lessdot \tv{a}, \ol{X \lessdot N} }
+  }
+\end{mathpar}
+
+According to the Method-Cons rule the constraints generated by the call to \texttt{id} are:
+$\mtypeEnvironment \vdash (p1:\tv{b}).id(p2:\tv{c}):\tv{d} \implies \set{\tv{b} \lessdot \tv{x}_1, \tv{c} \lessdot \tv{x}_2, \tv{x}_1 \lessdotCC \type{Id},
+\tv{x}_2 \lessdotCC \wtv{b}, \wtv{b} \lessdot \tv{d}}$.
+
+\subsection{Or-Constraints}
+In case the input program contains multiple method declarations holding the same name and same amount of parameters then so called Or-Constraints must be generated.
+Usually Java is able to determine which method to call based on the argument's types passed to the method. %'
+During the constraint generation step the argument types are unknown and we have to assume multiple methods as invocation target.
+
+\begin{lstlisting}
+class String{
+  bool equals(String s){ .. }
+}
+class Int{
+  bool equals(Int i){ .. }
+}
+class OrConsExample{
+  m(a, b){
+    return a.equals(b);
+  }
+}
+\end{lstlisting}
+
+The method call to \texttt{equals} now has multiple possibilities.
+It could either be a call to the method in the class \texttt{Int} or in \texttt{String}.
+The method type environment therfore contains two versions of the \texttt{equals} method:
+
+$\mtypeEnvironment{} = \set{ \texttt{equals}_1 : \type{String}, \type{String} \to \type{bool}, 
+\texttt{equals}_2 : \type{Int}, \type{Int} \to \type{bool}}$
+
+The Or-Cons rule considers multiple declarations of the same method separately and joins all of them into a Or-Constraint.
+
+\begin{mathpar}
+  \inferrule[Or-Cons]{
+    \texttt{m}_1 \ldots \texttt{m}_n \in \text{dom}(\mtypeEnvironment{}) \\
+    \mtypeEnvironment \vdash \expr{e}.\texttt{m}_1(\overline{\expr{e}}) : \tv{a} \implies C_1 \quad
+    \ldots \quad
+    \mtypeEnvironment \vdash \expr{e}.\texttt{m}_n(\overline{\expr{e}}) : \tv{a} \implies C_n
+  }{
+      \mtypeEnvironment \vdash \expr{e}.\texttt{m}(\overline{\expr{e}}) : \tv{a} \implies \orCons{}(C_1, \ldots, C_n)
+  }
+\end{mathpar}
 
 % Problem:
 % <X, A extends List<X>> void t2(List<A> l){}
@@ -410,3 +609,7 @@ $\wtv{x}$ is a type variable we use for the generic $\type{X}$. It is flagged as
 % \ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} }
 % \end{array}
 % \end{displaymath}
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "TIforWildFJ"
+%%% End:

helpers.tex

@@ -0,0 +1,34 @@
+
+\section{Additional Functions}
+\begin{description}
+\item[$\tph{}$] returns all type placeholders inside a given type.
+
+\textit{Example:} $\tph(\wctype{\wildcard{X}{\tv{a}}{\bot}}{Pair}{\wtv{b},\rwildcard{X}}) = \set{\tv{a}, \wtv{b}}$
+
+%\textbf{Wildcard renaming}\\
+\item[Wildcard renaming:]
+The \rulename{Reduce} rule separates wildcards from their environment.
+At this point each wildcard gets a new and unique name.
+To only rename the respective wildcards the reduce rule renames wildcards up to alpha conversion:
+($[\ol{C}/\ol{B}]$ in the \rulename{reduce} rule)
+\begin{align*}
+  [\type{A}/\type{B}]\type{B} &= \type{A} \\
+  [\type{A}/\type{B}]\type{C} &= \type{C} & \text{if}\ \type{B} \neq \type{C}\\
+  [\type{A}/\type{B}]\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} &= \wcNtype{\overline{\wildcard{X}{[\type{A}/\type{B}]\type{U}}{[\type{A}/\type{B}]\type{L}}}}{[\type{A}/\type{B}]N} & \text{if}\ \type{B} \notin \overline{\rwildcard{X}} \\
+  [\type{A}/\type{B}]\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} &= \wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} & \text{if}\ \type{B} \in \overline{\rwildcard{X}} \\
+\end{align*}
+\item[Free Variables:]
+The $\text{fv}$ function assumes every wildcard type variable to be a free variable aswell.
+% TODO: describe a function which determines free variables? or do an example?
+\begin{align*}
+\text{fv}(\rwildcard{A}) &= \set{ \rwildcard{A} } \\
+\text{fv}(\tv{a}) &= \emptyset \\
+%\text{fv}(\wtv{a}) &= \set{\wtv{a}} \\
+\text{fv}(\wctype{\Delta}{C}{\ol{T}}) &= \set{\text{fv}(\type{T}) \mid \type{T} \in \ol{T}} / \text{dom}(\Delta) \\
+\end{align*}
+
+\item[Fresh Wildcards:]
+$\text{fresh}\ \overline{\wildcard{A}{\tv{u}}{\tv{l}}}$ generates fresh wildcards.
+The new names $\ol{A}$ are fresh, aswell as the type variables $\ol{\tv{u}}$ and $\ol{\tv{l}}$,
+which are used for the upper and lower bounds.
+\end{description}

introduction.tex

@@ -4,35 +4,210 @@
 % - Kapitel 1.2 + 1.3 ist noch zu komplex
 % - Constraints und Unifikation erklären, bevor Unifikation erwähnt wird
 
-\section{Type Inference for Java}
+%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
+
+
+% \begin{recap}\textbf{TI for FGJ without Wildcards:}
+% \TFGJ{} generates subtype constraints $(\type{T} \lessdot \type{T})$ consisting of named types and type placeholders.
+% For example the method invocation \texttt{concat(l, new Object())} generates the constraints
+% $\tv{l} \lessdot \exptype{List}{\tv{a}}, \type{Object} \lessdot \tv{a}$.
+% Subtyping without the use of wildcards is invariant \cite{FJ}:
+% Therefore the only possible solution for the type placeholder $\tv{a}$ is $\tv{a} \doteq \type{Object}$. % in Java and Featherweight Java.
+% The correct type for the variable \texttt{l} is $\exptype{List}{\type{Object}}$ (or a direct subtype).
+% %- usually the type of e must be subtypes of the method parameters
+% %- in case of a polymorphic method: type placeholders resemble type parameters
+% The type inference algorithm for Featherweight Generic Java \cite{TIforFGJ} (called \TFGJ{}) is complete and sound:
+% It is able to find a type solution for a Featherweight Generic Java program, which has no type annotations at all,
+% if there is any.
+% It's only restriction is that no polymorphic recursion is allowed.
+% \end{recap}
+
+\section{Introduction}
+\label{sec:introduction}
+
+Type inference is a hallmark of functional programming, where it
+improves readability and conciseness while 
+enabling safe rapid prototyping by allowing the compiler to deduce
+types automatically without explicit type annotations. It allows
+developers to safely refactor their programs before fixing function
+signatures.  In object-oriented programming (OOP), however, the use of
+type inference is more restricted. It is often employed for local
+variables and the instantiation of generic type parameters, offering
+similar readability and conciseness benefits as in functional
+programming. In languages like Java, the overall architecture of
+method signatures must be designed by the programmer up-front.
+
+Java features a limited form of local type inference for local
+variables defined with  the \texttt{var} keyword, lambda expressions,
+and method calls. Java infers the type of variables defined with
+\texttt{var}. The rationale here is that instantiations of generic 
+types (e.g., maps of maps) are often unwiedly and they can be easily
+inferred from the initializing expression. The type of a lambda
+expression is inferred from the target type, i.e., the type of the
+method argument that accepts the lambda. The rationale is the intended
+use of lambdas as callback functions for listeners etc. For calls
+to generic methods, Java infers the most specific instantiation of the
+generic parameters for each individual call. 
+
+The local type inference features of Java add some convenience, but
+programmers still have to provide method signatures beforehand. So there
+is scope for a global type inference algorithm that infers
+method signatures even if no type information (except class headers
+and types of field variables) is given.
+We present such a global type inference algorithm for Featherweight
+Generic Java with wildcards, a Java core calculus with generics and
+wildcards in the tradition of Featherweight Java \cite{FJ} and its
+extensions \cite{WildFJ,WildcardsNeedWitnessProtection}. Our approach can also be used for regular Java programs,
+but we limit the formal presentation to this core calculus.
+
 %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,
+Our algorithm enables programmers to write Java code with only a
-finding better type solutions for already typed Java programs (for example more generical ones),
+minimum of type annotations (class headers and types of field
-or allowing to write typeless Java code which is then type infered and thereby type checked by our algorithm.
+variables), it can fill in missing type annotations in partially
-The algorithm proposed in this paper can determine a correct typing for the untyped Java source code example shown in figure \ref{fig:intro-example-typeless}.
+type-annotated programs, and it can suggest better (more general)
-Our algorithm is also capable of finding solutions involving wildcards as shown in figure \ref{fig:intro-example-typed}.
+types for ordinary, typed Java programs.
+
+Listing~\ref{lst:intro-example-typeless} shows an example input of a
+method implementation without any type annotation. Our algorithm
+infers the type annotations in Listing~\ref{lst:intro-example-typed}:
+it adds the type arguments to \texttt{List} at object creation and it
+infers the most specific return type \texttt{List<?>}, which is a
+wildcard type. Our algorithm is the first to infer wildcard types that
+comes with a soundness proof.
+Previous work on global type inference for Java either does not
+consider wildcards or it simplifies the problem by not modeling key
+features of Java wildcards.
+
+
+%The algorithm proposed in this paper can determine a correct typing for the untyped Java source code example shown in listing \ref{lst:intro-example-typeless}.
+%In this case our algorithm would also be able to propose a solution including wildcards as shown in listing \ref{lst:intro-example-typed}.
 
 %This paper extends a type inference algorithm for Featherweight Java \cite{TIforFGJ} by adding wildcards.
 %The last step to create a type inference algorithm compatible to the Java type system.
-The algorithm presented in this paper is a slightly improved version of the one in \cite{TIforFGJ} including wildcard support.
-%a modified version of the \unify{} algorithm presented in \cite{plue09_1}.
-The input to the type inference algorithm is a Featherweight Java program (example in figure \ref{fig:nested-list-example-typeless}) conforming to the syntax shown in figure \ref{fig:syntax}.
-The \fjtype{} algorithm calculates constraints based on this intermediate representation,
-which are then solved by the \unify{} algorithm
-resulting in a correctly typed program (see figure \ref{fig:nested-list-example-typed}).
 
+
+\begin{figure}[tp]
+\begin{minipage}{0.43\textwidth}
+\begin{lstlisting}[style=java,label=lst:intro-example-typeless,caption=Missing return type]
+genList() {
+  if( ... ) {
+    return new List(1);
+  } else {
+    return new List("Str");
+  }
+}
+    \end{lstlisting}
+\end{minipage}%
+\hfill
+\begin{minipage}{0.55\textwidth}
+\begin{lstlisting}[style=tfgj,caption=Type inference solution,label=lst:intro-example-typed]
+List<?> genList() {
+  if( ... ) {
+    return new List<Integer>(1);
+  } else {
+    return new List<String>("Str");
+  }
+}
+    \end{lstlisting}
+\end{minipage}
+\end{figure}
+  
+
+
+Global Type Inference for Featherweight Java \cite{TIforFGJ} is a
+sound, but incomplete inference algorithm for Featherweight Generic
+Java. It does not support wildcards, which means that it infers the
+return type \texttt{Object} for the method \texttt{genList} in
+Listing~\ref{lst:intro-example-typeless}. Like our algorithm, their
+algorithm restricts to monomorphic recursion, which leads to
+incompleteness. 
+
+
+A type unification algorithm for Java with wildcards \cite{plue09_1} states the same capabilities,
+but it does not handle capture conversion correctly because it only supports types which are expressible in Java syntax (more details in
+section~\ref{challenges}).  
+Moreover, it appears that the subtype relation changes depending on whether a type is used as an argument to a method invocation.
+We resolve this problem by modeling Java wildcards as existential
+types \cite{WildFJ,WildcardsNeedWitnessProtection}, which also serve
+as the basis of our soundness proof.
+% forces us to define a new kind of subtype constraint. %, the current state of the art
+%and is able to deal with types that are not directly denotable in Java. 
+
+
+%The algorithm presented in this paper is able to solve all those challenges correctly
+%and it's correctness is proven using a Featherweight Java calculus \cite{WildFJ}.
+%But they are all correctly solved by our new type inference algorithm presented in this paper.
+
+
+\begin{lstlisting}[caption=Part of a valid Java program, style=tfgj, label=lst:tiExample,float=tp]
+<T> List<T> emptyList() { ... }
+
+List<String> ls = emptyList();
+\end{lstlisting}
+Standard Java provides type inference in a restricted form % namely {Local Type Inference}.
+which only works for local environments where the surrounding context has known types.
+The example in Listing~\ref{lst:tiExample} exhibits the main differences to our global type inference algorithm.
+The method call \texttt{emptyList} lacks its type parameters.
+Java relies on a matching algorithm \cite{javaTIisBroken} to instantiate \texttt{T} with \texttt{String} 
+resulting in the correct expected type \texttt{List<String>}.
+This local type inference depends on the type annotation on the left side of the assignment.
+When calling the \texttt{emptyList} method without this type context
+its return value will be inferred as \texttt{List<Object>}.
+Therefore, Java rejects the code snippet in Listing~\ref{lst:tiLimit}:
+it infers the type  \texttt{List<Object>} for
+\texttt{emptyList()} instead of the required
+$\exptype{List}{\exptype{List}{String}}$. 
+\begin{lstlisting}[caption=Limitations of Java's Type Inference,
+  label=lst:tiLimit, float=tp]
+emptyList().add(new List<String>())
+    .get(0)
+    .get(0); //Typing Error
+\end{lstlisting}
+%List<String> <. A
+%List<A> <: List<B>, B <: List<C> 
+% B = A and therefore A on the left and right side of constraints.
+% this makes matching impossible
+Hence, the second call to \texttt{get} produces a type error.
+
+The type inference algorithm presented in this paper correctly instantiates the type parameter \texttt{T} of the \texttt{emptyList}
+method with \texttt{List<List<String>>} and render this code snippet correct.
+
+
+% %motivate constraints: 
+% To solve this example our Type Inference algorithm will create constraints
+% $
+% \exptype{List}{\tv{a}} \lessdot \tv{b},
+% \tv{b} \lessdot \exptype{List}{\tv{c}},
+% \tv{c} \lessdot \exptype{List}{\tv{d}}
+% $
+
+
+
+%\subsection{Conclusion}
+% Additions: TODO
+% - Global Type Inference Algorithm, no type annotations are needed
+% - Soundness Proof 
+% - Easy to implement
+% - Capture Conversion support
+% - Existential Types support
+We summarize our contributions:
 \begin{itemize}
 \item
-We introduce the language \tifj{} (chapter \ref{sec:tifj}).
+We introduce the language \tifj{} (section \ref{sec:tifj}), 
-A Featherweight Java derivative including Generics, Wildcards and Type Inference.
+a Featherweight Java derivative including generics, wildcards, and type inference.
 \item
-We support capture conversion and Java style method calls.
+  Our algorithm handles existential types in a form which is not
-This requires existential types in a form which is not denotable by Java syntax \cite{aModelForJavaWithWildcards}.
+  denotable by Java syntax \cite{aModelForJavaWithWildcards}. Thus, we support capture conversion and Java style method calls.
 \item
   We present a novel approach to deal with existential types and capture conversion during constraint unification.
-The algorithm is split in two parts. A constraint generation step and an unification step.
+% \item The algorithm is split in two parts. A constraint generation step and an unification step.
+% Input language and constraint generations can be extended without altering the unification part.
 \item
-We proof soundness and aim for a good compromise between completeness and time complexity.
+  We prove soundness and aim for a good compromise between completeness and time complexity.
 \end{itemize}
 % Our algorithm finds a correct type solution for the following example, where the Java local type inference fails:
 % \begin{verbatim}
@@ -52,107 +227,6 @@ We proof soundness and aim for a good compromise between completeness and time c
 % }
 % \end{verbatim}
 
-\begin{figure}%[tp]
-      \begin{subfigure}[t]{\linewidth}
-\begin{lstlisting}[style=fgj]
-class List<A> {
-    List<A> add(A v) { ... }
-}
-
-class Example {
-    m(l, la, lb){
-        return l
-            .add(la.add(1))
-            .add(lb.add("str"));
-    }
-}
-\end{lstlisting}
-        \caption{Java method with missing return type}
-        \label{fig:nested-list-example-typeless}
-      \end{subfigure}
-      ~
-%       \begin{subfigure}[t]{\linewidth}
-% \begin{lstlisting}[style=tfgj]
-% class List<A> {
-%     List<A> add(A v) { ... }
-% }
-
-% class Example {
-%     m(l, la, lb){
-%         return let r2 : (*@$\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$@*) = {
-%             let r1 : (*@$\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$@*) = l in {
-%                 let p1 : (*@$\exptype{List}{\type{Integer}}$@*) = {
-%                     let xa = la in xa.add(1)
-%                     } in x1.add(p1)    
-%             } in {
-%                 let p2 = {
-%                     let xb = lb in xb.add("str")
-%                     } in x2.add(p2)
-%             };
-%     }
-% }
-% \end{lstlisting}
-%         \caption{Featherweight Java Representation}
-%         \label{fig:nested-list-example-let}
-%       \end{subfigure}
-%       ~
-      \begin{subfigure}[t]{\linewidth}
-\begin{lstlisting}[style=tfgj]
-class List<A> {
-    List<A> add(A v) { ... }
-}
-
-class Example {
-    m(List<List<? extends Object>> l, List<Integer> la, List<String> lb){
-        return l
-            .add(la.add(1))
-            .add(lb.add("str"));
-    }
-}
-\end{lstlisting}
-        \caption{Java Representation}
-        \label{fig:nested-list-example-typed}
-      \end{subfigure}
-      %\caption{Example code}
-      %\label{fig:intro-example-code}
-\end{figure}
-
-
-%TODO
-% The goal is to proof soundness in respect to the type rules introduced by \cite{aModelForJavaWithWildcards}
-% and \cite{WildcardsNeedWitnessProtection}.
-
-\begin{figure}%[tp]
-      \begin{subfigure}[t]{0.49\linewidth}
-    \begin{lstlisting}[style=fgj]
-genList() {
-    if( ... ) {
-        return new List<String>();
-    } else {
-        return new List<Integer>();
-    }
-}
-    \end{lstlisting}
-        \caption{Java method with missing return type}
-        \label{fig:intro-example-typeless}
-      \end{subfigure}
-      ~
-      \begin{subfigure}[t]{0.49\linewidth}
-    \begin{lstlisting}[style=tfgj]
-List<?> genList() {
-    if( ... ) {
-        return new List<String>();
-    } else {
-        return new List<Integer>();
-    }
-}
-    \end{lstlisting}
-        \caption{Correct type}
-        \label{fig:intro-example-typed}
-      \end{subfigure}
-      %\caption{Example code}
-      %\label{fig:intro-example-code}
-\end{figure}
 
 % \subsection{Wildcards}
 % Java subtyping involving generics is invariant.
@@ -162,438 +236,150 @@ List<?> genList() {
 % \texttt{List<Object>} is not a valid return type for the method \texttt{genList}.
 % The type inference algorithm has to find the correct type involving wildcards (\texttt{List<?>}).
 
-\subsection{Java Wildcards}
+\section{Java Wildcards}
-Wildcards are expressed by a \texttt{?} in Java and can be used as type parameters.
+\label{sec:java-wildcards}
-Wildcards add variance to Java type parameters.
-Generally Java has invariant subtyping for polymorphic 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}.
 
-Wildcards can be formalized as existential types \cite{WildFJ}.
+As Java is an imperative language, subtyping for generic types is invariant.
-\texttt{List<? extends Object>} and \texttt{List<? super String>} are both wildcard types
+%but it incooperates use-site variance via so called wildcard types.
-denoted in our syntax by $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$ and
+Even though \texttt{String} is subtype of \texttt{Object},
-$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
+a \texttt{List<String>} is not a subtype of \texttt{List<Object>}:
+because someone might store an  \texttt{Integer} in the list, which is
+compatible with \texttt{Object}, but not with \texttt{String} (see Listing~\ref{lst:invarianceExample}).
 
-The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound at the same time,
+Invariance is overly restrictive in read-only or write-only
-and a type they are bound to.
+contexts. Hence, Java incooperates use-site variance by allowing wildcards (\texttt{?}) in types.
-In this case the name is $\rwildcard{X}$ and it's bound to the the type \texttt{List}.
+For example, the type \texttt{List<?>} (short for \texttt{List<? extends Object>}, with \texttt{?} being a placeholder for any type)
+is a supertype of \texttt{List<String>} and \texttt{List<Object>}.
+%The \texttt{?} is a wildcard type which can be replaced by any type as needed.
+%
+Listing~\ref{lst:wildcardIntro} shows a use of wildcards that renders the assignment \texttt{lo = ls} correct.
+The program still does not compile, because the addition of an \texttt{Integer} to \texttt{lo} is still incorrect.
 
-Those properties are needed to formalize capture conversion.
+\begin{figure}[tp]
-Polymorphic method calls need to be wraped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}.
+\begin{minipage}{0.48\textwidth}
-In Java this is done implicitly in a process called capture conversion.
+\begin{lstlisting}[caption=Java Invariance Example,label=lst:invarianceExample]{java}
-
+List<String> ls = ...;
-One problem is the divergence between denotable and expressable types in Java \cite{semanticWildcardModel}.
+List<Object> lo = ...;
-A wildcard in the Java syntax has no name and is bound to its enclosing type.
+lo = ls; // typing error!
-$\exptype{List}{\exptype{List}{\type{?}}}$ equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
+lo.add(new Integer(1));
-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}
-
+\end{minipage}
-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}}}$
-
-\section{Type Inference for Capture Conversion}
-why do we need a lessdotCC constraint
-\dbox{Eine dashbox!}
-input is e.m(e);
-\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{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
-- type parameters: can be set to free variables!
-    - but must afterwards be closed again
-    - the free variables can only be used inside the let statement
-- we align the let statements in a way thate mimics Java capture conversion:
-
-
-% $\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.
-% \begin{verbatim}
-% m(l) {
-%     return l.add(l);
-% }
-% \end{verbatim}
-
-% $\tv{l} \lessdotCC \exptype{List}{\wtv{x}}, \tv{l} \lessdotCC \wtv{x}$
-
-\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})$.
-\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}{\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
-%TODO: first show local type inference and explain lessdotCC constraints. then show example with global TI
-\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) ...
-
-List<? super String> l = ...;
-add(l, "String");
-\end{lstlisting}
-\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}
-\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.
-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(...)}.
-%This is a valid Java program where the type parameters for the polymorphic method \texttt{add}
-%are determined by local type inference.
-Our type inference algorithm has to add let statements if necessary, including the capture types.
-
-Lets have a look at the constraints generated by \fjtype{} for the example in listing \ref{lst:addExample}:
-\begin{constraintset}
-\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
-\textit{Capture Conversion:}\ \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
-\\
-\hline
-\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}).
-Therefore we assign the constraint $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$
-which allows \unify{} to do a capture conversion to $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
-\textit{Note:} The constraint $\type{String} \lessdot \rwildcard{X}$ is satisfied because $\rwildcard{X}$ has $\type{String}$ as lower bound.
-
-% No capture conversion for methods in the same class:
-% Given two methods without type annotations like
-% \begin{verbatim}
-% // m :: () -> r
-% m() = new List<String>() :? new List<Integer>();
-
-% // id :: (a) -> a
-% id(a) = a
-% \end{verbatim}
-
-% and a method call \texttt{id(m())} would lead to the constraints:
-% $\exptype{List}{\type{String}} \lessdot \ntv{r},
-% \exptype{List}{\type{Integer}} \lessdot \ntv{r},
-% \ntv{r} \lessdotCC \ntv{a}$
-
-% In this example capture conversion is not applicable,
-% because the \texttt{id} method is not polymorphic.
-% The type solution provided by \unify{} for this constraint set is:
-% $\sigma(\ntv{r}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, 
-% \sigma(\ntv{a}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$
-% \begin{verbatim}
-% List<?> m() = new List<String>() :? new List<Integer>();
-% List<?> id(List<?> a) = a
-% \end{verbatim}
-
-The following example has the \texttt{id} method already typed and the method \texttt{m}
-extended by a recursive call \texttt{id(m())}:
-\begin{verbatim}
-<A> List<A> id(List<A> a) = a
-
-m() = new List<String>() :? new List<Integer>() :? id(m());
-\end{verbatim}
-Now the constraints make use of a $\lessdotCC$ constraint:
-$\exptype{List}{\type{String}} \lessdot \ntv{r},
-\exptype{List}{\type{Integer}} \lessdot \ntv{r},
-\ntv{r} \lessdotCC \exptype{List}{\wtv{a}}$
-
-After substituting $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\ntv{r}$ like in the example before
-we get the constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$.
-Due to the $\lessdotCC$ \unify{} is allowed to perform a capture conversion yielding
-$\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
-\textit{Note:} The wildcard placeholder $\wtv{a}$ is allowed to hold free variables whereas a normal placeholder like $\ntv{r}$
-is never assigned a type containing free variables.
-Therefore \unify{} sets $\wtv{a} \doteq \rwildcard{X}$, completing the constraint set and resulting in the type solution:
-\begin{verbatim}
-List<?> m() = new List<String>() :? new List<Integer>() :? id(m());
-\end{verbatim}
-
-
-\subsection{Challenges}\label{challenges}
-%TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
-
-
-The introduction of wildcards adds additional challenges.
-% we cannot replace every type variable with a wildcard
-Type variables can also be used as type parameters, for example
-$\exptype{List}{String} \lessdot \exptype{List}{\tv{a}}$.
-A problem arises when replacing type variables with wildcards.
-
-% Wildcards are not reflexive.
-% ( on the equals property ), every wildcard has to be capture converted when leaving its scope
-
-% do not substitute free type variables
-
-Lets have a look at two examples:
-\begin{itemize}
-\item \begin{example} \label{intro-example1}
-The first one is a valid Java program.
-The type \texttt{List<? super String>} is \textit{capture converted} to a fresh type variable $\rwildcard{X}$
-which is used as the generic method parameter \texttt{A}.
-
-Java uses capture conversion to replace the generic \texttt{A} by a capture converted version of the
-\texttt{? super String} wildcard.
-Knowing that the type \texttt{String} is a subtype of any type the wildcard \texttt{? super String} can inherit
-it is safe to pass \texttt{"String"} for the first parameter of the function.
-
-\begin{verbatim}
-<A> List<A> add(List<A> l, A v) {}
-
-List<? super String> list = ...;
-add("String", list);
-\end{verbatim}
-\end{example}
-
-\item \begin{example}\label{intro-example2}
-This example displays an incorrect Java program.
-The method call to \texttt{concat} with two wildcard lists is unsound.
-Each list could be of a different kind and therefore the \texttt{concat} cannot succeed.
-\begin{verbatim}
-<A> List<A> concat(List<A> l1, List<A> l2) { ... }
-
-List<?> list = ... ;
-concat(list, list);
-\end{verbatim}
-
-
-% $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}, \\
-% \wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
-\end{example}
-
-% \item 
-% \unify{} morphs a constraint set into a correct type solution
-% gradually assigning types to type placeholders during that process.
-% Solved constraints are removed and never considered again.
-% In the following example \unify{} solves the constraint generated by the expression
-% \texttt{l.add(l.head())} first, which results in $\ntv{l} \lessdot \exptype{List}{\wtv{a}}$.
-% \begin{verbatim}
-% anyList() = new List<String>() :? new List<Integer>()
-
-% add(anyList(), anyList().head());
-% \end{verbatim}
-% The type for \texttt{l} can be any kind of list, but it has to be a invariant one.
-% Assigning a \texttt{List<?>} for \texttt{l} is unsound, because the type list hiding behind
-% \texttt{List<?>} could be a different one for the \texttt{add} call than the \texttt{head} method call.
-% An additional constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
-% is solved by removing the wildcard $\rwildcard{X}$ if possible.
-
-
-\end{itemize}
-
-The \unify{} algorithm only sees the constraints with no information about the program they originated from.
-The main challenge was to find an algorithm which computes $\sigma(\wtv{a}) = \rwildcard{X}$ for example \ref{intro-example1} but not for example \ref{intro-example2}.
-
-\subsection{Capture Conversion}
-The input to our type inference algorithm does not contain let statements.
-Those are added after computing a type solution.
-Let statements act as capture conversion and only have to be applied in method calls involving wildcard types.
-
-\begin{figure} 
-  \begin{minipage}{0.45\textwidth}
-\begin{lstlisting}[style=fgj]
-<X> List<X> clone(List<X> l);
-example(p){
-  return clone(p);
-}
-\end{lstlisting}
-    \end{minipage}%
 \hfill
 \begin{minipage}{0.5\textwidth}
-\begin{lstlisting}[style=tfgj]
+\begin{lstlisting}[caption=Use-Site Variance Example,label=lst:wildcardIntro]{java}
-(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){
+List<String> ls = ...;
-  return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in
+List<? extends Object> lo = ...;
-   clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
+lo = ls; // correct
-}
+lo.add(new Integer(1)); // error!
 \end{lstlisting}
 \end{minipage}
-\caption{Type inference adding capture conversion}\label{fig:addingLetExample}
 \end{figure}
 
-Figure \ref{fig:addingLetExample} shows a let statement getting added to the typed output.
+Wildcard types like \texttt{List<?>} are virtual types, i.e., the run-time 
-The method \texttt{clone} cannot be called with the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
+type of an object is always a fully instantiated type like
-After a capture conversion \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$ with $\rwildcard{X}$ being a free variable.
+\texttt{List<String>} or \texttt{List<Object>}.
-Afterwards we have to find a supertype of $\exptype{List}{\rwildcard{X}}$, which does not contain free variables
+The issue is that the run-time type underlying a wildcard type can
-($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in this case).
+change at any time, for example when multiple threads share a reference to the same field.
+Hence, a wildcard \texttt{?} must be considered a different type everytime it is accessed.
+For that reason, the  call to the method \texttt{concat} with two wildcard lists in Listing~\ref{lst:concatError} is rejected.
+% 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{?}.
 
-During the constraint generation step most types are not known yet and are represented by a type placeholder.
+\begin{figure}[tp]
-During a methodcall like the one in the \texttt{example} method in figure \ref{fig:ccExample} the type of the parameter \texttt{p}
+\begin{lstlisting}[caption=Wildcard Example with faulty call to a concat method,label=lst:concatError]{java}
-is not known yet.
+<X> List<X> concat(List<X> l1, List<X> l2){
-The type \texttt{List<?>} would be one possibility as a parameter type for \texttt{p}.
+    return l1.addAll(l2);
-To make wildcards work for our type inference algorithm \unify{} has to apply capture conversions if necessary.
-
-The type placeholder $\tv{r}$ is the return type of the \texttt{example} method.
-One possible type solution is $\tv{p} \doteq \tv{r} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$,
-which leads to:
-\begin{verbatim}
-List<?> example(List<?> p){
-  return clone(p);
 }
-\end{verbatim}
 
-But by substituting $\tv{p} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in the constraint
+List<?> l1 = new List<String>("foo");
-$\tv{p} \lessdotCC \exptype{List}{\wtv{x}}$ leads to
+List<?> l2 = new List<Integer>(1); // List containing Integer
-$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$.
 
-To make this typing possible we have to introduce a capture conversion via a let statement:
+concat(l1, l2); // Error! Would concat two different lists
-$\texttt{return}\ (\texttt{let}\ \texttt{x} : \wctype{\rwildcard{X}}{List}{\rwildcard{X}} = \texttt{p}\ \texttt{in} \
+\end{lstlisting}
-\texttt{clone}\generics{\rwildcard{X}}(x) : \wctype{\rwildcard{X}}{List}{\rwildcard{X}})$
-
-Inside the let statement the variable \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$
-
-
-This spawns additional problems.
-
-\begin{figure} 
-\begin{minipage}{0.45\textwidth}
-\begin{verbatim}
-<X> List<X> clone(List<X> l){...}
-
-example(p){
-  return clone(p);
-}
-\end{verbatim}
-  \end{minipage}%
-  \hfill
-  \begin{minipage}{0.35\textwidth}
-\begin{constraintset}
-    \textbf{Constraints:}\\
-    $
-  \tv{p} \lessdotCC \exptype{List}{\wtv{x}}, \\
-\tv{p} \lessdot \tv{r}, \\
-\tv{p} \lessdot \type{Object}, 
-\tv{r} \lessdot \type{Object}
-    $
-\end{constraintset}
-  \end{minipage}
-
-\caption{Type inference example}\label{fig:ccExample}
 \end{figure}
 
-In addition with free variables this leads to unwanted behaviour.
+To determine the correctness of method calls involving wildcard types Java's typechecker
-Take the constraint
+makes use of a concept called \textbf{capture conversion}.
-$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ for example.
+%  was designed to make Java wildcards useful.
-After a capture conversion from $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ to $\exptype{List}{\rwildcard{Y}}$ and a substitution $\wtv{a} \doteq \rwildcard{Y}$
+% - without capture conversion 
-we get
+% - is used to open wildcard types
-$\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$.
+% - 
-Which is correct if we apply capture conversion to the left side:
+One way to formalize this concept is by replacing wildcards with
-$\exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$
+existential types and modeling capture conversion with suitably
-If the input constraints did not intend for this constraint to undergo a capture conversion then \unify{} would produce an invalid
+inserted let statements \cite{WildcardsNeedWitnessProtection}. 
-type solution due to:
+Our Featherweight Java derivative called \TamedFJ{} is modeled after
-$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \nless: \exptype{List}{\rwildcard{X}}$
+Bierhoff's calculus \cite{WildcardsNeedWitnessProtection} (see section~\ref{sec:tifj}).
-The reason for this is the \texttt{S-Exists} rule's premise
+To express the example in Listing~\ref{lst:wildcardIntro} in our calculus we first translate the wildcard types:
-$\text{dom}(\Delta') \cap \text{fv}(\exptype{List}{\rwildcard{X}}) = \emptyset$.
+\texttt{List<? extends Object>} becomes
-
+$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$,
-Additionally free variables are not allowed to leave the scope of a capture conversion
+where the existentially bound variable \texttt{A} has a lower bound
-introduced by a let statement.
+$\bot$ and an upper bound $\type{Object}$.
-%TODO we combat both of this with wildcard type placeholders (? flag)
+Before we can call the \texttt{add} method on this type we perform
-
+capture conversion by inserting a let statement:
-Type placeholders which are not flagged as possible free variables ($\wtv{a}$) can never hold a free variable or a type containing free variables.
+\begin{lstlisting}
-Constraint generation places these standard place holders at method return types and parameter types.
+let v : (*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$@*) = lo in v.<A>add(new Integer(1));
-\begin{lstlisting}[style=fgj]
-<X> List<X> clone(List<X> l);
-(*@$\red{\tv{r}}$@*) example((*@$\red{\tv{p}}$@*) p){
-  return clone(p);
-}
 \end{lstlisting}
-This prevents type solutions that contain free variables in parameter and return types.
+The variable \expr{lo} (from Listing~\ref{lst:wildcardIntro}) is
-When calling a method which already has a type annotation we have to consider adding a capture conversion in form of a let statement.
+assigned to a new immutable variable \expr{v} with type
-The constraint $\tv{p} \lessdot \exptype{List}{\wtv{x}}$ signals the \unify{} algorithm that here a capture conversion is possible.
+$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$, 
-$\sigma(\tv{p}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, \sigma(\tv{r}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, $ is a possible solution.
+but inside the let statement the variable \expr{v} will be treated as
-But only when adding a capture conversion:
+$\exptype{List}{\rwildcard{A}}$. 
-\begin{lstlisting}[style=fgj]
+Here $\rwildcard{A}$ is a fresh variable or a captured wildcard.
-<X> List<X> clone(List<X> l);
+The only information we have about $\rwildcard{A}$ is that it is a
-(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){
+supertype of $\bot$ and a subtype of $\type{Object}$
-  return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
+It is important to give the captured wildcard type $\rwildcard{A}$ an unique name which is used nowhere else.
-}
+This approach also clarifies why the method call to \texttt{concat}
+in listing \ref{lst:concatError} is rejected (see Listing~\ref{lst:concatTamedFJ}).
+\begin{figure}[tp]
+\begin{lstlisting}[style=TamedFJ,caption=\TamedFJ{} representation of the concat call from listing \ref{lst:concatError}, label=lst:concatTamedFJ]
+let l1' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l1 in
+    let l2' : (*@$\wctype{\rwildcard{Y}}{List}{\exptype{List}{\rwildcard{Y}}}$@*) = l2 in
+        concat(l1', l2') // Error!
 \end{lstlisting}
+\end{figure}
+
+% % TODO intro to Featherweight Java
+% is a formal model of the Java programming language reduced to a core set of instructions.
+% - We extend this model by existential types and let expressions.
+% - We copy this from \ref{WildFJ} but make type annotations optional
+% - Our calculus is called \TamedFJ{}
+% - \TamedFJ{} binds every method argument with a let statement.
+
+% To enable the use of wildcards in argument types of a method invocation
+% Java uses a process called \textit{Capture Conversion}.
+% This behaviour is emulated by our language \TamedFJ{};
+% a Featherweight Java \cite{FJ} derivative with added wildcard support
+% and a global type inference feature (syntax definition in section \ref{sec:tifj}).
+% %\TamedFJ{} is basically the language described by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection} with optional type annotations.
+% Let's have a look at a representation of the \texttt{add} call from the last line in listing \ref{lst:wildcardIntro} with our calculus \TamedFJ{}:
+% %The \texttt{add} call in listing \ref{lst:wildcardIntro} needs to be encased by a \texttt{let} statement in our calculus.
+% %This makes the capture converion explicit.
+% \begin{lstlisting}
+% let v : (*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$@*) = lo in v.<A>add(new Integer(1));
+% \end{lstlisting}
+% The method call is encased in a \texttt{let} statement and
+% \expr{lo} is assigned to a new variable \expr{v} of \linebreak[2]
+% \textbf{Existential Type} $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$.
+% Our calculus uses existential types \cite{WildFJ} to formalize wildcards:
+% \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}}$.
+% The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound,
+% and a type they are bound to.
+% In this case the name is $\rwildcard{A}$ and it's bound to the the type \texttt{List}.
+% Inside the \texttt{let} statement the variable \expr{v} has the type
+% $\exptype{List}{\rwildcard{A}}$.
+% This is an explicit version of \linebreak[2]
+% \textbf{Capture Conversion},
+% which makes use of the fact that a concrete type must be behind every wildcard type.
+% There is no instantiation of a \texttt{List<?>},
+% but there exists some unknown type $\exptype{List}{\rwildcard{A}}$, with $\rwildcard{A}$ inbetween the bounds $\bot$ (bottom type, subtype of all types) and
+% \texttt{Object}.
+% Inside the body of the let statement \expr{v} is treated as a value with the constant type $\exptype{List}{\rwildcard{A}}$.
+% Existential types enable us to formalize \textit{Capture Conversion}.
+% Polymorphic method calls need to be wrapped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}.
+% In Java this is done implicitly in a process called capture conversion (as proposed in Wild FJ \cite{WildFJ}).
 
-Capture constraints cannot be stored in a set.
-$\wtv{a} \lessdotCC \wtv{b}$ is not the same as $\wtv{a} \lessdotCC \wtv{b}$.
-Both constraints will end up the same after a substitution for both placeholders $\tv{a}$ and $\tv{b}$.
-But afterwards a capture conversion is applied, which can generate different types on the left sides.
-\begin{itemize}
-  \item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Y}}$ 
-  \item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Z}}$ 
-\end{itemize}

martin.bib

@@ -50,6 +50,8 @@ keywords = {subtyping, type inference, principal types}
   SERIES       = {Lecture Notes in Artificial Intelligence}
 }
 
+
+
 @article{DM82,
     author={Luis Damas and Robin Milner},
     title={Principal type-schemes for functional programs},
@@ -66,13 +68,38 @@ keywords = {subtyping, type inference, principal types}
     month=Jan,
     year={1965}}
     
+@article{DBLP:journals/jcss/Milner78, 
+  author    = {Robin Milner},
+  title     = {A Theory of Type Polymorphism in Programming},
+  journal   = {Journal of Computer and Systems Sciences},
+  volume    = {17},
+  number    = {3},
+  pages     = {348--375},
+  year      = {1978},
+  url       = {https://doi.org/10.1016/0022-0000(78)90014-4},
+  doi       = {10.1016/0022-0000(78)90014-4},
+  timestamp = {Tue, 16 Feb 2021 14:04:22 +0100},
+  biburl    = {https://dblp.org/rec/journals/jcss/Milner78.bib},
+  bibsource = {dblp computer science bibliography, https://dblp.org}
+}   
+
 @article{MM82,
-    author={A. Martelli and U. Montanari},
+author = {Martelli, Alberto and Montanari, Ugo},
 title = {An Efficient Unification Algorithm},
-    journal={ACM Transactions on Programming Languages and Systems},
+year = {1982},
+issue_date = {April 1982},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
 volume = {4},
-    pages={258-282},
+number = {2},
-    year={1982}}
+issn = {0164-0925},
+url = {https://doi.org/10.1145/357162.357169},
+doi = {10.1145/357162.357169},
+journal = {ACM Trans. Program. Lang. Syst.},
+month = {apr},
+pages = {258–282},
+numpages = {25}
+}
 
 @InProceedings{Plue07_3,
   author = 	 {Martin Pl{\"u}micke},
@@ -326,6 +353,14 @@ articleno = {138},
 numpages = {22},
 keywords = {Null, Java Wildcards, Existential Types}
 }
+@inproceedings{AT16,
+author = {Amin, Nada and Tate, Ross},
+year = {2016},
+month = {10},
+pages = {838-848},
+title = {Java and scala's type systems are unsound: the existential crisis of null pointers},
+doi = {10.1145/2983990.2984004}
+}
 @InProceedings{TIforFGJ,
   author =	{Stadelmeier, Andreas and Pl\"{u}micke, Martin and Thiemann, Peter},
   title =	{{Global Type Inference for Featherweight Generic Java}},
@@ -352,6 +387,16 @@ keywords = {Null, Java Wildcards, Existential Types}
   publisher={Addison-Wesley Professional}
 }
 
+@Book{GoJoStBrBuSm23,
+  author = {Gosling, James and Joy, Bill and Steele, Guy and Bracha, Gilad and Buckley, Alex and Smith, Daniel},
+  title = "{The Java\textsuperscript{\textregistered} {L}anguage {S}pecification}",
+  Optpublisher = "Addison-Wesley",
+  url = {https://docs.oracle.com/javase/specs/jls/se21/jls21.pdf},
+  edition = {{J}ava {S}{E} 21},
+  year = 2023,
+  OPtseries = {The Java series}
+}
+
 @inproceedings{semanticWildcardModel,
   title={Towards a semantic model for Java wildcards},
   author={Summers, Alexander J and Cameron, Nicholas and Dezani-Ciancaglini, Mariangiola and Drossopoulou, Sophia},
@@ -388,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},
@@ -428,3 +473,99 @@ numpages = {20},
 keywords = {wildcards, union types, type inference, type argument inference, subtyping, polymorphic methods, parameterized types, intersection types, generics, bounded quantification}
 }
 
+@article{FJ,
+author = {Igarashi, Atsushi and Pierce, Benjamin C. and Wadler, Philip},
+title = {Featherweight Java: a minimal core calculus for Java and GJ},
+year = {2001},
+issue_date = {May 2001},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {23},
+number = {3},
+issn = {0164-0925},
+url = {https://doi.org/10.1145/503502.503505},
+doi = {10.1145/503502.503505},
+abstract = {Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy. Featherweight Java bears a similar relation to Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational "feel," providing classes, methods, fields, inheritance, and dynamic typecasts with a semantics closely following Java's. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The minimal syntax, typing rules, and operational semantics of Featherweight Java make it a handy tool for studying the consequences of extensions and variations. As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and give a detailed proof of type safety. The extended system formalizes for the first time some of the key features of GJ.},
+journal = {ACM Trans. Program. Lang. Syst.},
+month = {may},
+pages = {396–450},
+numpages = {55},
+keywords = {Compilation, Java, generic classes, language design, language semantics}
+}
+
+@inproceedings{principalTypes,
+  title={What are principal typings and what are they good for?},
+  author={Jim, Trevor},
+  booktitle={Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
+  pages={42--53},
+  year={1996}
+}
+
+@article{aNormalForm,
+  title={Reasoning about programs in continuation-passing style.},
+  author={Sabry, Amr and Felleisen, Matthias},
+  journal={ACM SIGPLAN Lisp Pointers},
+  number={1},
+  pages={288--298},
+  year={1992},
+  publisher={ACM New York, NY, USA}
+}
+
+@InProceedings{PH23,
+  author = 	 {Martin Pl{\"u}micke  and Daniel Holle},
+  title = 	 {Principal generics in {J}ava--{T}{X}},
+  crossref = {kps2023},
+  pages = 	 {122--143},
+  year = 	 {2023},
+  Opteditor = 	 {Thomas Noll and Ira Fesefeldt},
+  address = 	 {Aachen},
+  Optnumber = 	 {AIB-2023-03},
+  month = 	 {September},
+  series = {Aachener Informatik-Berichte (AIB)},
+  url = {https://publications.rwth-aachen.de/record/972197/files/972197.pdf#%5B%7B%22num%22%3A281%2C%22gen%22%3A0%7D%2C%7B%22name%22%3A%22XYZ%22%7D%2C89.292%2C740.862%2Cnull%5D},
+  Optdoi = {10.18154/RWTH-2023-10034},
+  Optnote = {(to appear)}
+}
+
+@Proceedings{kps2023,
+  booktitle = 	 {22. Kolloquium Programmiersprachen und Grundlagen der Programmierung},
+  year = 	 {2023},
+  editor = 	 {Noll, Thomas and Fesefeldt, Ira Justus},
+  number = 	 {AIB-2023-03},
+  series = 	 {Technical report / Department of Computer Science. - Informatik},
+  month = 	 {September},
+  organization = {RWTH Aachenen},
+  doi = {10.18154/RWTH-2023-10034}
+}
+
+@InProceedings{plue24_1,
+  author = 	 {Martin Pl{\"u}micke},
+  title = 	 {Avoiding the Capture Conversion in {J}ava--{T}{X}},
+  crossref =  {HKPTW24},
+  pages = 	 {109--115},
+  year = 	 {2023}
+}
+
+@proceedings{HKPTW24,
+  author = 	 {Daniel Holle and Jens Knoop and Martin Pl\"umicke and Peter Thiemann and Baltasar Tranc\'{o}n y Widemann},
+  booktitle = 	 {Proceedings of the 38th and 39th Annual Meeting of the GI Working Group Programming Languages and
+Computing Concepts},
+  institution =  {DHBW Stuttgart},
+  year = 	 {2024},
+  series = 	 {INSIGHTS -- Schriftenreihe der Fakult\"at Technik},
+  number = 	 {01/2024},
+  ISSN =         {2193-9098},
+  url =          {https://www.dhbw-stuttgart.de/forschung-transfer/technik/schriftenreihe-insights}
+}
+
+@article{wells1999typability,
+  title={Typability and type checking in System F are equivalent and undecidable},
+  author={Wells, Joe B},
+  journal={Annals of Pure and Applied Logic},
+  volume={98},
+  number={1-3},
+  pages={111--156},
+  year={1999},
+  publisher={Elsevier}
+}
+

prolog.tex

@@ -1,5 +1,6 @@
 \usepackage{xspace}
 \usepackage{color,ulem}
+\usepackage{mathpartir}
 \usepackage{listings}
 \lstset{language=Java,
   showspaces=false,
@@ -11,14 +12,24 @@
   escapeinside={(*@}{@*)},
   captionpos=t,float,abovecaptionskip=-\medskipamount
 }
+
 \lstdefinestyle{fgj}{backgroundcolor=\color{lime!20}}
 \lstdefinestyle{tfgj}{backgroundcolor=\color{lightgray!20}}
-\lstdefinestyle{letfj}{backgroundcolor=\color{lightgray!20}}
+\lstdefinestyle{letfj}{backgroundcolor=\color{lime!20}}
+\lstdefinestyle{tamedfj}{backgroundcolor=\color{yellow!20}}
+\lstdefinestyle{java}{backgroundcolor=\color{lightgray!20}}
+\lstdefinestyle{constraints}{
+  basicstyle=\normalfont,
+  backgroundcolor=\color{red!20}
+}
 
 \newtheorem{recap}[note]{Recap}
 
+\newcommand{\rulenameAfter}[1]{\begin{array}[b]{l}\rulename{#1}\\[-1em] \ \end{array}}
+
 \newcommand{\tifj}{\texttt{TamedFJ}}
 
+\newcommand{\wcSep}{\vdash}
 \newcommand\mv[1]{{\tt #1}}
 \newcommand{\ol}[1]{\overline{\tt #1}}
 \newcommand{\exptype}[2]{\mathtt{#1 \texttt{<} #2 \texttt{>} }}
@@ -68,6 +79,9 @@
 \newcommand\subeq{\mathbin{\texttt{<:}}}
 \newcommand\extends{\ensuremath{\triangleleft}}
 
+\newcommand{\QMextends}[1]{\textrm{\normalshape\ttfamily ?\,extends}\linebreak[0]\,#1}
+\newcommand{\QMsuper}[1]{\textrm{\normalshape\ttfamily ?\linebreak[0]\,su\-per}\linebreak[0]\,#1}
+
 \newcommand\rulename[1]{\textup{\textsc{(#1)}}}
 \newcommand{\generalizeRule}{General}
 
@@ -94,7 +108,8 @@
 \newcommand{\constraints}{\ensuremath{\mathit{\overline{c}}}}
 \newcommand{\itype}[1]{\ensuremath{\mathit{#1}}}
 \newcommand{\il}[1]{\ensuremath{\overline{\itype{#1}}}}
-\newcommand{\type}[1]{\mathtt{#1}}
+\newcommand{\gtype}[1]{\type{#1}}
+\newcommand{\type}[1]{\ensuremath{\mathtt{#1}}}
 \newcommand{\anyType}[1]{\mathit{#1}}
 \newcommand{\gType}[1]{\texttt{#1}}
 \newcommand{\mtypeEnvironment}{\ensuremath{\Pi}}
@@ -102,9 +117,11 @@
 \newcommand{\localVarAssumption}{\ensuremath{\mathtt{\eta}}}
 \newcommand{\expandLB}{\textit{expandLB}}
 
-\newcommand{\letfj}{\emph{LetFJ}}
+\newcommand{\letfj}{\textbf{LetFJ}}
 \newcommand{\tph}{\text{tph}}
 
+\newcommand{\expr}[1]{\texttt{#1}}
+
 \def\exptypett#1#2{\texttt{#1}\textrm{{\tt <#2}}\textrm{{\tt >}}\xspace}
 \def\exp#1#2{#1(\,#2\,)\xspace}
 \newcommand{\ldo}{, \ldots , }
@@ -116,8 +133,9 @@
 \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{\cctv}[1]{\ensuremath{\tv{#1}_!}}
-\newcommand{\ntv}[1]{\tv{#1}}
+\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
+%\newcommand{\ntv}[1]{\tv{#1}}
 \newcommand{\wcstore}{\ensuremath{\Delta}}
 
 %\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}_?}}
@@ -139,7 +157,6 @@
 \newcommand{\ruleSubstWC}[0]{\rulename{Subst-WC}}
 \newcommand{\subclass}{\mathtt{\sqsubset}\mkern-5mu :}
 
-\newcommand{\TameFJ}{\text{TameFJ}}
 \newcommand{\TamedFJ}{\textbf{TamedFJ}}
 \newcommand{\TYPE}{\textbf{TYPE}}
 

rebuttal.md

@@ -0,0 +1,11 @@
+Thank you very much for your in depth reviews. We submitted the paper in an early stage to get early feedback and we'd appreciate the chance to submit a revised version. We are already working on the shortcomings you exposed in your reviews.
+
+A prototype implementation of the type inference algorithm is currently in development. We expect to use the prototype to explore the boundaries of what the algorithm is capable of. In the next revision of the paper we will report positive and negative examples as well as measurements of the algorithm's runtime.
+
+We plan to address the following points before submitting the revision:
+* Implementation of the algorithm and a showcase of working use cases.
+* Reworked and detailed soundness proof.
+* Provide better explanations and examples on constraint generation.
+* Fix typos, errors, ambiguous explanations, etc..
+* Discussion of the algorithm's complexity, our minimal aim is NP-Hardness, but we will try to draw comparisons to similar algorithms like the ones from Plümicke or Stadelmeier already mentioned in the paper.
+* A discussion on completeness and why a complete type inference algorithm for Java is not possible.

relatedwork.tex

@@ -0,0 +1,76 @@
+
+\section{Related Work}
+Igarashi et al \cite{FJ} define Featherweight Java
+and its generic sibling, Featherweight Generic Java. Their language is
+a functional calculus reduced to the bare essentials, they develop the full metatheory, they
+support generics, and study the type erasing transformation used by
+the Java compiler. Stadelmeier et. al. extends this approach by global type
+inference \cite{TIforFGJ}.
+
+\subsection{Wildcards in formal Java models}
+Wildcards are first described in a research paper in \cite{addingWildcardsToJava}. In
+\cite{TEP05} the Featherweight Java-Calculus \textsf{Wild~ FJ} is introduced. It
+contains a formal description of wildcards. The Java Language Specification
+\cite{GoJoStBrBuSm23}  refers to \textsf{Wild~FJ} for the introduction of
+wildcards. In \cite{aModelForJavaWithWildcards} a formal model based of explicite existential types
+is introduced and proven as sound. Additionally, for a subset of Java a
+translation to the formal model is given, such that this subset is proven as
+sound. In \cite{WildcardsNeedWitnessProtection} another core calculus is
+introduced, which is proven as 
+sound, too. In this paper it is shown that the unsoundness of Java which is
+discovered in \cite{AT16} is avoidable, even in the absence of nullness-aware type
+system. In \cite{TamingWildcards} finally a framework is presented which combines
+use-site variance (wildcards as in Java) and definition-site variance (as in Scala). For
+instance, it can be used to add use-site variance to Scala and extend the Java
+type system to infer the definition-site variance.
+
+Our calculus is mixture ...
+
+\subsection{Type inference}
+Some object-oriented languages like Scala, C\#, and Java perform
+\emph{local} type inference \cite{PT98,OZZ01}. Local type
+inference means that missing type annotations are recovered using only
+information from adjacent nodes in the syntax tree without long distance
+constraints. For instance, the type of a variable initialized with a
+non-functional expression or the return type of a method can be
+inferred. However, method argument types, in particular for recursive
+methods, cannot be inferred by local type inference.
+
+Milner's algorithm $\mathcal{W}$ \cite{DBLP:journals/jcss/Milner78} is
+the gold standard for global type inference for languages with
+parametric polymorphism, which is used by ML-style languages. The fundamental idea
+of the algorithm is to enforce type equality by many-sorted type
+unification \cite{Rob65,MM82}. This approach is effective and results
+in so-called principal types because many-sorted unification is
+unitary, which means that there is at most one most general result.
+
+Pl\"umicke \cite{Plue07_3} presents a first attempt to adopt Milner's
+approach to Java. However, the presence of subtyping means that type
+unification is no longer unitary, but still finitary. Thus, there is
+no longer a single most general type, but any type is an instance of a
+finite set of maximal types (for more details see Section
+\ref{sec:unification}). Further work by the same author
+\cite{plue15_2,plue17_2},
+refines this approach by moving to a constraint-based algorithm and by
+considering lambda expressions and Scale-like function types.
+
+Pluemicke has a different approach to introduce wildcards in \cite{plue09_1}. He
+allows wildcards as any subsitution for type variables and disclaim the
+capture conversion. Instead he extended
+the subtyping ordering such that for $\theta \sub \theta' \sub \theta''$ holds
+indeed the transitiv closure of $\QMextends{\theta} \sub \theta'$ and $\theta' \sub
+\QMsuper{\theta''}$ but not the reflexive closure. He gave a type unification
+algorithm for this type system, which he proved as sound and complete. 
+
+The problem of his type system is in the lossing reflexivity as shown in
+example \ref{lst:intro-example-typeless}. First approaches to solve this problem he gave in
+\cite{plue24_1}, where he fixes that no pairwise different nodes in the
+abstract syntax gets the same type variable and that no pairwise different type
+variables are equalized. In \cite{PH23} he showed how his type inference
+algorithm suffices theese properties.
+
+% In Pl\"umicke's work there is indeed a formal definition of the subtying
+% ordering and a correctness proof of the type unification algorithms but no
+% soundness proof of the type system, itself. Therefore we choose for our type
+% inference algorithms with wildcars the approach of ???????
+

soundness.tex

@@ -1,238 +1,217 @@
 \section{Soundness}
 
-\newcommand{\CC}{\text{CC}}
+The differenciation of wildcard placeholders and normal type placeholders is vital for the soundness proof.
+During a let statement the environment $\Delta$ is extended by capture converted wildcards,
+but only for the scope of the body of the let statement.
+The capture converted wildcards must not be used outside of the let statement.
+This is ensured by two things:
+The first is lemma \ref{lemma:freeVariablesOnlyTravelOneHop} which ensures that free variables only
+travel one hop at the time through a constraint set.
+And the second one is the fact that normal type placeholders never contain free variables.
 
-\begin{lemma}
+\unify{} calculates solutions for all normal type placeholders.
-A sound TypelessFJ program is also sound under LetFJ type rules.
+Those are used for all untyped method's argument and return type.
-\begin{description}
+A correct typing for method calls can be deducted from those type informations.
-    \item[if:]
-$\Gamma | \Delta \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \ \text{in}\ C \text{with} \ \generics{\ol{Y \triangleleft P}}$
-\end{description}
-\end{lemma}
 
-TODO: Beforehand we have to show that $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
+\begin{lemma}{Soundness:}\label{lemma:soundness}
-Here $\Delta$ does not contain every $\overline{\Delta}$ ever created.
-%what prevents a free variable to emerge in \Delta.N example Y^Object |- C<String> <: X^Y.C<X>
-% if the Y is later needed for an equals: same(id(x), x2)
-Free wildcards do not move inwards. We can show that every new type is either well-formed and therefore does not contain any free variables.
-Or it is a generic method call: is it possible to use any free wildcards here?
-let empty 
-
-<X> Box<X> empty()
-same(Box<?>, empty())
-let p1 : X.Box<X> = Box<?> in let 
-X.Box<X> <. Box<x> 
-Box<e> <. Box<x>
-
-boxin(empty()), Box2<?>
-
-Where can a problem arise? When we use free wildcards before they are freed.
-But we can always CC them first. Exception two types: X.Pair<X, y> and Y.Pair<x, Y>
-Here y = Y and x = X but 
-
-<X,Y> void same(Pair<X,Y> a, Pair<X,Y> b){}
-<X> Pair<?, X> left() { return null; }
-<X> Pair<X, ?> right() { return null; }
-
-<X> Box<X> id(Box<? extends Box<X>> x)
-here it could be beneficial to use a free wildcard as the parameter X to have it later
-Box<?> x = ...
-same(id(x), id(x)) <- this will be accepted by TI
-
-let left : X,Y.Pair<X,Y> = left() in
- let right : Pair<X,Y> = right() in
-
-Compromise:
-- Generate constraints so that they comply with LetFJ
-- Propose a version which is close to Java
-
-Version for LetFJ:
-Is it still possible to do the capture conversion in form of constraints?
-X.C<X> <. C<x>
-T <. X.C<X>
-how to proof: X.C<X> ok
-
-
-If $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
-then there exists a $|\texttt{e}|$ with $\Delta | \Theta \vdash |\texttt{e}| : \wcNtype{\Delta'}{N}$ in LetFJ.
-This is possible by starting with the parameter types as the base case $\overline{\Delta} = \emptyset$.
-
-
-Each type $\wcNtype{\Delta'}{N}$ can only use wildcards already freed.
-
-\textit{Proof} by structural induction.
-\begin{description}
-    \item[$\texttt{e} = \texttt{x}$] $\Delta | \Theta \vdash \texttt{e} : \type{T} \mid \emptyset$
-    $\Delta \vdash \type{T} \ \ok$ by \rulename{T-Method}
-    and therefore $\Delta | \Theta \vdash \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$.
-
-$|\texttt{x}, \texttt{e}| = \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$
-
-\item[$\texttt{e} = \texttt{e}.\texttt{m}(\ol{e})$] there must be atleast one value in $\texttt{e}$ or $\ol{e}$
-\item[$\texttt{e}.f$] given let x : T = e' in x 
-let x : T = e' in let xf = x.f in xf
-
-Required:
-$ \Delta | \Theta \vdash e' : \type{T}_1$
-$\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$
-$\Delta, \Delta' | \Theta, x : \type{N} \vdash let xf = x.f in xf : \type{T}_2$
-
-\end{description}
-
-
-\textbf{Proof:} Every program complying with our type rules can be converted to a correct LetFJ program.
-First we convert the program so that every wildcards used in an expression are in the $\Delta$ environment:
-m(p) = e => let xp = p in [xp/p]e
-x1.m(x2) => let xm = x1.m(x2=) in xm
-x.f => let xf = x.f in xf
-Then we have to proof there is never a wildcard used before it is declared.
-Wildcards are introduced by the capture conversions and nothing else.
-
-
-\begin{theorem}\label{testenv-theorem}
-Type inference produces a correctly typed program.
-\begin{description}
-    \item[If] $\fjtypeinference(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
-    \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \mtypeEnvironment{}'$
-    \item[Then] $\texttt{class}\ \exptype{C}{\ol{X}
-    \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \} \text{ok}$,
-    with $\ol{M} = $
-\end{description}
-\end{theorem}
-
-\begin{lemma}{Well-formedness:}
-TODO: 
-\end{lemma}
-
-\begin{lemma}{Soundness:}
     \unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
     \begin{description}
-    \item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = C$
+    \item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = (\Delta', C)$
-    and $(\Delta_u, \sigma) = \unify{}(\Delta', C)$ and let $\Delta = \Delta_u \cup \Delta'$
+    \item[then] $\Delta|\Gamma  \vdash \texttt{e} : \sigma(\tv{a})$ where $\Delta = \Delta_u \cup \Delta'$
-%    , with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } }$
-%    and $\vdash \ol{L} : \mtypeEnvironment{}$
-%    and $\Gamma \subseteq \mtypeEnvironment{}$
-%    \item[given] a $(\Delta, \sigma)$ with $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
-%    and there exists a $\Delta'$ with $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T'})}$
-    \item[then] there is a completion $|\texttt{e}|$ with $\Delta|\Gamma  \vdash |\texttt{e}| : \sigma(\tv{a})$
     \end{description}
 \end{lemma}
-Regular type placeholders represent type annotations.
-These are the only types a \wildFJ{} program needs to be correctly typed.
-The type placeholders flagged as wildcard placeholders are intermediate types
-used in let statements and as type parameters for generic method calls.
-
-%Unify needs to return S aswell and guarantee that the \Delta' environment are the wildcards
-% only used inside the constraint the wildcard variable occurs
-% should Unify also return the \Delta' environment? Otherwise the bounds of free wildcard variables are lost
-
-% Or is it possible to deduct the right \ol{S} directly from the types in the normal TPHs?
-
 \textit{Proof:}
 By structural induction over the expression $\texttt{e}$. 
 \begin{description}
-    \item[$\texttt{e}.\texttt{f}$] Let $\sigma(\tv{r}) = \wcNtype{\Delta_c}{N}$,
+    \item[$\texttt{let}\ \texttt{x} = \texttt{t}_1 \ \texttt{in}\ \expr{t}_2$]
-    then $\Delta|\Gamma  \vdash \texttt{e} : \wcNtype{\Delta_c}{N}$ by assumption.
+    $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ by lemma \ref{lemma:wildcardWellFormedness}.
-    $\Delta', \Delta, \Delta_c \vdash \type{N} <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise.
+    $\Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok$ by lemma \ref{lemma:unifyWellFormedness}.
-    %Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$.
+        $\Delta|\Gamma \vdash \expr{t}_1: \sigma(\tv{e}_1)$ by assumption.
-    %Let $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) = \wcNtype{\Delta_t}{N_t}$.
+        $\Delta \vdash \sigma(\tv{e}_1) <: \wcNtype{\Delta'}{N}$ by constraint $\tv{e}_1 \lessdot \tv{x}$ and lemma \ref{lemma:unifySoundness}.
+        The body of the let statement will only use the free variables provided by $\Delta$ and $\Delta'$.
+        We can prove this by lemma \ref{lemma:tvsNoFV} and the fact that the wildcard placeholders used generated the body of the let statement are not used outside of it.
+        Therefore we can say $\Delta,\Delta' | \Gamma, \expr{x}:\type{N} \vdash \expr{t}_2 : \sigma(\tv{e}_2)$ by assumption
+        and $\Delta, \Delta' \vdash  \sigma(\tv{e}_2) <: \sigma(\tv{a})$ by lemma \ref{lemma:unifySoundness}
+        given the constraint $\tv{e}_2 \lessdot \tv{a}$.
+    \item[$\texttt{let}\ \texttt{x} = \texttt{t}_1 \ \texttt{in}\ \expr{x}.\texttt{f}$]
+The let statement in the input is untyped and we have to create a let statement
+$\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{t}_1 \ \texttt{in}\ \expr{x}.\texttt{f}$
+that suffices the T-Let and T-Field type rules.
+The case where no capture conversion is needed, because $\Delta' = \emptyset$, is trivial. Here the Let statement can be skipped entirely.
+We investigate the case $\sigma(\tv{x}) = \wcNtype{\Delta}{N}$.
+%Constraints t1 <. x, x <. C<a>, T <. t2
+Let $\type{T}_1 = \wcNtype{\Delta'}{N} = \sigma(\tv{x})$, $\sigma(\tv{t_1}) = \type{T}_1$,
+$\sigma(\tv{a}) = \type{T}_2$ then
+\begin{itemize}
+\item $\Delta | \Gamma \vdash t_1 : \type{T}_1$ by assumption
+\item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ by constraint $\tv{t_1} \lessdot \tv{x}$ and lemma \ref{lemma:unifySoundness}
+\item $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_2$
+First we can say $\Delta | \Gamma \vdash \expr{x} : \type{N}$ by T-Var.
+%$\Delta, \Delta', \overline{\Delta} \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
+%and lemma \ref{lemma:unifySoundness}.
+%The environment $\overline{\Delta}$ is not needed, because of lemma \ref{lemma:freeVariablesOnlyTravelOneHop}:
+%$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$
+%by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
+%and lemmas \ref{lemma:unifySoundness} and \ref{lemma:freeVariablesOnlyTravelOneHop}.
+By lemma \ref{lemma:unifyWellFormedness} and WF-Var we can deduct
+$\text{fv}(\wcNtype{\Delta'}{N}) \subseteq \Delta$ 
+and by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
+and lemmas \ref{lemma:unifySoundness} and \ref{lemma:freeVariablesOnlyTravelOneHop}
+we can finally say 
+$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$.
+With the constraint $\tv{a} \doteq [\ol{\wtv{a}}/\ol{X}]\type{T}$
+and $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) \in \text{fields}(\sigma(\exptype{C}{\ol{\wtv{a}}}))$ by F-Class
+we proof $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_2$.
+\item $\Delta, \Delta' \vdash \type{T}_2 <: \type{T}$ by constraint %TODO: Rename constraints
+\end{itemize}
 
-    The completion of $|\texttt{e}.\texttt{f}|$ is $\texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f}$
+%generated constraints: t1 <. x, x <. N, T <. t2
+        We are allowed to use capture conversion for $\expr{v}$ here.
+        $\Delta \vdash \expr{v} : \sigma(\tv{a})$ by assumption.
+        $\Delta \vdash \sigma(\tv{a}) <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ and
+        $\Delta \vdash \type{U}_i <: \sigma(\tv{a})$,
+    because of the constraints $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$, $\tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$ and lemma \ref{lemma:unifySoundness}.
+    $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$.
 
-    We now show
+\item[$\text{let}\ \expr{x} = \expr{e} \ \text{in}\ 
-    $\Delta|\Gamma \vdash \texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f} : \sigma(a)$
+\text{let}\ \overline{\expr{x} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x})$]
-    by the T-Field rule.
+generates constraints $\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}},
-    $\Delta \vdash \wcNtype{\Delta_c}{N} <: \wcNtype{\Delta_c}{N}$ by S-Refl.
+\tv{r} \lessdot \tv{a}, \ol{\tv{x}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{r}, \ol{\wtv{b}} \lessdot \ol{N}$.
-    $\Delta, \Delta_c \vdash \type{U}_i <: \sigma(\tv{a})$,
+%We need to proof $\text{let}\ \expr{x} : \wcNtype{\Delta'}{N} = \expr{e}, \,
-    because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$ and lemma \ref{lemma:unifySoundness}.
+%\overline{\expr{x} : \wcNtype{\Delta'}{N} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x}) : \type{T}_2$
-    $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$
+%where $\sigma(\tv{x}) = \wcNtype{\Delta'}{N}$, $\sigma(\ol{\tv{x}}) = \ol{\wcNtype{\Delta'}{N}}$,  $\sigma(\tv{a}) = \type{T}_2$.
-    and $\text{fv}(\type{U}_i) \subseteq \text{fv}(\type{N})$ by definition of $\textit{fields}$.
+We omit the case where a capture conversion is not needed and
+assume $\sigma(\tv{x}) = \wcNtype{\Delta'}{N}$, $\sigma(\ol{\tv{x}}) = \ol{\wcNtype{\Delta'}{N}}$.
+We have to show T-Let and T-Call which leaves us with:
+\begin{itemize}
+    \item $\Delta | \Gamma \vdash \expr{e} : \sigma(\tv{e})$ and $\Delta | \Gamma \vdash \overline{\expr{e} : \sigma(\tv{e})}$ by assumption
+    \item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ and $\Delta \vdash \overline{\type{T}_1 <: \wcNtype{\Delta'}{N}}$ by constraints $\tv{e} \lessdot \tv{x}$, $\overline{\tv{e} \lessdot \tv{x}}$ and lemma \ref{lemma:unifySoundness}
+    \item $\Delta, \Delta', \overline{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash \expr{x}.\texttt{m}(\ol{x}) : \sigma(\tv{r})$ by T-Call and lemma \ref{lemma:freeVariableScope}, because the following promises are satisfied.
+    Note: The lemma \ref{lemma:freeVariableScope} and the fact that the wildcard placeholders $\overline{\wtv{b}}$ are
+    solely used here guarantees that no other than the variables declared in $\Delta, \Delta', \overline{\Delta}$ appear in $\sigma'(\overline{\wtv{b}})$.
+    \begin{itemize}
+        \item $\generics{\ol{X} \triangleleft \ol{U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m})$ is given, otherwise the program fails at the constraint generation step.
+        \item $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$ by constraints $\ol{\wtv{b}} \lessdot [\ol{\wtv{b}}/\ol{X}]\ol{N}$ and lemma \ref{lemma:unifySoundness}
+        there must be some $\ol{S}$ satisfying this premise.
         
-    $\text{dom}(\Delta_c) \subseteq \text{fv}{\type{N}}$ by lemma \ref{lemma:tvsNoFV}.
+        % what about we apply Unify again. With the known types. TODO: proof that unify can be applied again, with the capture converted versions of the constraints
+        %TODO: does not work because left side is a wildcard variable (maybe just change lemma soundness a bit)
+        \item 
+    \end{itemize}
+\end{itemize}
+    \item[$\texttt{v}.\texttt{m}(\ol{v})$]
+    Proof is analog to field access, except the $\Delta \vdash \ol{S}\ \ok$ premise.
+    We know that $\unify{}(\Delta, [\overline{\wtv{b}}/\ol{Y}]\set{
+        \ol{\tv{e}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a}, 
+        \ol{Y} \lessdot \ol{N} } \cup C) = (\Delta', \sigma)$
+        and if we assume $\sigma(\ol{\tv{e}}) = \ol{\wcNtype{\Delta}{N'}}$
+        then the call to $\unify{}(\Delta \cup \overline{\Delta}, [\overline{\ntv{b}}/\ol{Y}]\set{
+            \ol{N'} \lessdot \ol{T}, \type{T} \lessdot \tv{a}, 
+            \ol{Y} \lessdot \ol{N} } \cup C)$ succeeds with $\overline{\ntv{b}}$ being normal placeholders this time,
+            which proofs $\Delta \vdash \ol{S}\ \ok$ via lemma \ref{lemma:unifyWellFormedness}.
+            %TODO: why does this call succeed?
+% Lets have a look at the case where the receiver and parameter types are all named types.
+% So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta_u}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta_u}{N}$
+% and a $\Delta'$, $\overline{\Delta}$ where $\Delta' \subseteq \Delta_u$, $\overline{\Delta \subseteq \Delta_u}$
+% and $\text{dom}(\Delta') = (\text{fv}(\type{N})/\Delta)$, $\overline{\text{dom}(\Delta) = (\text{fv}(\type{N})/\Delta)}$  in
 
-    % X.List<X> <. List<a?>
+% $\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{e} \ \texttt{in}\ 
-    % $\sigma(\ol{\tv{r}}) = \overline{\wcNtype{\Delta}{N}}$,
+% \texttt{let}\ \ol{x} : \overline{\wcNtype{\Delta'}{N}} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x})$
-    % $\ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
-    % TODO: S ok? We could proof $\Delta, \Delta' \overline{\Delta} \vdash \ol{S} \ \ok$
-    % by proofing every substitution in Unify is ok aslong as every type in the inputs is ok
-    % S ok when all variables are in the environment and every L <: U and U <: Class-bound
-    % This can be given by the constraints generated. We can proof if T ok and S <: T and T <: S' then S ok and S' ok
 
-    % If S ok and T <. S , then Unify generates a T ok
+% %TODO: show that this type exists \wcNtype{\Delta'}{N} (a \Delta' which only contains free variables of the type N)
-    S typeinference:
+% % and which is a supertype of T_r (so no free variables in T_r)
-    T <: [S/Y]U
+% % Solution: Make this a lemma and guarantee that Unify does only create types Delta.T with \Delta subset fv(T)
-    We apply the following lemma
+% % This is possible because free variables (except those in \Delta_in) are never used in wildcard environments
-    Lemma
-    if T ok and T <: S then S ok
 
-    until
+% %By lemma \ref{lemma:unifyWeakening}
-    T = [S/Y]U
+% We know that 
+% $\unify{}(\Delta, [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{ \overline{\wcNtype{\Delta}{N}} \lessdotCC \ol{T}, \wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}})$
+% has a solution.
+% Also $\overline{\wcNtype{\Delta}{N}} \lessdot \ol{T}$ and $\wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}$ will be converted to 
+% $\ol{N} \lessdot \ol{T}$ and $\type{N} \lessdot \exptype{C}{\ol{X}}$ by the \rulename{Capture} rule.
+% Which then results in the same as calling $\unify{}((\Delta, \Delta', \overline{\Delta}), [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{\ol{N} \lessdot \ol{T}, \type{N} \lessdot \exptype{C}{\ol{X}}})$,
+% which shows $\Delta, \Delta', \overline{\Delta} \vdash \overline{N} <: [\ol{S}/\ol{X}]\overline{U}$.
 
-    and then we can say by 
+%     This implies $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ and $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
-    Lemma:
+%     $\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T}$,
-    If [S/Y]U ok then S ok (TODO: proof!)
+%     $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
+%     and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$
+%     are guaranteed by the generated constraints and lemma \ref{lemma:unifySoundness}.% and \ref{lemma:unifyCC}.
+%     $\Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}$ due to $\ol{T} = \ol{\wcNtype{\Delta}{N}}$ and S-Refl. $\Delta, \Delta' \vdash \type{T}_r <: \wcNtype{\Delta'}{N}$ accordingly.
+%     $\Delta|\Gamma \vdash \texttt{t}_r : \type{T}_r$ and $\Delta|\Gamma \vdash \ol{t} : \ol{T}_r$ by assumption.
+%     $\Delta, \Delta' \vdash \ol{\wcNtype{\Delta}{N}} \ \ok$ by lemma \ref{lemma:unifyWellFormedness},
+%     therefore $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} \ \ok$, which implies $\Delta, \Delta', \overline{\Delta} \vdash \ol{U} \ \ok$
+%     %by lemma \ref{lemma:wfHereditary}
+%     and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok $ by premise of WF-Class.
+%     The same goes for $\wcNtype{\Delta'}{N}$.
 
-    So we do not have to proof S ok (but T)
+%     % \begin{gather}
+% %         \label{sp:0}
+% %         \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T} \\
+% %         \label{sp:1}
+% %         \Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U} \\
+% %         \label{sp:2}
+% %         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \\
+% %         \label{sp:3}
+% %         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\
+% %         \label{sp:4}
+% %         \Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
+% %     \end{gather}
 
-    % T_r <: C<T> (S is in T)
+% Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$).
-    % Is C<T> ok?
-    % if every type environment \Delta supplied to Unify is ok (L <: U), then \sigma(a) = \Delta'.N implies \Delta' conforms to (L <: U)
-    % this together with the X <. N constraints proofs T_r ok
-
-    $\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO
-    %Easy, because unify only generates substitutions for normal type placeholders which are OK
-
-    \item[$\texttt{e}.\texttt{m}(\ol{e})$]
-Lets have a look at the case where the receiver and parameter types are all named types.
-So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta_u}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta_u}{N}$
-and a $\Delta'$, $\overline{\Delta}$ where $\Delta' \subseteq \Delta_u$, $\overline{\Delta \subseteq \Delta_u}$
-and $\text{dom}(\Delta') = (\text{fv}(\type{N})/\Delta)$, $\overline{\text{dom}(\Delta) = (\text{fv}(\type{N})/\Delta)}$  in
-
-$\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{e} \ \texttt{in}\ 
-\texttt{let}\ \ol{x} : \overline{\wcNtype{\Delta'}{N}} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x})$
-
-%TODO: show that this type exists \wcNtype{\Delta'}{N} (a \Delta' which only contains free variables of the type N)
-% and which is a supertype of T_r (so no free variables in T_r)
-% Solution: Make this a lemma and guarantee that Unify does only create types Delta.T with \Delta subset fv(T)
-% This is possible because free variables (except those in \Delta_in) are never used in wildcard environments
-
-By lemma \ref{lemma:unifyWeakening} we know that 
-$\unify{}(\Delta, [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{ \overline{\wcNtype{\Delta}{N}} \lessdotCC \ol{T}, \wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}})$
-has a solution.
-Also $\overline{\wcNtype{\Delta}{N}} \lessdot \ol{T}$ and $\wcNtype{\Delta'}{N} \lessdotCC \exptype{C}{\ol{X}}$ will be converted to 
-$\ol{N} \lessdot \ol{T}$ and $\type{N} \lessdot \exptype{C}{\ol{X}}$ by the \rulename{Capture} rule.
-Which then results in the same as calling $\unify{}((\Delta, \Delta', \overline{\Delta}), [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{\ol{N} \lessdot \ol{T}, \type{N} \lessdot \exptype{C}{\ol{X}}})$,
-which shows $\Delta, \Delta', \overline{\Delta} \vdash \overline{N} <: [\ol{S}/\ol{X}]\overline{U}$.
-
-    This implies $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ and $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
-    $\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T}$,
-    $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
-    and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$
-    are guaranteed by the generated constraints and lemma \ref{lemma:unifySoundness} and \ref{lemma:unifyCC}.
-    $\Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}$ due to $\ol{T} = \ol{\wcNtype{\Delta}{N}}$ and S-Refl. $\Delta, \Delta' \vdash \type{T}_r <: \wcNtype{\Delta'}{N}$ accordingly.
-    $\Delta|\Gamma \vdash \texttt{t}_r : \type{T}_r$ and $\Delta|\Gamma \vdash \ol{t} : \ol{T}_r$ by assumption.
-    $\Delta, \Delta' \vdash \ol{\wcNtype{\Delta}{N}} \ \ok$ by lemma \ref{lemma:unifyWellFormedness},
-    therefore $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} \ \ok$, which implies $\Delta, \Delta', \overline{\Delta} \vdash \ol{U} \ \ok$
-    by lemma \ref{lemma:wfHereditary} and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok $ by premise of WF-Class.
-    The same goes for $\wcNtype{\Delta'}{N}$.
-
-    % \begin{gather}
-%         \label{sp:0}
-%         \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T} \\
-%         \label{sp:1}
-%         \Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U} \\
-%         \label{sp:2}
-%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \\
-%         \label{sp:3}
-%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\
-%         \label{sp:4}
-%         \Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
-%     \end{gather}
-
-Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$).
 
 \end{description}
 
+
+During the unification process free variables can only move one hop at a time.
+Free variables originate from capture constraints.
+By applying the capture rule to a constraint of the form $\wcNtype{\Delta}{N} \lessdotCC \type{T}$ the variables declared in $\Delta$
+are now free in the constraint $\type{N} \lessdot \type{T}$.
+The other way of free variables traveling into a constraint is by substitution.
+This is only possible if a constraint contains wildcard placeholders.
+And only free variables which reside in the same constraint as a wildcard placeholders have the possibility of being set in.
+
+This effect is transitive. Free variables travel from constraint to constraint.
+If there is no connection of constraints containing wildcard type placeholders between a free variable and a constraint,
+then free variables cannot travel there.
+
+\begin{lemma}
+    Free variables travel only 
+\end{lemma}
+
+\begin{lemma}{Free variables}\label{lemma:freeVariableScope}
+    Free variables never leave their scope.
+    If a set of constraints does not share a single wildcard type placeholder with the rest of the constraint set,
+    then it will never contain free variables used outside of it.
+$(\Delta, \sigma) = \unify{}(\Delta_{in}, C \cup C')$
+
+and $\text{wtv}(C') \cap \text{wtv}(C) = \emptyset$
+and $\overline{\sigma(\tv{x}) = \wcNtype{\Delta}{N}}$
+
+then $\Delta, \Delta', \overline{\Delta}$ are all the variables used in $C'$.
+\end{lemma}
+\textit{Proof:} This is due to free variables only travel inbetween constraints and themselves via substitution.
+
+If $\type{S} \lessdotCC \type{T}$ spawns free variables, they will be contained within the reach of the wildcard type placeholders
+used for the method call.
+No other free variables can move into that scope.
+With this lemma we can further proof that during a method call only the generated free variables are used.
+
+% \begin{lemma}
+%     Free variables never leave their scope.
+%     $C' = \set{
+%         \overline{\tv{e} \lessdot \tv{x}}, \overline{\tv{x} \lessdotCC \tv{x}},
+%         \overline{\tv{r} \lessdot \tv{a}}
+%     }$
+% $(\Delta, \sigma) = \unify{}(\Delta_{in}, C \cup C')$
+
+% and $\text{wtv}(C') \cap \text{wtv}(C) = \emptyset$
+% and $\overline{\sigma(\tv{x}) = \wcNtype{\Delta}{N}}$
+
+% then $\Delta, \Delta', \overline{\Delta}$ are all the variables used in $C'$.
+% %if a wildcard type placeholder does not appear anywhere else, then only the free variables of its scope can be used for him
+% \end{lemma}
+
 % \begin{lemma} Unify does add free variables to types not containing free variables (or wildcard placeholders)
 % \begin{description}
 %     \item[If] $(\sigma, \Delta) = \unify{}( \Delta', C )$
@@ -272,29 +251,47 @@ by induction over every step of the \unify{} algorithm.
 Hint: a type placeholder $\tv{a}$ will never be replaced by a free variable or a type containing free variables.
 This fact together with the presumption that every supplied type is well-formed we can easily show that this lemma is true.
 
-\textit{Proof: (Variant 2)}
+% \textit{Proof: (Variant 2)}
-The GenSigma and GenDelta rules check for well-formedness.
+% The GenSigma and GenDelta rules check for well-formedness.
+
+
+\begin{lemma}\label{lemma:wildcardWellFormedness}
+\unify{} generates well-formed existential types
+\begin{description}
+\item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$
+\item[and] $\forall \wcNtype{\Delta''}{N} \in C: \text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
+\item[and] $\sigma(\tv{a}) = \wcNtype{\Delta'}{N}$
+%\item[then] $\Delta \vdash \ol{L <: U}$ and $\Delta \vdash \ol{U <: U'}$ % (with U' being upper limit by class definition)
+\item[then] $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$
+\end{description}
+\end{lemma}
+\textit{Proof} is straightforward induction over the transformation rules of \unify{}
+under the assumption that all supplied existential types are satisfying the premise.
+All parts of \unify{} that generate wildcard types always spawn types $\wcNtype{\Delta'}{N}$
+with $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$.
+Only the \rulename{Adapt} rule is able to produce types neglecting the premise,
+but is immediately corrected by the \rulename{Trim} rule.
 
 % All types supplied to the Unify algorithm by TYPEs only contain ? extends or ? super wildcards. (X : [bot..T] or X : [T .. Object]).
 % Both are well formed!
 
-\begin{lemma}\label{lemma:wfHereditary}
+% \begin{lemma}\label{lemma:wfHereditary}
-    Well-formedness is hereditary
+%     Well-formedness is hereditary
-    \begin{description}
+%     \begin{description}
-        \item[If] $\triangle \vdash \exptype{C}{\ol{X}} \ \ok$ and $\triangle \vdash \exptype{C}{\ol{X}} <: \type{S}$
+%         \item[If] $\triangle \vdash \exptype{C}{\ol{X}} \ \ok$ and $\triangle \vdash \exptype{C}{\ol{X}} <: \type{S}$
-        \item[Then] $\triangle \vdash \type{S} \ \ok$
+%         \item[Then] $\triangle \vdash \type{S} \ \ok$
-    \end{description}
+%     \end{description}
-\end{lemma}
+% \end{lemma}
-\textit{Proof:}
+% \textit{Proof} by induction on subtyping rules in figure \ref{fig:subtyping}
 
-\begin{lemma}
+% \begin{lemma}
     
-    \begin{description}
+%     \begin{description}
-        \item[If] $\Delta \vdash \wctype{\Delta'}{C}{\ol{T}} \ \ok$
+%         \item[If] $\Delta \vdash \wctype{\Delta'}{C}{\ol{T}} \ \ok$
-        \item[Then] $\Delta, \Delta' \vdash \ok{T} \ \ok$
+%         \item[Then] $\Delta, \Delta' \vdash \ok{T} \ \ok$
-    \end{description}
+%     \end{description}
-\end{lemma}
+% \end{lemma}
-\textit{Proof:} by definition of WF-Class
+% \textit{Proof:} by definition of WF-Class
 
 
 \begin{lemma} \label{lemma:tvsNoFV}
@@ -315,32 +312,64 @@ Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises.
 % Delta |-  N <. T
 % \end{lemma}
 
-\begin{lemma} \label{lemma:unifyWeakening}
+% \begin{lemma}\label{lemma:wildcardsStayInScope}
-Removing constraints does not render \unify{} impossible as long as the removed constraints do not share wildcard placeholders.
+% Free variables can only hop to another constraint if they share the same wildcard placeholder.
-If there is a solution for a constraint set $C$, then there is also a solution for a subset of that constraint set.
+% \begin{description}
-\begin{description}
+%     \item[If] $(\sigma, \Delta) = \unify{} (\Delta', C \cup \set{\wcNtype{\Delta'}{N} \lessdot \tv{a}})$
-    \item[If] $(\sigma, \Delta) = \unify{}( C \cup C')$ and $\text{wtv}(C) \cap \text{wtv}(C') = \emptyset$
+%     \item[and] $\tv{a}$ being a type placeholders used in $C$
-    \item[then] $ (\sigma', \Delta') = \unify{}( C')$
+%     \item[then] $\text{fv}(\sigma(\tv{a})) \subseteq \Delta, \Delta'$
-\end{description}
+% \end{description}
+% \end{lemma}
 
-\end{lemma}
+
-\textit{Proof:}
+
+%TODO: use this to proof soundness. Wildcard placeholders are not shared with other constraints and therefore only the wildcards generated by capture conversion are used in a let statement.
+
+% \begin{lemma} \label{lemma:unifyWeakening}
+% Removing constraints does not render \unify{} impossible as long as the removed constraints do not share wildcard placeholders.
+% If there is a solution for a constraint set $C$, then there is also a solution for a subset of that constraint set.
+% \begin{description}
+%     \item[If] $(\sigma, \Delta) = \unify{}( C \cup C')$% and $\text{wtv}(C) \cap \text{wtv}(C') = \emptyset$
+%     \item[then] $ (\sigma', \Delta') = \unify{}( C')$
+% \end{description}
+
+% \end{lemma}
+%\textit{Proof:}
 %TODO
 % does this really work. We have to show that the algorithm never gets stuck as long as there is a solution
 % maybe there are substitutions with types containing free variables that make additional solutions possible. Check!
-
+\begin{lemma}{\unify{} Soundness:}\label{lemma:unifySoundness}
-\begin{lemma}\label{lemma:unifySoundness}
+\unify{}'s type solutions are correct respective to the subtyping rules defined in figure \ref{fig:subtyping}.
-The \unify{} algorithm only produces correct output.
 \begin{description}
 \item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$
-%\item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
+\item[Then] there exists a substitution $\sigma'$ with:
-\item[Then] there exists a $\sigma'$ with:
+\begin{itemize}
-$\sigma \subseteq \sigma'$ and
+\item $\sigma \subseteq \sigma'$
-$\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
+\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
-and $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$ where $\overline{\sigma(\type{S'}) = \wcNtype{\Delta}{N}}$,
+\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \wcNtype{\Delta}{N}}$
-otherwise $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \sigma'(\type{T'})}$
+\item $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$
-% and $\sigma(\type{T'}) = \sigma(\type{T'})$.
+\end{itemize}
+\end{description}
+\end{lemma}
 
+\begin{lemma}{\unify{} Soundness:}%\label{lemma:unifySoundness}
+\unify{}'s type solutions are correct respective to the subtyping rules defined in figure \ref{fig:subtyping}.
+\begin{description}
+\item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$
+with $\text{wtv}(\ol{S}) = \emptyset$ and $\text{wtv}(\ol{T}) = \emptyset$
+\item[Then] $\Delta, \Delta' \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$
+\item[and] either $\Delta, \Delta' \vdash \overline{\sigma(\type{S'}) <: \sigma(\type{T'})}$
+or $\Delta, \Delta', \overline{\Delta} \vdash \overline{\sigma'(\type{S'}) <: \sigma(\type{T'})}$
+with the capture converted substitution $\sigma' = \set{ \tv{a} \mapsto \type{N} \mid \tv{a} \mapsto \wcNtype{\Delta}{N} \in \sigma}$
+and $\overline{\Delta} = \set{\Delta \mid \tv{a} \mapsto \wcNtype{\Delta}{N} \in \sigma }$
+
+% there exists a substitution $\sigma'$ and a set of types $\overline{\wcNtype{\Delta}{N}}$ with:
+% \begin{itemize}
+% \item $\sigma \subseteq \sigma'$
+% \item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
+% \item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \wcNtype{\Delta}{N}}$ 
+% \item $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$
+% \end{itemize}
 \end{description}
 \end{lemma}
 
@@ -378,6 +407,7 @@ $\Delta \vdash  \sigma(C') \implies \Delta \vdash \sigma(C)$
 \begin{description}
 \item[AddDelta] $C$ is not changed
 \item[GenDelta] by definition, S-Var-Left, and S-Trans %The generated type variable is unique due to the solved form property. %and the solved form property (no $\tv{a}$ in $C$)
+\item[GenDelta'] same as GenDelta by setting $\sigma'(\wtv{b}) = \rwildcard{B}$
 \item[GenSigma] by definition and S-Refl.
 % holds for $\set{\tv{a} \doteq \type{G}}$ by definition.
 % Holds for $C$ by assumption and because $\tv{a} \notin C$ by solved form definition ($[\type{G}/\tv{a}]C = C$).
@@ -388,6 +418,8 @@ $\Delta \vdash  \sigma(C') \implies \Delta \vdash \sigma(C)$
 \item[Settle] Assumption, S-Trans
 \item[Super] S-Extends ($\vdash \wctype{\Delta}{C}{\ol{T}} <: \wctype{\Delta}{D}{[\ol{T}/\ol{X}]\ol{N}}$), S-Trans
 \item[\generalizeRule{}] by Assumption, because $C \subset C'$
+\item[Same] by S-Exists
+\item[SameW] %TODO
 \item[Adapt] Assumption, S-Extends, S-Trans
 \item[Adopt] Assumption, because $C \subset C'$
 %\item[Capture, Reduce] are always applied together. We have to destinct between two cases:
@@ -411,6 +443,13 @@ Therefore we can say that $\Delta, \Delta', \overline{\Delta} \vdash \sigma'(\ex
 <: \sigma'(\wctype{\Delta}{C}{\ol{T}})$ with $\overline{\Delta}$ being all the fresh wildcards generated by \rulename{Capture}.
 
 \item[Reduce]
+To proof $\wctype{\Delta}{C}{\ol{S}} <: \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{T}}$
+we have to show S-Exists for some $\Delta''$ and $\ol{T} = \sigma(\overline{\wtv{a}})$:
+\begin{itemize}
+\item $\Delta'' \vdash \subst{\ol{T}}{\ol{X}}\ol{L} <: \ol{T}$ by assumption and $\subst{\ol{\wtv{a}}}{\ol{X}}\ol{L} \lessdot \ol{\wtv{a}}$
+\item $\Delta'' \vdash \ol{T} <: \subst{\ol{T}}{\ol{X}}\ol{U}$ by assumption and $\ol{\wtv{a}} \lessdot \subst{\ol{\wtv{a}}}{\ol{X}}\ol{L}$
+\item $\text{fv}(\ol{T}) \subseteq \text{dom}(\Delta'', \Delta')$ by setting $\Delta''$ accordingly
+\end{itemize}
 
 %Assumption and S-Exists.
 % Three different cases of the constraint $\exptype{C}{\ol{S}} \lessdot \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}$:
@@ -424,7 +463,7 @@ Therefore we can say that $\Delta, \Delta', \overline{\Delta} \vdash \sigma'(\ex
 % List<X> <. Y.List<Y>, free variables are either in 
 If $\text{fv}(\exptype{C}{\ol{S}}) = \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists.
 Otherwise 
-$\Delta' \vdash \CC{}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$
+$\Delta' \vdash \text{CC}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$
 holds with any $\Delta'$ so that $(\text{fv}(\exptype{C}{\ol{S}}) \cup \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) ) \subseteq \text{dom}(\Delta') $.
 \item[Match] Assumption, S-Trans
 \item[Trim] Assumption and S-Exists
@@ -432,7 +471,8 @@ holds with any $\Delta'$ so that $(\text{fv}(\exptype{C}{\ol{S}}) \cup \text{fv}
 \item[Circle] S-Refl
 \item[Swap] by definition
 \item[Erase] S-Refl
-\item[Equals] %by definition
+\item[Equals] by definition \ref{def:equal}
+%by definition
 %TODO
 % Unify does never contain wildcard environments with unused wildcards. Therefore after N <: N' and N' <: N, both types have the same wildcard environment
 
@@ -505,159 +545,165 @@ $\sigma(\wildcardEnv) = \sigma([\type{T}/\tv{a}]\wildcardEnv)$
 Same as Subst
 \end{description}
 
+\begin{lemma}
+\label{lemma:freeVariablesOnlyTravelOneHop}
+A constraint $\tv{a} \lessdotCC \type{T}$ or $\tv{a} \lessdot \type{T}$ implies that
+$\text{fv}(\sigma(\type{T})) \subseteq \text{fv}(\sigma(\tv{a}))$.
+Only free variables, which are part of the left side are used on the right side.
+\end{lemma}
 
-\subsection{Converting to Wild FJ}
+% \subsection{Converting to Wild FJ}
-Wildcards are existential types which have to be \textit{unpacked} before they can be used.
+% Wildcards are existential types which have to be \textit{unpacked} before they can be used.
-In Java this is done implicitly by a process called capture conversion \cite{JavaLanguageSpecification}.
+% In Java this is done implicitly by a process called capture conversion \cite{JavaLanguageSpecification}.
-The type system in \cite{WildcardsNeedWitnessProtection} makes this process explicit by using \texttt{let} statements.
+% The type system in \cite{WildcardsNeedWitnessProtection} makes this process explicit by using \texttt{let} statements.
-Our type inference algorithm will accept an input program without let statements and add them where necessary.
+% Our type inference algorithm will accept an input program without let statements and add them where necessary.
 
-%Type inference adds \texttt{let} statements in a fashion similar to the Java capture conversion \cite{WildFJ}.
+% %Type inference adds \texttt{let} statements in a fashion similar to the Java capture conversion \cite{WildFJ}.
-%We wrap every parameter of a method invocation in \texttt{let} statement unknowing if a capture conversion is necessary.
+% %We wrap every parameter of a method invocation in \texttt{let} statement unknowing if a capture conversion is necessary.
 
-Figure \ref{fig:tletexpr} shows type rules for fields and method calls.
+% Figure \ref{fig:tletexpr} shows type rules for fields and method calls.
-They have been merged with let statements and simplified.
+% They have been merged with let statements and simplified.
 
-The let statements and the type $\wcNtype{\Delta'}{N}$, which the type inference algorithm can freely choose,
+% The let statements and the type $\wcNtype{\Delta'}{N}$, which the type inference algorithm can freely choose,
-are necessary for the soundness proof.
+% are necessary for the soundness proof.
 
-%TODO: Show that well-formed implies witnessed!
+% %TODO: Show that well-formed implies witnessed!
-We change the type rules to require the well-formedness instead of the witnessed property.
+% We change the type rules to require the well-formedness instead of the witnessed property.
-See figure \ref{fig:well-formedness}.
+% See figure \ref{fig:well-formedness}.
 
-Our well-formedness criteria is more restrictive than the ones used for \wildFJ{}.
+% Our well-formedness criteria is more restrictive than the ones used for \wildFJ{}.
-\cite{WildcardsNeedWitnessProtection} works with the two different judgements $\ok$ and \texttt{witnessed}.
+% \cite{WildcardsNeedWitnessProtection} works with the two different judgements $\ok$ and \texttt{witnessed}.
-With \texttt{witnessed} being the stronger one.
+% With \texttt{witnessed} being the stronger one.
-We rephrased the $\ok$ judgement to include \texttt{witnessed} aswell.
+% We rephrased the $\ok$ judgement to include \texttt{witnessed} aswell.
-$\type{T} \ \ok$ in this paper means $\type{T} \ \ok$ and $\type{T} \ \texttt{witnessed}$ in the sense of the \wildFJ{} type rules.
+% $\type{T} \ \ok$ in this paper means $\type{T} \ \ok$ and $\type{T} \ \texttt{witnessed}$ in the sense of the \wildFJ{} type rules.
-Java's type system is complex enough as it is. Simplification, when possible, is always appreciated.
+% Java's type system is complex enough as it is. Simplification, when possible, is always appreciated.
-Our $\ok$ rule may not be able to express every corner of the Java type system, but is sufficient to show soundness regarding type inference for a Java core calculus.
+% Our $\ok$ rule may not be able to express every corner of the Java type system, but is sufficient to show soundness regarding type inference for a Java core calculus.
 
-The \rulename{WF-Class} rule requires upper and lower bounds to be direct subtypes of each other $\type{L} <: \type{U}$.
+% The \rulename{WF-Class} rule requires upper and lower bounds to be direct subtypes of each other $\type{L} <: \type{U}$.
-The type rules from \cite{WildcardsNeedWitnessProtection} use a witness type instead.
+% The type rules from \cite{WildcardsNeedWitnessProtection} use a witness type instead.
-Stating that a type is well formed (\texttt{witnessed}) if there exists atleast one simple type $\type{N}$ as a possible subtype:
+% Stating that a type is well formed (\texttt{witnessed}) if there exists atleast one simple type $\type{N}$ as a possible subtype:
-$\Delta \vdash \type{N} <: \wctype{\Delta'}{C}{\ol{T}}$.
+% $\Delta \vdash \type{N} <: \wctype{\Delta'}{C}{\ol{T}}$.
 
-A witness type is easy to find by replacing every wildcard $\ol{W}$ in $\wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$ by its upper bound:
+% A witness type is easy to find by replacing every wildcard $\ol{W}$ in $\wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$ by its upper bound:
-$\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} <: \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$.
+% $\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} <: \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}}$.
-$\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} \ \texttt{witnessed}$ is given due to $\Delta \vdash \ol{T}, \ol{L}, \ol{U} \ \ok$
+% $\Delta \vdash \exptype{C}{[\ol{U}/\ol{W}]\ol{T}} \ \texttt{witnessed}$ is given due to $\Delta \vdash \ol{T}, \ol{L}, \ol{U} \ \ok$
-and $\Delta \vdash \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}} \ \ok$.
+% and $\Delta \vdash \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}} \ \ok$.
 
-\begin{figure}[tp]
+% \begin{figure}[tp]
-$\begin{array}{l}
+% $\begin{array}{l}
-    \typerule{T-Var}\\
+%     \typerule{T-Var}\\
-    \begin{array}{@{}c}
+%     \begin{array}{@{}c}
-        x : \type{T} \in \Gamma
+%         x : \type{T} \in \Gamma
-        \\
+%         \\
-        \hline
+%         \hline
-    \vspace*{-0.3cm}\\
+%     \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash x : \type{T}
+%         \Delta | \Gamma \vdash x : \type{T}
-    \end{array}
+%     \end{array}
-\end{array}$
+% \end{array}$
-\\[1em]
+% \\[1em]
-$\begin{array}{l}
+% $\begin{array}{l}
-    \typerule{T-New}\\
+%     \typerule{T-New}\\
-    \begin{array}{@{}c}
+%     \begin{array}{@{}c}
-        \Delta, \overline{\Delta} \vdash  \exptype{C}{\ol{T}} \ \ok \quad \quad
+%         \Delta, \overline{\Delta} \vdash  \exptype{C}{\ol{T}} \ \ok \quad \quad
-        \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
+%         \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
-        \Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
+%         \Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
-        \Delta \vdash  \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
+%         \Delta \vdash  \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
-        \Delta, \overline{\Delta} \vdash  \overline{\type{N}} <: \overline{\type{U}} \quad \quad
+%         \Delta, \overline{\Delta} \vdash  \overline{\type{N}} <: \overline{\type{U}} \quad \quad
-        \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
+%         \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
-        \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
+%         \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
-        \Delta \vdash \type{T},  \overline{\wcNtype{\Delta}{N}} \ \ok
+%         \Delta \vdash \type{T},  \overline{\wcNtype{\Delta}{N}} \ \ok
-        \\
+%         \\
-        \hline
+%         \hline
-    \vspace*{-0.3cm}\\
+%     \vspace*{-0.3cm}\\
-    \Delta | \Gamma \vdash \letstmt{\ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}{\texttt{new} \ \exptype{C}{\ol{T}}(\overline{t})} : \type{T}
+%     \Delta | \Gamma \vdash \letstmt{\ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}{\texttt{new} \ \exptype{C}{\ol{T}}(\overline{t})} : \type{T}
-    \end{array}
+%     \end{array}
-\end{array}$
+% \end{array}$
-\\[1em]
+% \\[1em]
-$\begin{array}{l}
+% $\begin{array}{l}
-    \typerule{T-Field}\\
+%     \typerule{T-Field}\\
-    \begin{array}{@{}c}
+%     \begin{array}{@{}c}
-        \Delta | \Gamma \vdash \texttt{t} : \type{T} \quad \quad 
+%         \Delta | \Gamma \vdash \texttt{t} : \type{T} \quad \quad 
-        \Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
+%         \Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
-        \textit{fields}(\type{N}) = \ol{U\ f} \\
+%         \textit{fields}(\type{N}) = \ol{U\ f} \\
-\Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
+% \Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
-\text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
+% \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
-\Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
+% \Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
-        \\
+%         \\
-        \hline
+%         \hline
-    \vspace*{-0.3cm}\\
+%     \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash \texttt{let}\ x : \wcNtype{\Delta'}{N} = \texttt{t} \ \texttt{in}\ x.\texttt{f}_i : \type{S}
+%         \Delta | \Gamma \vdash \texttt{let}\ x : \wcNtype{\Delta'}{N} = \texttt{t} \ \texttt{in}\ x.\texttt{f}_i : \type{S}
-    \end{array}
+%     \end{array}
-\end{array}$
+% \end{array}$
-\\[1em]
+% \\[1em]
-$\begin{array}{l}
+% $\begin{array}{l}
-    \typerule{T-Call}\\
+%     \typerule{T-Call}\\
-    \begin{array}{@{}c}
+%     \begin{array}{@{}c}
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
+%         \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
-        \textit{mtype}(\texttt{m}, \type{N}) = \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \quad \quad
+%         \textit{mtype}(\texttt{m}, \type{N}) = \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \quad \quad
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
+%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
-        \\
+%         \\
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
+%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
-        \Delta | \Gamma \vdash \texttt{t}_r : \type{T}_r \quad \quad
+%         \Delta | \Gamma \vdash \texttt{t}_r : \type{T}_r \quad \quad
-        \Delta | \Gamma \vdash \ol{t} : \ol{T} \quad \quad
+%         \Delta | \Gamma \vdash \ol{t} : \ol{T} \quad \quad
-        \Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
+%         \Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
-        \Delta \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
+%         \Delta \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
-        \\
+%         \\
-        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
+%         \Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
-        \Delta, \Delta', \Delta'' \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
+%         \Delta, \Delta', \Delta'' \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
-        \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
+%         \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
-        \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
+%         \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
-        \\
+%         \\
-        \hline
+%         \hline
-    \vspace*{-0.3cm}\\
+%     \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash \letstmt{x : \wcNtype{\Delta'}{N} = t_r, \ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}
+%         \Delta | \Gamma \vdash \letstmt{x : \wcNtype{\Delta'}{N} = t_r, \ol{x} : \ol{\wcNtype{\Delta}{N}} = \ol{t}}
-        {\texttt{x}.\generics{\ol{S}}\texttt{m}(\ol{x})} : \type{T}
+%         {\texttt{x}.\generics{\ol{S}}\texttt{m}(\ol{x})} : \type{T}
-    \end{array}
+%     \end{array}
-\end{array}$
+% \end{array}$
-\\[1em]
+% \\[1em]
-$\begin{array}{l}
+% $\begin{array}{l}
-    \typerule{T-Elvis}\\
+%     \typerule{T-Elvis}\\
-    \begin{array}{@{}c}
+%     \begin{array}{@{}c}
-        \Delta | \Gamma \vdash t_1 : \type{T}_1 \quad \quad 
+%         \Delta | \Gamma \vdash t_1 : \type{T}_1 \quad \quad 
-        \Delta | \Gamma \vdash t_2 : \type{T}_2 \quad \quad
+%         \Delta | \Gamma \vdash t_2 : \type{T}_2 \quad \quad
-        \Delta \vdash \type{T}_1 <: \type{T} \quad \quad
+%         \Delta \vdash \type{T}_1 <: \type{T} \quad \quad
-        \Delta \vdash \type{T}_2 <: \type{T}
+%         \Delta \vdash \type{T}_2 <: \type{T}
-        \\
+%         \\
-        \hline
+%         \hline
-    \vspace*{-0.3cm}\\
+%     \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash t_1 \elvis{} t_2 : \type{T}
+%         \Delta | \Gamma \vdash t_1 \elvis{} t_2 : \type{T}
-    \end{array}
+%     \end{array}
-\end{array}$
+% \end{array}$
-\\[1em]
+% \\[1em]
-$\begin{array}{l}
+% $\begin{array}{l}
-        \typerule{T-Method}\\
+%         \typerule{T-Method}\\
-    \begin{array}{@{}c}
+%     \begin{array}{@{}c}
-        \text{dom}(\Delta)=\ol{X} \quad \quad
+%         \text{dom}(\Delta)=\ol{X} \quad \quad
-        \Delta' = \overline{\type{Y} : \bot .. \type{U}} \quad \quad
+%         \Delta' = \overline{\type{Y} : \bot .. \type{U}} \quad \quad
-        \Delta, \Delta' \vdash \ol{U}, \type{T}, \ol{T}\ \ok \quad \quad
+%         \Delta, \Delta' \vdash \ol{U}, \type{T}, \ol{T}\ \ok \quad \quad
-        \texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \set{\ldots} \\
+%         \texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \set{\ldots} \\
-        \Delta, \Delta' | \overline{x:\type{T}}, \texttt{this} : \exptype{C}{\ol{X}} \vdash t:\type{S} \quad \quad
+%         \Delta, \Delta' | \overline{x:\type{T}}, \texttt{this} : \exptype{C}{\ol{X}} \vdash t:\type{S} \quad \quad
-        \Delta, \Delta' \vdash \type{S} <: \type{T} \quad \quad 
+%         \Delta, \Delta' \vdash \type{S} <: \type{T} \quad \quad 
-        \text{override}(\texttt{m}, \type{N}, \generics{\ol{Y \triangleleft U}}\ol{T} \to \type{T})
+%         \text{override}(\texttt{m}, \type{N}, \generics{\ol{Y \triangleleft U}}\ol{T} \to \type{T})
-        \\
+%         \\
-        \hline
+%         \hline
-    \vspace*{-0.3cm}\\
+%     \vspace*{-0.3cm}\\
-        \Delta \vdash \generics{\ol{Y \triangleleft U}} \type{T} \ \texttt{m}(\overline{\type{T} \ x}) = t \ \ok \ \texttt{in C}
+%         \Delta \vdash \generics{\ol{Y \triangleleft U}} \type{T} \ \texttt{m}(\overline{\type{T} \ x}) = t \ \ok \ \texttt{in C}
-    \end{array}
+%     \end{array}
-\end{array}$
+% \end{array}$
-\\[1em]
+% \\[1em]
-$\begin{array}{l}
+% $\begin{array}{l}
-        \typerule{T-Class}\\
+%         \typerule{T-Class}\\
-    \begin{array}{@{}c}
+%     \begin{array}{@{}c}
-        \Delta = \overline{\type{X} : \bot .. \type{U}} \quad \quad 
+%         \Delta = \overline{\type{X} : \bot .. \type{U}} \quad \quad 
-        \Delta \vdash \ol{U}, \ol{T} \ \ok \quad \quad
+%         \Delta \vdash \ol{U}, \ol{T} \ \ok \quad \quad
-        \Delta \vdash \type{N} \ \ok \quad \quad
+%         \Delta \vdash \type{N} \ \ok \quad \quad
-        \Delta \vdash \ol{M} \ \ok \texttt{ in C}
+%         \Delta \vdash \ol{M} \ \ok \texttt{ in C}
-        \\
+%         \\
-        \hline
+%         \hline
-    \vspace*{-0.3cm}\\
+%     \vspace*{-0.3cm}\\
-        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M} } \ \ok
+%         \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M} } \ \ok
-    \end{array}
+%     \end{array}
-\end{array}$
+% \end{array}$
-\caption{T-Call and T-Field} \label{fig:tletexpr}
+% \caption{T-Call and T-Field} \label{fig:tletexpr}
-\end{figure}
+% \end{figure}
 

tRules.tex

@@ -1,32 +1,85 @@
-\section{Syntax and Typing}\label{sec:tifj}
 
-The input syntax for our algorithm is shown in figure \ref{fig:syntax}
+\section{\TamedFJ{}}\label{sec:tifj}
-and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}.
+%LetFJ -> Output language!
+%TamedFJ -> ANF transformed input langauge
+%Input language only described here. It is standard Featherweight Java
+% we use the transformation to proof soundness. this could also be moved to the end. 
+% the constraint generation step assumes every method argument to be encapsulated in a let statement. This is the way Java is doing capture conversion
+This section defines the calculus \TamedFJ{}, which is used as input and output of our global type inference algorithm.
+%We assume that the input to our algorithm is a program, which carries none of the optional type annotations.
+%After calculating a type solution we can insert all missing types and generate a correct program.
+%The input to our algorithm is a typeless version of Featherweight Java.
+Figure~\ref{fig:syntax} contains the syntax with optional type annotations highlighted in yellow.
+The respective typing rules are defined in Figures~\ref{fig:expressionTyping} and~\ref{fig:typing}.
+\TamedFJ{} is a subset of the calculus defined by Bierhoff
+\cite{WildcardsNeedWitnessProtection}, but in addition we make the types for
+method arguments and return types optional. 
+The point is that a correct and fully typed \TamedFJ{} program is also a correct Featherweight Java program,
+which is vital for our soundness proof (chapter \ref{sec:soundness}).
+%The language is designed to showcase type inference involving existential types.
 
-Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
+A method assumption consists of a method name, a list of type variables, a list of argument types, and a return type.
-The input language is designed to showcase type inference involving existential types.
+The first type in the list of argument types is the type of the surrounding class also known as the \texttt{this} parameter.
-Method call rule T-Call is the most interesting part, because it emulates the behaviour of a Java method call,
+See Figure~\ref{fig:methodTypeExample} for an example, where the
-where existential types are implicitly \textit{opened} and \textit{closed}.
+\texttt{add} method is treated internally as a method with two
-
+arguments, because we add \texttt{this} to its argument list.
-Example: %TODO
+The type variable $\type{A}$ of the surrounding class is part of the
-\begin{verbatim}
+method's list of type parameters.
-class List<A> {
+%For example the \texttt{add} method in listing \ref{lst:tamedfjSample} is represented by the assumption
-    A head;
+%$\texttt{add} : \generics{\ol{X \triangleleft Object}}\ \type{X} \to \exptype{List}{\type{X}}$.
-    List<A> tail;
+\begin{figure}
-
+\center
-    add(v) = new List(v, this);
+\begin{minipage}{0.49\textwidth}
+    %[style=java,caption=\TamedFJ{} sample, label=lst:tamedfjSample]
+\begin{lstlisting}
+class List<A extends Object> {
+    List<A> add(A v){..,}
 }
-\end{verbatim}
+\end{lstlisting}
+\end{minipage}
+\begin{minipage}{0.49\textwidth}
+\begin{align*}
+&\mathrm{\Pi} = \set{\\
+&\texttt{add} : \generics{\type{A} \triangleleft \type{Object}}\ \exptype{List}{\type{A}},\type{A} \to \exptype{List}{\type{A}} \\
+&}
+\end{align*}
+\end{minipage}
+% \begin{minipage}{0.49\textwidth}
+% \begin{lstlisting}[style=java,caption=\TamedFJ{} sample, label=lst:tamedfjSample]
+% class List<A extends Object> {}
+% <A extends Object> List<A>
+%     add(List<A> this, A v){..,}
+% \end{lstlisting}
+% \end{minipage}
+\caption{\TamedFJ{} class and its corresponding method type environment}\label{fig:methodTypeExample}
+\end{figure}
 
-%The rules depicted here are type inference rules. It is not possible to derive a distinct typing from a given input program.
+\textit{Additional Notes:}%
-
+\begin{itemize}
-%The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}.
+%\item Method parameters and return types are optional.
-%and is solely used for examples.
+\item We require type annotations for fields and generic class parameters,
-The calculus does not include method overriding for simplicity reasons.
+  as we consider them as data declarations which are given by the programmer.
-Type inference for that is described in \cite{TIforFGJ} and can be added to this algorithm accordingly.
+% They are inferred in for example \cite{plue14_3b}
-Our algorithm is designed for extensibility with the final goal of full support for Java.
+\item We add the elvis operator ($\elvis{}$) to the syntax to easily showcase applications involving wildcard types.
-\unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
+This operator is used to emulate Java's \texttt{if-else} expression but without the condition clause.
-Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
+Our operator just returns one of the two given statements at random.
+The point is that the return type of the elvis operator has to be a supertype of its two subexpressions.
+\item The \texttt{new} expression does not require generic parameters.
+\item Every method has an unique name.
+The calculus does not include method overriding for simplicity.
+Type inference with method overriding is described elsewhere
+\cite{TIforFGJ} and can be added to our algorithm in a similar way.
+\item The \textsc{T-Program} typing rule ensures that there is one set of method assumptions used for all classes
+that are part of the program.
+\item Unlike previous work \cite{TIforFGJ},  the typing rules for expressions shown in
+  Figure~\ref{fig:expressionTyping} allow for polymorphic recursion.
+  Type inference for polymorphic recursion is undecidable
+  \cite{wells1999typability} and when proving completeness the calculus needs to be restricted in that regard (cf.\
+  \cite{TIforFGJ}).
+  Our algorithm is not complete (see discussion in section
+  \ref{sec:completeness}), so we keep the \TamedFJ{} calculus as simple as possible
+  and close to Featherweight Java to simplify the soundness proof. 
+\end{itemize}
 
 %Additional features like overriding methods and method overloading can be added by copying the respective parts from there.
 %Additional features can be easily added by generating the respective constraints (Plümicke hier zitieren)
@@ -38,32 +91,38 @@ Additional language constructs can be added by implementing the respective const
 % on overriding methods, because their type is already determined.
 % Allowing overriding therefore has no implication on our type inference algorithm.
 
+% The output is a valid Featherweight Java program.
+% We use the syntax of the version introduced in \cite{WildcardsNeedWitnessProtection}
+% calling it \letfj{} for that it is a Featherweight Java variant including \texttt{let} statements.
+
+\newcommand{\highlight}[1]{\begingroup\fboxsep=0pt\colorbox{yellow}{$\displaystyle #1$}\endgroup}
 \begin{figure}
+\par\noindent\rule{\textwidth}{0.4pt}
+\center
 $
 \begin{array}{lrcl}
-\hline
+%\hline
 \text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
 \text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
 \text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
 \text{Type variable contexts} &  \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
 \text{Class declarations} &  D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\
-\text{Method declarations} &  \texttt{M} & ::= & \texttt{m}(\overline{x}) = t \\
+\text{Method declarations} &  \texttt{M} & ::= & \highlight{\generics{\overline{\type{X} \triangleleft \type{N}}}}\ \highlight{\type{T}}\ \texttt{m}(\overline{\highlight{\type{T}}\ \expr{x}}) \{ \texttt{return} \ \expr{e}; \} \\
-\text{Terms} & t & ::= & x \\
+\text{Terms} & \expr{e} & ::= & \expr{x} \\
-& & \ \ | & \texttt{new} \ \type{C}(\overline{t})\\
+& & \ \ | & \texttt{new} \ \type{C}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
-& & \ \ | & t.f\\
+& & \ \ | & \expr{e}.f\\
-& & \ \ | & t.\texttt{m}(\overline{t})\\
+& & \ \ | & \expr{e}.\texttt{m}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
-& & \ \ | & t \elvis{} t\\
+& & \ \ | & \texttt{let}\ \expr{x} \highlight{: \wcNtype{\Delta}{N}} = \expr{e} \ \texttt{in} \ \expr{e}\\
-\text{Variable contexts} & \Gamma & ::= & \overline{x:\type{T}}\\
+& & \ \ | & \expr{e} \elvis{} \expr{e}\\
-\hline
+\text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
+\text{Method type environment} & \mathrm{\Pi} & ::= & \overline{ \texttt{m} : \generics{\ol{X \triangleleft N}}\ \ol{T} \to \type{T}}
+%\hline
 \end{array}
 $
-\caption{Input Syntax}\label{fig:syntax}
+\par\noindent\rule{\textwidth}{0.4pt}
+\caption{Input Syntax with optional type annotations}\label{fig:syntax}
 \end{figure}
 
-% Each class type has a set of wildcard types $\overline{\Delta}$ attached to it.
-% The type $\wctype{\overline{\Delta}}{C}{\ol{T}}$ defines a set of wildcards $\overline{\Delta}$,
-% which can be used inside the type parameters $\ol{T}$.
-
 \begin{figure}[tp]
 \begin{center}
 $\begin{array}{l}
@@ -72,17 +131,19 @@ $\begin{array}{l}
         \Delta \vdash \type{T} <: \type{T}
     \end{array}
  \end{array}$
+ \qquad
 $\begin{array}{l}
     \typerule{S-Trans}\\
     \begin{array}{@{}c}
-        \Delta \vdash \type{S} <: \type{T}' \quad \quad
+        \Delta \vdash \type{S} <: \type{T} \quad \quad
-        \Delta \vdash \type{T}' <: \type{T}
+        \Delta \vdash \type{T} <: \type{U}
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \Delta \vdash \type{S} <: \type{T}
+        \Delta \vdash \type{S} <: \type{U}
     \end{array}
  \end{array}$
+ \qquad
 $\begin{array}{l}
     \typerule{S-Upper}\\
     \begin{array}{@{}c}
@@ -93,6 +154,7 @@ $\begin{array}{l}
         \Delta \vdash \type{X} <: \type{U}
     \end{array}
  \end{array}$
+ \qquad
 $\begin{array}{l}
     \typerule{S-Lower}\\
     \begin{array}{@{}c}
@@ -115,13 +177,14 @@ $\begin{array}{l}
         \Delta \vdash \wctype{\Delta'}{C}{\ol{T}} <: \wcNtype{\Delta'}{[\ol{T}/\ol{X}]\type{N}}
     \end{array}
  \end{array}$
+ \quad
 $\begin{array}{l}
     \typerule{S-Exists}\\
     \begin{array}{@{}c}
         \Delta', \Delta \vdash [\ol{T}/\ol{\type{X}}]\ol{L} <: \ol{T} \quad \quad
         \Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\
         \text{fv}(\ol{T}) \subseteq \text{dom}(\Delta, \Delta') \quad
-        \text{dom}(\Delta') \cap \text{fv}(\wctype{\ol{\wildcard{X}{U}{L}}}{C}{\ol{S}}) = \emptyset
+        \text{dom}(\Delta') \cap \text{fv}(\wcNtype{\ol{\wildcard{X}{U}{L}}}{N}) = \emptyset
         \\
         \hline
     \vspace*{-0.3cm}\\
@@ -141,6 +204,7 @@ $\begin{array}{l}
         \Delta \vdash \bot \ \ok
     \end{array}
 \end{array}$
+\qquad
 $\begin{array}{l}
     \typerule{WF-Top}\\
     \begin{array}{@{}c}
@@ -151,6 +215,7 @@ $\begin{array}{l}
         \Delta \vdash \overline{\wildcard{W}{U}{L}}.\texttt{Object}
     \end{array}
 \end{array}$
+\qquad
 $\begin{array}{l}
     \typerule{WF-Var}\\
     \begin{array}{@{}c}
@@ -196,70 +261,129 @@ $\begin{array}{l}
 $\begin{array}{l}
     \typerule{T-Field}\\
     \begin{array}{@{}c}
-        \Delta | \Gamma \vdash \texttt{e} : \type{T} \quad \quad 
+        \Delta | \Gamma \vdash \expr{v} : \type{T} \quad \quad 
-        \Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
+        \Delta \vdash \type{T} <: \wcNtype{}{N} \quad \quad
         \textit{fields}(\type{N}) = \ol{U\ f} \\
-\Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
-\text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
-\Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
-        \\
         \hline
     \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash \texttt{e}.\texttt{f}_i : \type{S}
+        \Delta | \Gamma \vdash \expr{v}.\texttt{f}_i : \type{U}_i
     \end{array}
 \end{array}$
 \\[1em]
+% $\begin{array}{l}
+%     \typerule{T-Field}\\
+%     \begin{array}{@{}c}
+%         \Delta | \Gamma \vdash \texttt{e} : \type{T} \quad \quad 
+%         \Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
+%         \textit{fields}(\type{N}) = \ol{U\ f} \\
+% \Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
+% \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
+% \Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%         \Delta | \Gamma \vdash \texttt{e}.\texttt{f}_i : \type{S}
+%     \end{array}
+% \end{array}$
+% \\[1em]
+% $\begin{array}{l}
+%     \typerule{T-New}\\
+%     \begin{array}{@{}c}
+%         \Delta, \overline{\Delta} \vdash  \exptype{C}{\ol{T}} \ \ok \quad \quad
+%         \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
+%         \Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
+%         \Delta \vdash  \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
+%         \Delta, \overline{\Delta} \vdash  \overline{\type{N}} <: \overline{\type{U}} \quad \quad
+%         \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
+%         \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
+%         \Delta \vdash \type{T},  \overline{\wcNtype{\Delta}{N}} \ \ok
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%         \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}}
+%     \end{array}
+% \end{array}$
+% \\[1em] 
 $\begin{array}{l}
     \typerule{T-New}\\
     \begin{array}{@{}c}
         \Delta, \overline{\Delta} \vdash  \exptype{C}{\ol{T}} \ \ok \quad \quad
-        \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
+        \Delta \vdash  \overline{\type{S}} <: \overline{\type{U}} \\
-        \Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
+        \Delta | \Gamma \vdash \overline{\expr{v} : \type{S}} \quad \quad
-        \Delta \vdash  \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
+        \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} 
-        \Delta, \overline{\Delta} \vdash  \overline{\type{N}} <: \overline{\type{U}} \quad \quad
-        \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
-        \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
-        \Delta \vdash \type{T},  \overline{\wcNtype{\Delta}{N}} \ \ok
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}}
+        \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{v}) : \exptype{C}{\ol{T}}
+    \end{array}
+\end{array}$
+\hfill
+% $\begin{array}{l}
+%     \typerule{T-Call}\\
+%     \begin{array}{@{}c}
+%         \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
+%         \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
+%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
+%         \\
+%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
+%         \Delta | \Gamma \vdash  \texttt{e}, \ol{e} : \ol{T} \quad \quad
+%         \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
+%         \\
+%         \Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
+%         \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
+%         \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
+%         \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%         \Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T}
+%     \end{array}
+% \end{array}$
+% \\[1em]
+$\begin{array}{l}
+    \typerule{T-Call}\\
+    \begin{array}{@{}c}
+        \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
+        \Delta \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
+        \\
+        \Delta \vdash \ol{S} \ \ok \quad \quad
+        \Delta | \Gamma \vdash  \expr{v}, \ol{v} : \ol{T} \quad \quad
+        \Delta \vdash \ol{T} <: [\ol{S}/\ol{X}]\ol{U} 
+        \\
+        \hline
+    \vspace*{-0.3cm}\\
+        \Delta | \Gamma \vdash \expr{v}.\texttt{m}(\ol{v}) : \type{T}
     \end{array}
 \end{array}$
 \\[1em]
 $\begin{array}{l}
-    \typerule{T-Call}\\
+    \typerule{T-Let}\\
     \begin{array}{@{}c}
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
+        \Delta | \Gamma \vdash \expr{t}_1 : \type{T}_1 \quad \quad
-        \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
+        \Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
         \\
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
+        \Delta, \Delta' | \Gamma, \expr{x} : \wcNtype{}{N} \vdash \expr{t}_2 : \type{T}_2 \quad \quad
-        \Delta | \Gamma \vdash  \texttt{e}, \ol{e} : \ol{T} \quad \quad
+        \Delta, \Delta' \vdash  \type{T}_2 <: \type{T} \quad \quad
-        \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
-        \\
-        \Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
-        \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
         \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
-        \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
+        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T}
+        \Delta | \Gamma \vdash \texttt{let}\ \expr{x} = \expr{t}_1 \ \texttt{in} \ \expr{t}_2 : \type{T}
     \end{array}
 \end{array}$
 \\[1em]
 $\begin{array}{l}
     \typerule{T-Elvis}\\
     \begin{array}{@{}c}
-        \triangle | \Gamma \vdash \texttt{t} : \type{T}_1 \quad \quad
+        \triangle | \Gamma \vdash \texttt{t}_1 : \type{S} \quad \quad
-        \triangle | \Gamma \vdash \texttt{t}_2 : \type{T}_2 \quad \quad
+        \triangle | \Gamma \vdash \texttt{t}_2 : \type{T} \quad \quad
-        \triangle \vdash \type{T}_1 <: \type{T} \quad \quad
+        \triangle \vdash \type{S} <: \type{U} \quad \quad
-        \triangle \vdash \type{T}_2 <: \type{T} \quad \quad
+        \triangle \vdash \type{T} <: \type{U} \quad \quad
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \triangle | \Gamma \vdash \texttt{t}_1 \ \texttt{?:} \ \texttt{t}_2 : \type{T}
+        \triangle | \Gamma \vdash \texttt{t}_1 \ \texttt{?:} \ \texttt{t}_2 : \type{U}
     \end{array}
 \end{array}$
 \end{center}
@@ -271,9 +395,10 @@ $\begin{array}{l}
 $\begin{array}{l}
     \typerule{T-Method}\\
     \begin{array}{@{}c}
-        (\type{T'},\ol{T}) \to \type{T} \in \mathtt{\Pi}(\texttt{m})\quad \quad
+        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\ldots} \quad \quad 
-        \triangle' =  \overline{\type{Y} : \bot .. \type{P}} \quad \quad
+        \generics{\ol{Y \triangleleft \type{N}}}(\exptype{C}{\ol{X}},\ol{T}) \to \type{T} \in \mathtt{\Pi}(\texttt{m}) \quad \quad
-        \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \\
+        \triangle' =  \overline{\type{Y} : \bot .. \type{P}} \\
+        \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \quad \quad
         \text{dom}(\triangle) = \ol{X} \quad \quad
         %\texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \ \{ \ldots \} \\
         \mathtt{\Pi} | \triangle, \triangle' | \ol{x : T}, \texttt{this} : \exptype{C}{\ol{X}} \vdash \texttt{e} : \type{S} \quad \quad 
@@ -281,38 +406,33 @@ $\begin{array}{l}
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \text{ in C with } \generics{\ol{Y \triangleleft P}}
+        \mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) \set{ \texttt{return}\ \texttt{e}; } \ \ok \ \text{in C}
     \end{array}
 \end{array}$
 \\[1em]
 $\begin{array}{l}
     \typerule{T-Class}\\
     \begin{array}{@{}c}
-        \mathtt{\Pi}' = \mathtt{\Pi} \cup \set{ \texttt{m} : (\type{T'_m}, \ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M}} \quad \quad
+        %\forall \texttt{m} \in \ol{M} : \mathtt{\Pi}(\texttt{m}) = \generics{\ol{X \triangleleft \type{N}}}(\exptype{C}{\ol{X}},\ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \\
-        \forall \texttt{m} \in \ol{M}: \Delta \vdash \exptype{C}{\ol{X}} <: \type{T'_m}\\
-        \mathtt{\Pi}'' = \mathtt{\Pi} \cup \set{ \texttt{m} :
-            \generics{\ol{X \triangleleft \type{N}}, \ol{Y \triangleleft P}}(\exptype{C}{\ol{X}},\ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M} } \\
         \triangle = \overline{\type{X} : \bot .. \type{U}} \quad \quad
         \triangle \vdash \ol{U}, \ol{T}, \type{N} \ \ok \quad \quad
-        \mathtt{\Pi}' | \triangle \vdash \ol{M} \ \ok \text{ in C with} \ \generics{\ol{Y \triangleleft P}}
+        \mathtt{\Pi} | \triangle \vdash \ol{M} \ \ok \text{ in C}
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \}  : \mathtt{\Pi}''
+        \mathtt{\Pi} \vdash \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \} 
     \end{array}
 \end{array}$
-\\[1em]
+%\\[1em]
+\hfill
 $\begin{array}{l}
     \typerule{T-Program}\\
     \begin{array}{@{}c}
-        \emptyset \vdash \texttt{L}_1 : \mathtt{\Pi}_1 \quad \quad 
+        \mathtt{\Pi} = \overline{\texttt{m} : \generics{\ol{X \triangleleft \type{N}}}\ol{T} \to \type{T}}
-        \mathtt{\Pi}_1 \vdash \texttt{L}_2 : \mathtt{\Pi}_1 \quad \quad 
-        \ldots \quad \quad 
-        \mathtt{\Pi}_{n-1} \vdash \texttt{L}_n : \mathtt{\Pi}_n \quad \quad 
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \vdash \ol{L} : \mathtt{\Pi}_n
+    \mathtt{\Pi} \vdash \overline{D}
     \end{array}
 \end{array}$
 \end{center}
@@ -335,4 +455,9 @@ $\begin{array}{l}
         \text{fields}(\exptype{C}{\ol{T}}) = \ol{U\ g}, [\ol{T}/\ol{X}]\ol{S\ f}
     \end{array}
 \end{array}$
+\caption{Field access}
 \end{figure}
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "TIforWildFJ"
+%%% End:

todo-11.4.24

@@ -0,0 +1,16 @@
+- Eingangsbeispiel
+- Motivation (gibt es ein nicht funktionierendes Beispiel für lokale Typinferenz was mit unserem algorithmus funktioniert)
+- Zeile 52 steht LetFJ, muss eingeführt werden
+	- Operatoren motivieren. Denotable expressable types
+	Java macht CC implizit. Wir machen es mit let statements. Dadurch LetFJ einführen
+	- Java macht es anders. es gibt keine let statements
+	- In java kann ich die lets nur in bestimmter Weise einbauen. Die ANF Transformation macht aus TamedFJ das letFJ
+
+- constraints nicht zu früh erwähnen
+	- informal erwähnen. um capture conversion zu behandeln braucht es neue constraints
+	- ganz vorne auflisten. Capture Conversion ist eine Neuheit
+
+Figure 4 und 5 in ein Bild
+ - man könnte die syntax unterlegen und sagen die unterlegten elemente fallen weg
+ - in beiden Syntaxen die Methodendeklarationen sollen gleich sein. beides return benutzen
+	- anschließend bei der convertierung zu TamedFJ nur die Änderungen beschreiben (Änderungen nur in Expressions)

typeinference.tex

@@ -0,0 +1,416 @@
+
+\section{Global Type Inference Algorithm}
+\label{sec:glob-type-infer}
+
+This section gives an overview of the global type inference algorithm
+with examples and identifies the challenges that we had to overcome in
+the design of the algorithm.
+
+\begin{figure}[h]
+\begin{minipage}{0.49\textwidth}
+\begin{lstlisting}[style=tfgj, caption=Valid Java program, label=lst:addExample]
+<A> List<A> add(List<A> l, A v)
+
+List<? super String> l = ...;
+add(l, "String");
+\end{lstlisting}
+\end{minipage}\hfill
+\begin{minipage}{0.49\textwidth}
+\begin{lstlisting}[style=tamedfj, caption=\TamedFJ{} representation, label=lst:addExampleLet]
+<A> List<A> add(List<A> l, A v)
+List<? super String> l = ...;
+let v:(*@$\tv{v}$@*) = l
+    in add(v, "String");
+\end{lstlisting}
+\end{minipage}\\
+\begin{minipage}{0.49\textwidth}
+\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:addExampleCons]
+(*@$\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}} \lessdot \tv{v}$@*)
+(*@$\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$@*)
+(*@$\type{String} \lessdot \wtv{a}$@*)
+\end{lstlisting}
+\end{minipage}\hfill
+\begin{minipage}{0.49\textwidth}
+\begin{lstlisting}[style=tamedfj, caption=Type solution, label=lst:addExampleSolution]
+<A> List<A> add(List<A> l, A v)
+List<? super String> l = ...;
+let l2:(*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = l
+    in <X>add(l2, "String");
+\end{lstlisting}
+\end{minipage}
+\end{figure}
+
+% \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}
+
+%Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
+Listings~\ref{lst:addExample}, \ref{lst:addExampleLet}, \ref{lst:addExampleCons}, and
+\ref{lst:addExampleSolution} showcase the global type inference algorithm step by step.
+Note that regular Java code snippets are displayed in a grey box, \TamedFJ{} programs are yellow
+and constraints have a red background.
+%This example is fully typed except for the method call \texttt{add} missing its type parameters.
+In the Java code in Listing~\ref{lst:addExample}, the type of variable
+\texttt{l} is an existential type so that it has to undergo a capture conversion
+before being passed to a method call.
+To this end we convert the program to A-Normal form (Listing~\ref{lst:addExampleLet}),
+which introduces a let statement defining a new variable \texttt{v}.
+The constraint generation step also assigns type placeholders to all variables missing a type annotation.
+%In this case the variable \texttt{v} gets the type placeholder $\tv{v}$ (also shown in listing \ref{lst:addExampleCons})
+%during the constraint generation step.
+In this case the algorithm puts the type
+placeholder $\tv{v}$ for the type of \texttt{v} before generating constraints (see Listing~\ref{lst:addExampleCons}).
+These constraints mirror the typing rules of the \TamedFJ{} calculus (section~\ref{sec:tifj}).
+% During the constraint generation step the type of the variable \texttt{v} is unknown
+% and given the type placeholder $\tv{v}$.
+The call to \texttt{add} generates the \emph{capture constraint} $\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$.
+This constraint ($\lessdotCC$) is a kind of subtype constraint, which additionally
+expresses that the left side of the constraint is subject to a capture conversion.
+Next, the unification algorithm \unify{} (section~\ref{sec:unify}) solves the constraints.
+Havin the constraints in listing \ref{lst:addExampleCons} as an input \unify{} changes the constraint
+$\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}} \lessdot \tv{v}$
+to $\tv{v} \doteq \wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$
+therby finding a type solution for $\tv{v}$.
+Afterwards every occurence of $\tv{v}$ in the constraint set is replaced by $\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$
+leaving us with the following constraints which are now subject to a capture conversion by the \unify{} algorithm:
+% Initially, no type is assigned to $\tv{v}$.
+% % During the course of \unify{} more and more types emerge.
+% As soon as a concrete type for $\tv{v}$ is appears during constraint
+% solving,  \unify{} can conduct a capture conversion if needed.
+% %The constraints where this is possible are marked as capture constraints.
+% In this example, $\tv{v}$ will be set to
+% $\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$
+% leaving us with the following constraints: 
+
+\begin{displaymath}
+\prftree[r]{Capture}{
+\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}, \, \type{String} \lessdotCC \wtv{a}
+}{
+\wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
+}
+\end{displaymath}
+
+%Capture Constraints $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ allow for a capture conversion,
+%which converts a constraint of the form $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ to $(\exptype{C}{\rwildcard{X}} \lessdot \type{T})$
+The constraint $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$
+allows \unify{} to do a capture conversion to $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
+The captured wildcard $\rwildcard{X}$ gets a fresh name \texttt{Y}, which is stored in the wildcard environment of the \unify{} algorithm.
+Substituting \texttt{Y} for $\wtv{a}$ yields the constraints almost
+solved: $\exptype{List}{\rwildcard{Y}} \lessdot
+\exptype{List}{\rwildcard{Y}}$, $\type{String} \lessdot
+\rwildcard{Y}$. 
+The first constraint is obviously satisfied and $\type{String} \lessdot \rwildcard{Y}$ is satisfied
+because $\rwildcard{Y}$ has $\type{String}$ as lower bound.
+
+
+A correct Featherweight Java program including all type annotations and an explicit capture conversion via let statement is shown in Listing \ref{lst:addExampleSolution}.
+This program can be deduced from the solution of the \unify{} algorithm.% presented in Section~\ref{sec:unify}.
+In the body of the let statement the type $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$
+becomes $\exptype{List}{\rwildcard{X}}$ and the capture converted wildcard $\wildcard{X}{\type{Object}}{\type{String}}$ can be used as
+a type parameter of the call \texttt{<X>add(v, "String")}.
+
+% The input to our type inference algorithm is a modified version of the calculus in \cite{WildcardsNeedWitnessProtection} (see chapter \ref{sec:tifj}).
+% First \fjtype{} (see section \ref{chapter:constraintGeneration}) generates constraints
+% and afterwards \unify{} (section \ref{sec: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})$.
+% \textit{Note:} a type $\type{T}$ can either be a named type, a type placeholder or a wildcard type placeholder.
+% 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}{\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.
+
+% The central piece of this type inference algorithm, the \unify{} process, is described with implication rules (chapter \ref{sec:unify}).
+% We try to keep the branching at a minimal amount to improve runtime behavior.
+% Also the transformation steps of the \unify{} algorithm are directly related to the subtyping rules of our calculus.
+% There are no informal parts in our \unify{} algorithm.
+% It solely consist out of transformation rules which are bound to simple checks.
+
+\subsection{Notes on Capture Constraints}
+Capture constraints must be stored in a multiset so that it is possible that two syntactically equal constraints remain in the same set.
+The equality relation on Capture constraints is not reflexive.
+
+Capture Constraints are bound to a variable.
+For example a let statement like \lstinline{let x = v in x.get()} will create the capture constraint
+$\tv{x} \lessdotCC_x \exptype{List}{\wtv{a}}$.
+This time we annotated the capture constraint with an $x$ to show its relation to the variable \texttt{x}.
+Let's do the same with the constraints generated by the \texttt{concat} method invocation in listing \ref{lst:faultyConcat},
+creating the constraints \ref{lst:sameConstraints}.
+
+\begin{figure}
+  \begin{minipage}[t]{0.49\textwidth}
+    \begin{lstlisting}[caption=Faulty Method Call,label=lst:faultyConcat,style=TamedFJ]{tamedfj}
+  List<?> v = ...;
+  
+  let x = v in 
+      let y = v in
+        concat(x, y) // Error!
+    \end{lstlisting}\end{minipage}
+    \hfill
+    \begin{minipage}[t]{0.49\textwidth}
+  \begin{lstlisting}[caption=Annotated constraints,mathescape=true,style=constraints,label=lst:sameConstraints]
+  $\tv{x} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{x}$
+  $\tv{y} \lessdotCC_\texttt{y} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{y}$
+    \end{lstlisting}
+    \end{minipage}
+\end{figure}
+
+
+During the \unify{} process it could happen that two syntactically equal capture constraints evolve,
+but they are not the same because they are each linked to a different let introduced variable.
+In this example this happens when we substitute $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\tv{x}$ and $\tv{y}$
+resulting in:
+%For example by substituting $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{x}]$ and $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{y}]$:
+\begin{displaymath}
+  \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_x \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_y \exptype{List}{\wtv{a}}
+\end{displaymath}
+Thanks to the original annotations we can still see that those are different constraints.
+After \unify{} uses the \rulename{Capture} rule on those constraints
+it gets obvious that this constraint set is unsolvable:
+\begin{displaymath}
+  \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}},
+\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}
+\end{displaymath}
+
+%In this paper we do not annotate capture constraint with their source let statement.
+This paper will not annotate capture constraints with variable names.
+Instead we consider every capture constraint as distinct to other capture constraints even when syntactically the same,
+because we know that each of them originates from a different let statement.
+\textit{Hint:} An implementation of this algorithm has to consider that seemingly equal capture constraints are actually not the same
+and has to allow doubles in the constraint set.
+
+% %We see the equality relation on Capture constraints is not reflexive.
+% A capture constraint is never equal to another capture constraint even when structurally the same
+% ($\type{T} \lessdotCC \type{S} \neq \type{T} \lessdotCC \type{S}$).
+% This is necessary to solve challenge \ref{challenge:1}.
+% A capture constraint is bound to a specific let statement.
+
+\textit{Note:}
+In the special case \lstinline{let x = v in concat(x,x)} the constraints would look like
+$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}},
+\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
+and we could actually delete one of them without loosing information.
+But this case will never occur in our algorithm, because the let
+statements for our input programs are generated by transformation to ANF (see \ref{sec:anfTransformation}).
+
+
+\subsection{Challenges}\label{challenges}
+%TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
+
+% Wildcards are not reflexive.
+% ( on the equals property ), every wildcard has to be capture converted when leaving its scope
+
+% do not substitute free type variables
+
+Global type inference for Featherweight Generic Java without wildcards
+has been considered elsewher \cite{TIforFGJ}.
+Adding wildcards to the calculus created new problems, which have not
+been recognized by existing work on type unification for Java with wildcards~\cite{plue09_1}.
+% what is the problem?
+% Java does invisible capture conversion steps 
+Java's wildcard types are represented as existential types that have to be opened before they can be used.
+Opening can either be done implicitly
+(\cite{aModelForJavaWithWildcards}, \cite{javaTIisBroken}) or
+explicitly via a let statement (\cite{WildcardsNeedWitnessProtection}).
+For all variations it is vital to know the argument types with which a method is called.
+In the absence of type annotations,
+we do not know where an existential type will emerge and where a capture conversion is necessary.
+Rather, the type inference algorithm has to figure out the placement
+of existentials.
+We identified three main challenges related to Java wildcards and global type inference.
+\begin{enumerate}
+\item \label{challenge:1}
+One challenge is to design the algorithm in a way that it finds a
+correct solution for programs like the one shown in Listing~\ref{lst:addExample}
+and rejects programs like the one in Listing~\ref{lst:concatError}.
+The first one is a valid Java program,
+because the type \texttt{List<? super String>} is \textit{capture converted} to a fresh type variable $\rwildcard{X}$
+which is used as the generic method parameter for the call to \texttt{add} as shown in Listing~\ref{lst:addExampleLet}.
+Because we know that the type \texttt{String} is a subtype of the free variable $\rwildcard{X}$,
+it is safe to pass \texttt{"String"} for the first parameter of the function.
+
+The second program shown in Listing~\ref{lst:concatError} is incorrect.
+The method call to \texttt{concat} with two wildcard lists is unsound.
+The element types of the lists may be unrelated, therefore the call to \texttt{concat} cannot succeed.
+The problem gets apparent if we try to write the \texttt{concat}
+method call in the \TamedFJ{} calculus
+(Listing~\ref{lst:concatTamedFJ}): 
+\texttt{l1'} and \texttt{l2'} are two different lists inside the body of the let statements, namely
+$\exptype{List}{\rwildcard{X}}$ and $\exptype{List}{\rwildcard{Y}}$.
+For the method call \texttt{concat(x1, x2)} no replacement for the generic \texttt{A}
+exists to satisfy
+$\exptype{List}{\type{A}} <: \exptype{List}{\type{X}},
+\exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$.
+
+% \textbf{Solution:}
+% Capture Conversion during Unify.
+
+% \item 
+% \unify{} transforms a constraint set into a correct type solution by
+% gradually assigning types to type placeholders during that process.
+% Solved constraints are removed and never considered again.
+% In the following example, \unify{} solves the constraint generated by the expression
+% \texttt{l.add(l.head())} first, which results in $\ntv{l} \lessdot \exptype{List}{\wtv{a}}$.
+% \begin{verbatim}
+% anyList() = new List<String>() :? new List<Integer>()
+
+% add(anyList(), anyList().head());
+% \end{verbatim}
+% The type for \texttt{l} can be an arbitrary list, but it has to be a invariant one.
+% Assigning a \texttt{List<?>} for \texttt{l} is unsound, because the type list hiding behind
+% \texttt{List<?>} could be a different one for the \texttt{add} call than the \texttt{head} method call.
+% An additional constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
+% is solved by removing the wildcard $\rwildcard{X}$ if possible.
+
+% This problem is solved by ANF transformation
+
+\item
+% This problem is solved by assuming everything is a wildcard and lateron erasing excessive wildcards
+% this is solved by having wildcards bound to a type. But this makes it necessary to remove wildcards lateron otherwise Unify would have to backtrack
+The program in Listing~\ref{shuffleExample} exhibits a challenge involving wildcards and subtyping.
+The method call \texttt{shuffle(l)} is incorrect, because \texttt{l} has type
+$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ representing a list of unknown lists.
+However, $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ is a subtype of
+$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ which represents a list of lists, all of the same type $\rwildcard{X}$,
+and can be passed safely to \texttt{shuffle}.
+This behavior can also be explained by looking at the types and their capture converted versions:
+\begin{center}
+\begin{tabular}{l | l | l}
+Java type & \TamedFJ{} representation & Capture Conversion \\
+\hline
+$\exptype{List}{\exptype{List}{\texttt{?}}}$ & $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ & $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ \\
+$\exptype{List2D}{\texttt{?}}$ & $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ & $\exptype{List2D}{\rwildcard{X}}$ \\
+%Supertype of $\exptype{List2D}{\texttt{?}}$ & $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ & $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ \\
+\end{tabular}
+\end{center}
+%The direct supertype of $\exptype{List2D}{\rwildcard{X}}$ is $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
+%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}
+%can emerge, which have no equivalent in the Java syntax.
+
+\begin{lstlisting}[style=java,label=shuffleExample,caption=Intermediate Types Example]
+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{lstlisting}
+% 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=TamedFJ]
+% let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in <X>shuffle(l2d')
+% \end{lstlisting}
+
+% For the example shown in listing \ref{shuffleExample} the method call \texttt{shuffle(l2d)} creates the constraints:
+% \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}
+
+Given such a program the type inference algorithm has to allow the call \texttt{shuffle(l2d)} and
+decline the call to \texttt{shuffle(l)}.
+
+% The method call \texttt{shuffle(l)} is invalid however,
+% because \texttt{l} has the type
+% $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
+% There is no solution for the subtype constraint:
+% $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$
+
+\item \label{challenge3}
+% \textbf{Free variables cannot leave their scope}:
+% Let's assume we have a variable \texttt{ls} with type $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$
+% %When calling the \texttt{id} function with an element of this list we have to apply capture conversion.
+% and the following program:
+
+% \noindent
+% \begin{minipage}{0.62\textwidth}
+% \begin{lstlisting}
+% let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = ls.get(0) in id(x) : (*@$\ntv{z}$@*)
+% \end{lstlisting}\end{minipage}
+%   \hfill
+% \begin{minipage}{0.36\textwidth}
+%   \begin{lstlisting}[style=constraints]
+% (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$@*),
+% (*@$\exptype{List}{\wtv{x}} \lessdot \ntv{z},$@*)
+%   \end{lstlisting}
+% \end{minipage}
+% % the variable z must not contain free variables (TODO)
+
+Take the Java program in listing \ref{lst:mapExample} for example.
+It uses map to apply a polymorphic method \texttt{id} to every element of a list
+$\expr{l} :
+\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$. 
+
+How do we get the \unify{} algorithm to determine the correct type for the
+variable \expr{l2}?
+Although we do not specify constraint generation for language constructs like
+lambda expressions used in this example,
+we can imagine that the constraints have to look like in Listing~\ref{lst:mapExampleCons}.
+
+\begin{minipage}{0.45\textwidth}
+\begin{lstlisting}[caption=List Map Example,label=lst:mapExample]
+<X> List<X> id(List<X> l){ ... }
+List<List<?>> ls;
+l2 = l.map(x -> id(x));
+\end{lstlisting}\end{minipage}
+\hfill
+\begin{minipage}{0.45\textwidth}
+\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:mapExampleCons]
+(*@$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}}$@*)
+(*@$\exptype{List}{\wtv{x}} \lessdot \tv{z},$@*)
+(*@$\exptype{List}{\tv{z}} \lessdot \tv{l2}$@*)
+\end{lstlisting}
+\end{minipage}
+
+The constraints
+$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}},
+\exptype{List}{\wtv{x}} \lessdot \tv{z}$
+stem from the body of the lambda expression
+\texttt{id(x)}.
+\textit{For clarification:} This method call would be represented as the following expression in \TamedFJ{}:
+
+\texttt{let x1 :$\wctype{\rwildcard{A}}{List}{\rwildcard{A}}$ = x in id(x) :$\tv{z}$}
+
+The T-Let rule prevents us from using free variables created by the method call to \expr{id}
+to be used in the return type $\tv{z}$.
+But this restriction has to be communicated to the \unify{} algorithm,
+which does not know about the origin and context of 
+the constraints.
+If we naively substitute $\sigma(\tv{z}) = \exptype{List}{\rwildcard{A}}$
+the return type of the \texttt{map} function would be the type
+$\exptype{List}{\exptype{List}{\rwildcard{A}}}$, which would be unsound.
+
+% The type of \expr{l2} is the same as the one of \expr{l}:
+% $\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$
+
+% \textbf{Solution:}
+% We solve this issue by distinguishing between wildcard placeholders
+% and normal placeholders and introducing them as needed.
+% $\ntv{z}$ is a normal placeholder and is not allowed to contain free variables.
+\end{enumerate}