Comments

.gitignore

@@ -17,7 +17,3 @@
 *-blx.aux
 *-blx.bib
 *.run.xml
-*.vtc
-*.synctex.gz
-auto
-_region_.tex

TIforWildFJ.tex

@@ -1,5 +1,5 @@
 
-\documentclass[anonymous,USenglish]{llncs}
+\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate]{lipics-v2021}
 %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,28 +40,30 @@
 
 \input{prolog}
 
-\begin{document}
 \bibliographystyle{plainurl}% the mandatory bibstyle
 
 \title{Global Type Inference for Featherweight Java with Wildcards} %TODO Please add
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%% ANON
+%\titlerunning{Dummy short title} %TODO optional, please use if title is longer than one line
 
-% \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{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.
 
-% \authorrunning{A. Stadelmeier and M. Plümicke and P. Thiemann}
+\author{Martin Plümicke}{DHBW Stuttgart, Campus Horb, Germany}{pl@dhbw.de}{}{}
 
-%% END ANON
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\author{Peter Thiemann}{Universität Freiburg, Institut für Informatik, Germany}{thiemann@informatik.uni-freiburg.de}{}{}
 
-%\category{} %optional, e.g. invited paper
+\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.'
 
-%\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
+\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/
+
+\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, ...
@@ -75,36 +77,28 @@
 
 
 
-% %Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% \EventEditors{John Q. Open and Joan R. Access}
-% \EventNoEds{2}
-% \EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
-% \EventShortTitle{CVIT 2016}
-% \EventAcronym{CVIT}
-% \EventYear{2016}
-% \EventDate{December 24--27, 2016}
-% \EventLocation{Little Whinging, United Kingdom}
-% \EventLogo{}
-% \SeriesVolume{42}
-% \ArticleNo{23}
-% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\EventEditors{John Q. Open and Joan R. Access}
+\EventNoEds{2}
+\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
+\EventShortTitle{CVIT 2016}
+\EventAcronym{CVIT}
+\EventYear{2016}
+\EventDate{December 24--27, 2016}
+\EventLocation{Little Whinging, United Kingdom}
+\EventLogo{}
+\SeriesVolume{42}
+\ArticleNo{23}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+\begin{document}
 
 \maketitle
 
 %TODO mandatory: add short abstract of the document
 \begin{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.
+TODO: Abstract
 \end{abstract}
-\keywords{type inference, Java, subtyping, generics} %TODO mandatory; please add comma-separated list of keywords
 
 \input{introduction}
 
@@ -112,26 +106,50 @@
 
 \input{tRules}
 
-\input{typeinference}
-
 %\input{tiRules}
 
 \input{constraints}
 
 \input{Unify}
 
-\include{relatedwork}
+\section{Limitations}
+
+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,138 +1,11 @@
-%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}).
-Additionally we could prove that type solutions generated by our type inference algorithm are correct respective to \TamedFJ{}'s type rules.
-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.
+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
+type solutions for programs involving wildcards.
 
-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 proof soundness and completeness for \unify{}.
 
-%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,5 +1,7 @@
-
 \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.
+
 % 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.
@@ -12,99 +14,26 @@
 % 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
 
 The constraint generation works on the \TamedFJ{} language.
-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.
+This step is mostly same as in \cite{TIforFGJ} except for field access and method invocation.
+We will focus on those parts.
+Here the new capture constraints and wildcard type placeholders are introduced.
 
-%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]
+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.
+\begin{verbatim}
 m(l, v){
-    return l.add(v);
+  let x = x in x.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}
+\end{verbatim}
 
-\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}
+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.
 
-\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}
-
-\subsection{Constraint Generation Algorithm}
-% 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.
@@ -113,12 +42,25 @@ 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}}}$.
 
-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.
+Type variables declared in the class header are passed to \unify{}.
 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
@@ -126,37 +68,42 @@ Those type variables count as regular types and can be held by normal type place
 
 %NO equals constraints during the constraint generation step!
 \begin{figure}[tp]
-  \center
-\begin{tabular}{lcll}
-    $C $ &$::=$ &$\overline{c}$ & Constraint set \\
-    $c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \lessdotCC \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
-    $\type{T}, \type{U}, \type{L} $ & $::=$ & $\tv{a} \mid \gtype{G}$ & Type placeholder or Type \\
-    $\tv{a}$ & $::=$ & $\ntv{a} \mid \wtv{a}$ & Normal and wildcard type placeholder \\
-    $\gtype{G}$ & $::=$ & $\type{X} \mid \ntype{N}$ & Wildcard, or Class Type \\
-    $\ntype{N}, \ntype{S}$ & $::=$ & $\wctype{\triangle}{C}{\ol{T}} $ & Class Type \\
-    $\triangle$ & $::=$ & $\overline{\wtype{W}}$ & Wildcard Environment \\
-    $\wtype{W}$ & $::=$ & $\wildcard{X}{U}{L}$ & Wildcard \\
-\end{tabular}
-  \caption{Syntax of types and constraints used by \fjtype{} and \unify{}}
+  \begin{align*}
+    % Type
+    \type{T}, \type{U} &::= \tv{a} \mid \wtv{a} \mid \mv{X} \mid {\wcNtype{\Delta}{N}} && \text{types and type placeholders}\\
+    \type{N} &::= \exptype{C}{\ol{T}} && \text{class type (with type variables)} \\
+    % Constraints
+    \constraint &::= \type{T} \lessdot \type{U} \mid \type{T} \lessdotCC \type{U} && \text{Constraint}\\
+    \consSet &::= \set{\constraints} && \text{constraint set}\\
+    % Method assumptions:
+    \methodAssumption &::= \texttt{m} : \exptype{}{\ol{Y}
+                        \triangleleft \ol{P}}\ \ol{\type{T}} \to \type{T}  &&
+                                                                \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}{\overline{\type{X} \triangleleft \type{N}}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\
+      \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\ol{X} \triangleleft \ol{N}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\
               & \begin{array}{ll@{}l}
 \textbf{let} & \ol{\methodAssumption} =
                 \set{ \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \mid
                   \set{ \mv{m}(\ol{x}) = \expr{e} } \in \ol{M}, \, \tv{a}, \ol{\tv{a}}\ \text{fresh} } \\
-              & \Delta = \set{ \overline{\wildcard{X}{\type{N}}{\bot}} } \\
-              & C = \begin{array}[t]{l}
+              \textbf{in} 
+                  & \begin{array}[t]{l}
                 \set{ \typeExpr(\mtypeEnvironment \cup \ol{\methodAssumption} \cup \set{\mv{this} :
               \exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}} }, \texttt{e}, \tv{a})
                \\ \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}}
-                  \end{array} \\
-              \textbf{in} 
-                  & (\Delta, C)
+                  \end{array}
                 \end{array}
     \end{array}
   \end{gather*}
@@ -166,16 +113,16 @@ Those type variables count as regular types and can be held by normal type place
 
 \begin{displaymath}
   \begin{array}{@{}l@{}l}
-    \typeExpr{} &({\mtypeEnvironment}, \Gamma , \texttt{e}.\texttt{f}, \tv{a}) = \\
+    \typeExpr{} &({\mtypeEnvironment} , \texttt{e}.\texttt{f}, \tv{a}) = \\
                 & \begin{array}{ll}
                     \textbf{let} 
                     & \tv{r} \ \text{fresh} \\
-                    & \consSet_R = \typeExpr({\mtypeEnvironment}, \Gamma, \texttt{e}, \tv{r})\\
+                    & \consSet_R = \typeExpr({\mtypeEnvironment}, \texttt{e}, \tv{r})\\
                     & \constraint = \begin{array}[t]{@{}l@{}l}
                       \orCons\set{
                       \set{ &
                       \tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}} ,
-                      \tv{a} \doteq [\overline{\wtv{a}}/\ol{X}]\type{T},
+                      [\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} ,
                       \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}
@@ -189,12 +136,12 @@ Those type variables count as regular types and can be held by normal type place
 
 \begin{displaymath}
   \begin{array}{@{}l@{}l}
-    \typeExpr{} &({\mtypeEnvironment}, \Gamma , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2, \tv{a}) = \\
+    \typeExpr{} &({\mtypeEnvironment} , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2, \tv{a}) = \\
                 & \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)\\
+                    & \consSet_1 = \typeExpr({\mtypeEnvironment}, \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}
@@ -207,7 +154,7 @@ Those type variables count as regular types and can be held by normal type place
 
 \begin{displaymath}
   \begin{array}{@{}l@{}l}
-      \typeExpr{} & ({\mtypeEnvironment}, \Gamma , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\
+      \typeExpr{} & ({\mtypeEnvironment} , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\
       & \begin{array}{ll}
       \textbf{let}
       & \tv{r}, \ol{\tv{r}} \text{ fresh} \\
@@ -217,55 +164,16 @@ Those type variables count as regular types and can be held by normal type place
       \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T}) \\
       & \mathbf{where}\ \begin{array}[t]{l}
         \expr{v}, \ol{v} : \ol{S} \in \localVarAssumption \\
-        \texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T} \in {\mtypeEnvironment }
+        \texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T} \in {\mtypeEnvironment}
       \end{array}
                     
       \end{array}
       \end{array}
   \end{displaymath}
-
-\begin{displaymath}
-  \begin{array}{@{}l@{}l}
-    \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}, \Gamma, e_1, \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}}}
-                  \end{array} 
-  \end{array}
-\end{displaymath}
-
-%We could skip wfresh here:
-\begin{displaymath}
-  \begin{array}{@{}l@{}l}
-    \typeExpr{} &({\mtypeEnvironment}, \Gamma , x, \tv{a}) = 
-    \mtypeEnvironment(x)
-  \end{array}
-\end{displaymath}
-
-\begin{displaymath}
-  \begin{array}{@{}l@{}l}
-    \typeExpr{} &({\mtypeEnvironment}, \Gamma , \texttt{new}\ \type{C}(\overline{e}), \tv{a}) = \\
-                & \begin{array}{ll}
-                    \textbf{let} 
-                    & \ol{\ntv{r}}, \ol{\ntv{a}} \ \text{fresh} \\
-                    & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \Gamma, \overline{e}, \ol{\ntv{r}}) \\
-                    & 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{\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]
+\textbf{Example:}
+\begin{verbatim}
 class Class1{
   <A> A head(List<X> l){ ... }
   List<? extends String> get() { ... }
@@ -276,7 +184,7 @@ class Class2{
     return c1.head(c1.get());
   }
 }
-\end{lstlisting}
+\end{verbatim}
 %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:
@@ -292,8 +200,7 @@ leading to the following type annotations:
 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{minipage}{0.45\textwidth}
   \begin{lstlisting}[style=tamedfj]
 class Class2 {
   example(c1) = let x = c1 in
@@ -302,33 +209,42 @@ class Class2 {
 \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}
+      \begin{minipage}{0.5\textwidth}
+\begin{constraintset}
+$
+    \begin{array}{l}
+      \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{array}
+$
+  \end{constraintset}
 \end{minipage}
 
 Following is a possible solution for the given constraint set:
 
-\noindent
 \begin{minipage}{0.55\textwidth}
-  \begin{lstlisting}[style=tamedfj]
+  \begin{lstlisting}[style=letfj]
 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);
+  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}
+      \begin{minipage}{0.4\textwidth}
+\begin{constraintset}
+$
+    \begin{array}{l}
+    \sigma(\ntv{x}) = \type{Class1} \\
+    %\tv{xp} \lessdot \exptype{List}{\wtv{x}}, \\
+    %\exptype{List}{\type{String}} \lessdot \tv{p1}, \\
+    \sigma(\tv{xp}) = \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \\
+    \end{array}
+$
+  \end{constraintset}
 \end{minipage}
 
 For $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$ to be a correct solution for $\tv{xp}$
@@ -338,7 +254,6 @@ 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.
@@ -348,183 +263,43 @@ 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}
+\begin{displaymath}
+  \begin{array}{@{}l@{}l}
+    \typeExpr{} &({\mtypeEnvironment} , 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_2 = \typeExpr({\mtypeEnvironment}, 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}}}
+                  \end{array} 
+  \end{array}
+\end{displaymath}
 
-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.
+%We could skip wfresh here:
+\begin{displaymath}
+  \begin{array}{@{}l@{}l}
+    \typeExpr{} &({\mtypeEnvironment} , x, \tv{a}) = 
+    \mtypeEnvironment(x)
+  \end{array}
+\end{displaymath}
 
-\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}
+\begin{displaymath}
+  \begin{array}{@{}l@{}l}
+    \typeExpr{} &({\mtypeEnvironment} , \texttt{new}\ \type{C}(\overline{e}), \tv{a}) = \\
+                & \begin{array}{ll}
+                    \textbf{let} 
+                    & \ol{\tv{r}} \ \text{fresh} \\
+                    & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \overline{e}, \ol{\tv{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}} \\
+                    {\mathbf{in}} & {
+                    \overline{\consSet} \cup
+                        \set{\tv{a} \doteq \exptype{C}{\ol{a}}}}
+                  \end{array} 
+  \end{array}
+\end{displaymath}
 
 % Problem:
 % <X, A extends List<X>> void t2(List<A> l){}
@@ -608,8 +383,4 @@ The Or-Cons rule considers multiple declarations of the same method separately a
 %  \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
 % \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:
+% \end{displaymath}

helpers.tex

@@ -1,34 +0,0 @@
-
-\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}

martin.bib

@@ -50,8 +50,6 @@ 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},
@@ -67,39 +65,14 @@ keywords = {subtyping, type inference, principal types}
     pages={23-41},
     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 = {Martelli, Alberto and Montanari, Ugo},
-title = {An Efficient Unification Algorithm},
-year = {1982},
-issue_date = {April 1982},
-publisher = {Association for Computing Machinery},
-address = {New York, NY, USA},
-volume = {4},
-number = {2},
-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}
-}
+    author={A. Martelli and U. Montanari},
+    title={An Efficient Unification Algorithm},
+    journal={ACM Transactions on Programming Languages and Systems},
+    volume={4},
+    pages={258-282},
+    year={1982}}
 
 @InProceedings{Plue07_3,
   author = 	 {Martin Pl{\"u}micke},
@@ -353,14 +326,6 @@ 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}},
@@ -387,16 +352,6 @@ doi = {10.1145/2983990.2984004}
   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},
@@ -433,7 +388,7 @@ numpages = {14},
 keywords = {existential types, joins, parametric types, single-instantiation inheritance, subtyping, type inference, wildcards}
 }
 
-@inproceedings{javaTIisBroken,
+@inproceedings{10.1145/1449764.1449804,
 author = {Smith, Daniel and Cartwright, Robert},
 title = {Java type inference is broken: can we fix it?},
 year = {2008},
@@ -511,61 +466,3 @@ keywords = {Compilation, Java, generic classes, language design, language semant
   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,6 +1,5 @@
 \usepackage{xspace}
 \usepackage{color,ulem}
-\usepackage{mathpartir}
 \usepackage{listings}
 \lstset{language=Java,
   showspaces=false,
@@ -12,21 +11,14 @@
   escapeinside={(*@}{@*)},
   captionpos=t,float,abovecaptionskip=-\medskipamount
 }
-
 \lstdefinestyle{fgj}{backgroundcolor=\color{lime!20}}
 \lstdefinestyle{tfgj}{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}
@@ -79,9 +71,6 @@
 \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}
 
@@ -108,8 +97,7 @@
 \newcommand{\constraints}{\ensuremath{\mathit{\overline{c}}}}
 \newcommand{\itype}[1]{\ensuremath{\mathit{#1}}}
 \newcommand{\il}[1]{\ensuremath{\overline{\itype{#1}}}}
-\newcommand{\gtype}[1]{\type{#1}}
-\newcommand{\type}[1]{\ensuremath{\mathtt{#1}}}
+\newcommand{\type}[1]{\mathtt{#1}}
 \newcommand{\anyType}[1]{\mathit{#1}}
 \newcommand{\gType}[1]{\texttt{#1}}
 \newcommand{\mtypeEnvironment}{\ensuremath{\Pi}}
@@ -117,7 +105,7 @@
 \newcommand{\localVarAssumption}{\ensuremath{\mathtt{\eta}}}
 \newcommand{\expandLB}{\textit{expandLB}}
 
-\newcommand{\letfj}{\textbf{LetFJ}}
+\newcommand{\letfj}{\emph{LetFJ}}
 \newcommand{\tph}{\text{tph}}
 
 \newcommand{\expr}[1]{\texttt{#1}}
@@ -133,9 +121,8 @@
 \newcommand{\wtypestore}[3]{\ensuremath{#1 = \wtype{#2}{#3}}}
 %\newcommand{\wtype}[2]{\ensuremath{[#1\ #2]}}
 \newcommand{\wtv}[1]{\ensuremath{\tv{#1}_?}}
-\newcommand{\cctv}[1]{\ensuremath{\tv{#1}_!}}
-\newcommand{\ntv}[1]{\ensuremath{\underline{\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}_?}}

rebuttal.md

@@ -1,11 +0,0 @@
-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

@@ -1,76 +0,0 @@
-
-\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,216 +1,237 @@
 \section{Soundness}
 
-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.
+\newcommand{\CC}{\text{CC}}
 
-\unify{} calculates solutions for all normal type placeholders.
-Those are used for all untyped method's argument and return type.
-A correct typing for method calls can be deducted from those type informations.
-
-\begin{lemma}{Soundness:}\label{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}) = (\Delta', C)$
-    \item[then] $\Delta|\Gamma  \vdash \texttt{e} : \sigma(\tv{a})$ where $\Delta = \Delta_u \cup \Delta'$
-    \end{description}
-\end{lemma}
-\textit{Proof:}
-By structural induction over the expression $\texttt{e}$. 
+\begin{lemma}
+A sound TypelessFJ program is also sound under LetFJ type rules.
 \begin{description}
-    \item[$\texttt{let}\ \texttt{x} = \texttt{t}_1 \ \texttt{in}\ \expr{t}_2$]
-    $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ by lemma \ref{lemma:wildcardWellFormedness}.
-    $\Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok$ by lemma \ref{lemma:unifyWellFormedness}.
-        $\Delta|\Gamma \vdash \expr{t}_1: \sigma(\tv{e}_1)$ by assumption.
-        $\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}
+    \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}
 
-%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})$.
+TODO: Beforehand we have to show that $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$
+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 
 
-\item[$\text{let}\ \expr{x} = \expr{e} \ \text{in}\ 
-\text{let}\ \overline{\expr{x} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x})$]
-generates constraints $\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}},
-\tv{r} \lessdot \tv{a}, \ol{\tv{x}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{r}, \ol{\wtv{b}} \lessdot \ol{N}$.
-%We need to proof $\text{let}\ \expr{x} : \wcNtype{\Delta'}{N} = \expr{e}, \,
-%\overline{\expr{x} : \wcNtype{\Delta'}{N} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x}) : \type{T}_2$
-%where $\sigma(\tv{x}) = \wcNtype{\Delta'}{N}$, $\sigma(\ol{\tv{x}}) = \ol{\wcNtype{\Delta'}{N}}$,  $\sigma(\tv{a}) = \type{T}_2$.
-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.
-        
-        % 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> Box<X> empty()
+same(Box<?>, empty())
+let p1 : X.Box<X> = Box<?> in let 
+X.Box<X> <. Box<x> 
+Box<e> <. Box<x>
 
-% $\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})$
+boxin(empty()), Box2<?>
 
-% %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
+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 
 
-% %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}$.
+<X,Y> void same(Pair<X,Y> a, Pair<X,Y> b){}
+<X> Pair<?, X> left() { return null; }
+<X> Pair<X, ?> right() { return null; }
 
-%     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}$.
+<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
 
-%     % \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}
+let left : X,Y.Pair<X,Y> = left() in
+ let right : Pair<X,Y> = right() in
 
-% Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$).
+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}
 
 
-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.
+\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.
 
-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 
+\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}{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'$.
+\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$
+    and $(\Delta_u, \sigma) = \unify{}(\Delta', C)$ and let $\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}
-\textit{Proof:} This is due to free variables only travel inbetween constraints and themselves via substitution.
+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.
 
-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.
+%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
 
-% \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')$
+% Or is it possible to deduct the right \ol{S} directly from the types in the normal TPHs?
 
-% and $\text{wtv}(C') \cap \text{wtv}(C) = \emptyset$
-% and $\overline{\sigma(\tv{x}) = \wcNtype{\Delta}{N}}$
+\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}$,
+    then $\Delta|\Gamma  \vdash \texttt{e} : \wcNtype{\Delta_c}{N}$ by assumption.
+    $\Delta', \Delta, \Delta_c \vdash \type{N} <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise.
+    %Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$.
+    %Let $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) = \wcNtype{\Delta_t}{N_t}$.
+    
+    The completion of $|\texttt{e}.\texttt{f}|$ is $\texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f}$
+    
+    We now show
+    $\Delta|\Gamma \vdash \texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f} : \sigma(a)$
+    by the T-Field rule.
+    $\Delta \vdash \wcNtype{\Delta_c}{N} <: \wcNtype{\Delta_c}{N}$ by S-Refl.
+    $\Delta, \Delta_c \vdash \type{U}_i <: \sigma(\tv{a})$,
+    because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$ and lemma \ref{lemma:unifySoundness}.
+    $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$
+    and $\text{fv}(\type{U}_i) \subseteq \text{fv}(\type{N})$ by definition of $\textit{fields}$.
 
-% 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}
+    $\text{dom}(\Delta_c) \subseteq \text{fv}{\type{N}}$ by lemma \ref{lemma:tvsNoFV}.
+
+    % X.List<X> <. List<a?>
+    % $\sigma(\ol{\tv{r}}) = \overline{\wcNtype{\Delta}{N}}$,
+    % $\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
+    S typeinference:
+    T <: [S/Y]U
+    We apply the following lemma
+    Lemma
+    if T ok and T <: S then S ok
+
+    until
+    T = [S/Y]U
+
+    and then we can say by 
+    Lemma:
+    If [S/Y]U ok then S ok (TODO: proof!)
+
+    So we do not have to proof S ok (but T)
+
+    % T_r <: C<T> (S is in T)
+    % 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}
 
 % \begin{lemma} Unify does add free variables to types not containing free variables (or wildcard placeholders)
 % \begin{description}
@@ -251,47 +272,29 @@ 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)}
-% 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.
+\textit{Proof: (Variant 2)}
+The GenSigma and GenDelta rules check for well-formedness.
 
 % 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}
-%     Well-formedness is hereditary
-%     \begin{description}
-%         \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$
-%     \end{description}
-% \end{lemma}
-% \textit{Proof} by induction on subtyping rules in figure \ref{fig:subtyping}
+\begin{lemma}\label{lemma:wfHereditary}
+    Well-formedness is hereditary
+    \begin{description}
+        \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$
+    \end{description}
+\end{lemma}
+\textit{Proof:}
 
-% \begin{lemma}
+\begin{lemma}
     
-%     \begin{description}
-%         \item[If] $\Delta \vdash \wctype{\Delta'}{C}{\ol{T}} \ \ok$
-%         \item[Then] $\Delta, \Delta' \vdash \ok{T} \ \ok$
-%     \end{description}
-% \end{lemma}
-% \textit{Proof:} by definition of WF-Class
+    \begin{description}
+        \item[If] $\Delta \vdash \wctype{\Delta'}{C}{\ol{T}} \ \ok$
+        \item[Then] $\Delta, \Delta' \vdash \ok{T} \ \ok$
+    \end{description}
+\end{lemma}
+\textit{Proof:} by definition of WF-Class
 
 
 \begin{lemma} \label{lemma:tvsNoFV}
@@ -312,67 +315,34 @@ Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises.
 % Delta |-  N <. T
 % \end{lemma}
 
-% \begin{lemma}\label{lemma:wildcardsStayInScope}
-% Free variables can only hop to another constraint if they share the same wildcard placeholder.
-% \begin{description}
-%     \item[If] $(\sigma, \Delta) = \unify{} (\Delta', C \cup \set{\wcNtype{\Delta'}{N} \lessdot \tv{a}})$
-%     \item[and] $\tv{a}$ being a type placeholders used in $C$
-%     \item[then] $\text{fv}(\sigma(\tv{a})) \subseteq \Delta, \Delta'$
-% \end{description}
-% \end{lemma}
+\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}
 
-
-
-%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:}
+\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}
 \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'} })$
-\item[Then] there exists a substitution $\sigma'$ with:
+\item[Then] 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' \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}
 
-\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}
-
 % \begin{lemma} % a lemma where we distinguis between free variable on the left or the right side of a constraint (not needed anymore)
 %     The \unify{} algorithm only produces correct output for constraints not containing free variables.    
 % \begin{description}
@@ -418,8 +388,6 @@ $\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:
@@ -443,13 +411,6 @@ 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}}$:
@@ -463,7 +424,7 @@ we have to show S-Exists for some $\Delta''$ and $\ol{T} = \sigma(\overline{\wtv
 % 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 \text{CC}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$
+$\Delta' \vdash \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
@@ -545,165 +506,159 @@ $\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}
-% 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}.
-% 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.
+\subsection{Converting to Wild FJ}
+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}.
+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.
 
-% %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.
+%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.
 
-% Figure \ref{fig:tletexpr} shows type rules for fields and method calls.
-% They have been merged with let statements and simplified.
+Figure \ref{fig:tletexpr} shows type rules for fields and method calls.
+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,
-% are necessary for the soundness proof.
+The let statements and the type $\wcNtype{\Delta'}{N}$, which the type inference algorithm can freely choose,
+are necessary for the soundness proof.
 
-% %TODO: Show that well-formed implies witnessed!
-% We change the type rules to require the well-formedness instead of the witnessed property.
-% See figure \ref{fig:well-formedness}.
+%TODO: Show that well-formed implies witnessed!
+We change the type rules to require the well-formedness instead of the witnessed property.
+See figure \ref{fig:well-formedness}.
 
-% 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}.
-% With \texttt{witnessed} being the stronger one.
-% 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.
-% 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 well-formedness criteria is more restrictive than the ones used for \wildFJ{}.
+\cite{WildcardsNeedWitnessProtection} works with the two different judgements $\ok$ and \texttt{witnessed}.
+With \texttt{witnessed} being the stronger one.
+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.
+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.
 
-% 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.
-% 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}}$.
+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.
+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}}$.
 
-% 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}} \ \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$.
+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}} \ \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$.
 
-% \begin{figure}[tp]
-% $\begin{array}{l}
-%     \typerule{T-Var}\\
-%     \begin{array}{@{}c}
-%         x : \type{T} \in \Gamma
-%         \\
-%         \hline
-%     \vspace*{-0.3cm}\\
-%         \Delta | \Gamma \vdash x : \type{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 | \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}\\
-%     \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}$
-% \\[1em]
-% $\begin{array}{l}
-%     \typerule{T-Field}\\
-%     \begin{array}{@{}c}
-%         \Delta | \Gamma \vdash \texttt{t} : \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{let}\ x : \wcNtype{\Delta'}{N} = \texttt{t} \ \texttt{in}\ x.\texttt{f}_i : \type{S}
-%     \end{array}
-% \end{array}$
-% \\[1em]
-% $\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
-%         \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} \ \ok \quad \quad
-%         \Delta | \Gamma \vdash \texttt{t}_r : \type{T}_r \quad \quad
-%         \Delta | \Gamma \vdash \ol{t} : \ol{T} \quad \quad
-%         \Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
-%         \Delta \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
-%         \\
-%         \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
-%         \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 \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}
-%     \end{array}
-% \end{array}$
-% \\[1em]
-% $\begin{array}{l}
-%     \typerule{T-Elvis}\\
-%     \begin{array}{@{}c}
-%         \Delta | \Gamma \vdash t_1 : \type{T}_1 \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}_2 <: \type{T}
-%         \\
-%         \hline
-%     \vspace*{-0.3cm}\\
-%         \Delta | \Gamma \vdash t_1 \elvis{} t_2 : \type{T}
-%     \end{array}
-% \end{array}$
-% \\[1em]
-% $\begin{array}{l}
-%         \typerule{T-Method}\\
-%     \begin{array}{@{}c}
-%         \text{dom}(\Delta)=\ol{X} \quad \quad
-%         \Delta' = \overline{\type{Y} : \bot .. \type{U}} \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} \\
-%         \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 
-%         \text{override}(\texttt{m}, \type{N}, \generics{\ol{Y \triangleleft U}}\ol{T} \to \type{T})
-%         \\
-%         \hline
-%     \vspace*{-0.3cm}\\
-%         \Delta \vdash \generics{\ol{Y \triangleleft U}} \type{T} \ \texttt{m}(\overline{\type{T} \ x}) = t \ \ok \ \texttt{in C}
-%     \end{array}
-% \end{array}$
-% \\[1em]
-% $\begin{array}{l}
-%         \typerule{T-Class}\\
-%     \begin{array}{@{}c}
-%         \Delta = \overline{\type{X} : \bot .. \type{U}} \quad \quad 
-%         \Delta \vdash \ol{U}, \ol{T} \ \ok \quad \quad
-%         \Delta \vdash \type{N} \ \ok \quad \quad
-%         \Delta \vdash \ol{M} \ \ok \texttt{ in C}
-%         \\
-%         \hline
-%     \vspace*{-0.3cm}\\
-%         \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M} } \ \ok
-%     \end{array}
-% \end{array}$
-% \caption{T-Call and T-Field} \label{fig:tletexpr}
-% \end{figure}
+\begin{figure}[tp]
+$\begin{array}{l}
+    \typerule{T-Var}\\
+    \begin{array}{@{}c}
+        x : \type{T} \in \Gamma
+        \\
+        \hline
+    \vspace*{-0.3cm}\\
+        \Delta | \Gamma \vdash x : \type{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 | \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}\\
+    \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}$
+\\[1em]
+$\begin{array}{l}
+    \typerule{T-Field}\\
+    \begin{array}{@{}c}
+        \Delta | \Gamma \vdash \texttt{t} : \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{let}\ x : \wcNtype{\Delta'}{N} = \texttt{t} \ \texttt{in}\ x.\texttt{f}_i : \type{S}
+    \end{array}
+\end{array}$
+\\[1em]
+$\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
+        \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} \ \ok \quad \quad
+        \Delta | \Gamma \vdash \texttt{t}_r : \type{T}_r \quad \quad
+        \Delta | \Gamma \vdash \ol{t} : \ol{T} \quad \quad
+        \Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
+        \Delta \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}
+        \\
+        \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
+        \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 \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}
+    \end{array}
+\end{array}$
+\\[1em]
+$\begin{array}{l}
+    \typerule{T-Elvis}\\
+    \begin{array}{@{}c}
+        \Delta | \Gamma \vdash t_1 : \type{T}_1 \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}_2 <: \type{T}
+        \\
+        \hline
+    \vspace*{-0.3cm}\\
+        \Delta | \Gamma \vdash t_1 \elvis{} t_2 : \type{T}
+    \end{array}
+\end{array}$
+\\[1em]
+$\begin{array}{l}
+        \typerule{T-Method}\\
+    \begin{array}{@{}c}
+        \text{dom}(\Delta)=\ol{X} \quad \quad
+        \Delta' = \overline{\type{Y} : \bot .. \type{U}} \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} \\
+        \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 
+        \text{override}(\texttt{m}, \type{N}, \generics{\ol{Y \triangleleft U}}\ol{T} \to \type{T})
+        \\
+        \hline
+    \vspace*{-0.3cm}\\
+        \Delta \vdash \generics{\ol{Y \triangleleft U}} \type{T} \ \texttt{m}(\overline{\type{T} \ x}) = t \ \ok \ \texttt{in C}
+    \end{array}
+\end{array}$
+\\[1em]
+$\begin{array}{l}
+        \typerule{T-Class}\\
+    \begin{array}{@{}c}
+        \Delta = \overline{\type{X} : \bot .. \type{U}} \quad \quad 
+        \Delta \vdash \ol{U}, \ol{T} \ \ok \quad \quad
+        \Delta \vdash \type{N} \ \ok \quad \quad
+        \Delta \vdash \ol{M} \ \ok \texttt{ in C}
+        \\
+        \hline
+    \vspace*{-0.3cm}\\
+        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M} } \ \ok
+    \end{array}
+\end{array}$
+\caption{T-Call and T-Field} \label{fig:tletexpr}
+\end{figure}
 

tRules.tex

@@ -1,85 +1,32 @@
+\section{Syntax and Typing}\label{sec:tifj}
 
-\section{\TamedFJ{}}\label{sec:tifj}
-%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.
+The input syntax for our algorithm is shown in figure \ref{fig:syntax}
+and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}.
 
-A method assumption consists of a method name, a list of type variables, a list of argument types, and a return type.
-The first type in the list of argument types is the type of the surrounding class also known as the \texttt{this} parameter.
-See Figure~\ref{fig:methodTypeExample} for an example, where the
-\texttt{add} method is treated internally as a method with two
-arguments, because we add \texttt{this} to its argument list.
-The type variable $\type{A}$ of the surrounding class is part of the
-method's list of type parameters.
-%For example the \texttt{add} method in listing \ref{lst:tamedfjSample} is represented by the assumption
-%$\texttt{add} : \generics{\ol{X \triangleleft Object}}\ \type{X} \to \exptype{List}{\type{X}}$.
-\begin{figure}
-\center
-\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){..,}
+Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
+The input language is designed to showcase type inference involving existential types.
+Method call rule T-Call is the most interesting part, because it emulates the behaviour of a Java method call,
+where existential types are implicitly \textit{opened} and \textit{closed}.
+
+Example: %TODO
+\begin{verbatim}
+class List<A> {
+    A head;
+    List<A> tail;
+
+    add(v) = new List(v, this);
 }
-\end{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}
+\end{verbatim}
 
-\textit{Additional Notes:}%
-\begin{itemize}
-%\item Method parameters and return types are optional.
-\item We require type annotations for fields and generic class parameters,
-  as we consider them as data declarations which are given by the programmer.
-% They are inferred in for example \cite{plue14_3b}
-\item We add the elvis operator ($\elvis{}$) to the syntax to easily showcase applications involving wildcard types.
-This operator is used to emulate Java's \texttt{if-else} expression but without the condition clause.
-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}
+%The rules depicted here are type inference rules. It is not possible to derive a distinct typing from a given input program.
+
+%The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}.
+%and is solely used for examples.
+The calculus does not include method overriding for simplicity reasons.
+Type inference for that is described in \cite{TIforFGJ} and can be added to this algorithm accordingly.
+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}.
 
 %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)
@@ -91,38 +38,200 @@ that are part of the program.
 % 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.
+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.
 
-\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} & ::= & \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}})\\
-& & \ \ | & \texttt{let}\ \expr{x} \highlight{: \wcNtype{\Delta}{N}} = \expr{e} \ \texttt{in} \ \expr{e}\\
-& & \ \ | & \expr{e} \elvis{} \expr{e}\\
+\text{Method declarations} &  \texttt{M} & ::= & \texttt{m}(\overline{\expr{x}}) = t \\
+\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 \\
 \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
+\hline
 \end{array}
 $
-\par\noindent\rule{\textwidth}{0.4pt}
-\caption{Input Syntax with optional type annotations}\label{fig:syntax}
+\caption{\TamedFJ{} Syntax}\label{fig:syntax}
 \end{figure}
 
+% \begin{figure}
+% $
+% \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} & ::= & \texttt{m}(\overline{\expr{x}}) = t \\
+% \text{Values} & v & ::= & \expr{x} \\
+% \text{Terms} & t & ::= & v \\
+% & & \ \ | & \texttt{let} \ \expr{x} = \texttt{new} \ \type{C}(\overline{v}) \ \texttt{in} \ t \\
+% & & \ \ | & \texttt{let} \ \expr{x} = v.f \ \texttt{in} \ t \\
+% & & \ \ | & \texttt{let} \ \expr{x} = v.\texttt{m}(\overline{v}) \ \texttt{in} \ t \\
+% & & \ \ | & \texttt{let} \ \expr{x} = v \elvis{} v \ \texttt{in} \ t \\
+% \text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
+% \hline
+% \end{array}
+% $
+% \caption{Input Syntax}\label{fig:syntax}
+% \end{figure}
+
+% \begin{figure}
+% $
+% \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} & ::= & \texttt{m}(\overline{\expr{x}}) = t \\
+% \text{Terms} & t & ::= & \expr{x} \\
+% & & \ \ | & \texttt{let} \ \expr{x} = t \ \texttt{in} \ t \\
+% & & \ \ | & \expr{x}.f \\
+% & & \ \ | & \expr{x}.\texttt{m}(\overline{\expr{x}}) \\
+% & & \ \ | & t \elvis{} t \\
+% \text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
+% \hline
+% \end{array}
+% $
+% \caption{Input Syntax}\label{fig:syntax}
+% \end{figure}
+
+
+% \begin{figure}
+% $
+% \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} & ::= & \texttt{m}(\overline{x}) = t \\
+% \text{Terms} & t & ::= & x \\
+% & & \ \ | & \texttt{new} \ \type{C}(\overline{t})\\
+% & & \ \ | & t.f\\
+% & & \ \ | & t.\texttt{m}(\overline{t})\\
+% & & \ \ | & t \elvis{} t\\
+% \text{Variable contexts} & \Gamma & ::= & \overline{x:\type{T}}\\
+% \hline
+% \end{array}
+% $
+% \caption{Input Syntax}\label{fig:syntax}
+% \end{figure}
+
+\subsection{ANF transformation}
+\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.
+This is similar to Java's syntax.
+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}.
+The input of this transformation is a Featherweight Java program in the syntax given \ref{fig:inputSyntax}
+and the output is a \TamedFJ{} program.
+
+\textit{Example:}\\
+\noindent
+\begin{minipage}{0.45\textwidth}
+\begin{lstlisting}[style=fgj,caption=Featherweight Java]
+m(l, v){
+    return l.add(v);
+}
+\end{lstlisting}
+    \end{minipage}%
+    \hfill
+    \begin{minipage}{0.5\textwidth}
+\begin{lstlisting}[style=tfgj,caption=\TamedFJ{} representation]
+m(l, v) = 
+    let x1 = l in
+        let x2 = v in x1.add(x2)
+\end{lstlisting}
+\end{minipage}
+
+
+% $
+% \begin{array}{|lrcl|l}
+% \hline
+% & & & \textbf{Featherweight Java Terms}\\
+% \text{Terms} & t & ::=
+% & \expr{x}
+% \\
+% & & \ \ |
+% & \texttt{new} \ \type{C}(\overline{t})
+% \\
+% & & \ \ |
+% & t.f
+% \\
+% & & \ \ | 
+% & t.\texttt{m}(\overline{t})
+% \\
+% & & \ \ | 
+% & t \elvis{} t\\
+% %
+% \hline
+% \end{array}
+% $
+
+\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}
+\end{array}$
+\end{center}
+\caption{ANF Transformation}\label{fig:anfTransformation}
+\end{figure}
+
+% $
+% \begin{array}{lrcl|l}
+% \hline
+% & & & \textbf{Featherweight Java} & \textbf{A-Normal form}  \\
+% \text{Terms} & t & ::=
+% & \expr{x}
+% & \expr{x}
+% \\
+% & & \ \ |
+% & \texttt{new} \ \type{C}(\overline{t})
+% & \texttt{let}\ \overline{x} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{x})
+% \\
+% & & \ \ |
+% & t.f
+% & \texttt{let}\ x = t \ \texttt{in}\ x.f
+% \\
+% & & \ \ | 
+% & t.\texttt{m}(\overline{t})
+% & \texttt{let}\ x_1 = t \ \texttt{in}\ \texttt{let}\ \overline{x} = \overline{t} \ \texttt{in}\ x_1.\texttt{m}(\overline{x})
+% \\
+% & & \ \ | 
+% & t \elvis{} t
+% & t \elvis{} t\\
+% %
+% \hline
+% \end{array}
+% $
+
+
+% 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}
@@ -130,20 +239,18 @@ $\begin{array}{l}
     \begin{array}{@{}c}
         \Delta \vdash \type{T} <: \type{T}
     \end{array}
- \end{array}$
- \qquad
+\end{array}$
 $\begin{array}{l}
     \typerule{S-Trans}\\
     \begin{array}{@{}c}
-        \Delta \vdash \type{S} <: \type{T} \quad \quad
-        \Delta \vdash \type{T} <: \type{U}
+        \Delta \vdash \type{S} <: \type{T}' \quad \quad
+        \Delta \vdash \type{T}' <: \type{T}
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \Delta \vdash \type{S} <: \type{U}
+        \Delta \vdash \type{S} <: \type{T}
     \end{array}
- \end{array}$
- \qquad
+\end{array}$
 $\begin{array}{l}
     \typerule{S-Upper}\\
     \begin{array}{@{}c}
@@ -153,8 +260,7 @@ $\begin{array}{l}
     \vspace*{-0.9em}\\
         \Delta \vdash \type{X} <: \type{U}
     \end{array}
- \end{array}$
- \qquad
+\end{array}$
 $\begin{array}{l}
     \typerule{S-Lower}\\
     \begin{array}{@{}c}
@@ -176,15 +282,14 @@ $\begin{array}{l}
     \vspace*{-0.3cm}\\
         \Delta \vdash \wctype{\Delta'}{C}{\ol{T}} <: \wcNtype{\Delta'}{[\ol{T}/\ol{X}]\type{N}}
     \end{array}
- \end{array}$
- \quad
+\end{array}$
 $\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}(\wcNtype{\ol{\wildcard{X}{U}{L}}}{N}) = \emptyset
+        \text{dom}(\Delta') \cap \text{fv}(\wctype{\ol{\wildcard{X}{U}{L}}}{C}{\ol{S}}) = \emptyset
         \\
         \hline
     \vspace*{-0.3cm}\\
@@ -204,7 +309,6 @@ $\begin{array}{l}
         \Delta \vdash \bot \ \ok
     \end{array}
 \end{array}$
-\qquad
 $\begin{array}{l}
     \typerule{WF-Top}\\
     \begin{array}{@{}c}
@@ -215,7 +319,6 @@ $\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}
@@ -357,15 +460,18 @@ $\begin{array}{l}
 \end{array}$
 \\[1em]
 $\begin{array}{l}
+%TODO: why is dom(\Delta) subset of fv(N) a restriction. This excludes X,Y^X.Pair<X,Y>? 
+%TODO: we do not allow X.Pair<X,X> in the t-let (could we allow it? what about L and U being WTVs?)
     \typerule{T-Let}\\
     \begin{array}{@{}c}
         \Delta | \Gamma \vdash \expr{t}_1 : \type{T}_1 \quad \quad
-        \Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}
+        %\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}
+        \Delta \vdash \type{T}_1 <: \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{X}}
         \\
-        \Delta, \Delta' | \Gamma, \expr{x} : \wcNtype{}{N} \vdash \expr{t}_2 : \type{T}_2 \quad \quad
+        \Delta, \Delta' | \Gamma, \expr{x} : \wctype{}{C}{\ol{X}} \vdash \expr{t}_2 : \type{T}_2 \quad \quad
         \Delta, \Delta' \vdash  \type{T}_2 <: \type{T} \quad \quad
-        \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
-        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok
+        % \text{dom}(\Delta') \subseteq \text{fv}(\type{N})  \quad \quad
+        \Delta \vdash \type{T}, \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{X}} \ \ok
         \\
         \hline
     \vspace*{-0.3cm}\\
@@ -376,14 +482,14 @@ $\begin{array}{l}
 $\begin{array}{l}
     \typerule{T-Elvis}\\
     \begin{array}{@{}c}
-        \triangle | \Gamma \vdash \texttt{t}_1 : \type{S} \quad \quad
-        \triangle | \Gamma \vdash \texttt{t}_2 : \type{T} \quad \quad
-        \triangle \vdash \type{S} <: \type{U} \quad \quad
-        \triangle \vdash \type{T} <: \type{U} \quad \quad
+        \triangle | \Gamma \vdash \texttt{t} : \type{T}_1 \quad \quad
+        \triangle | \Gamma \vdash \texttt{t}_2 : \type{T}_2 \quad \quad
+        \triangle \vdash \type{T}_1 <: \type{T} \quad \quad
+        \triangle \vdash \type{T}_2 <: \type{T} \quad \quad
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \triangle | \Gamma \vdash \texttt{t}_1 \ \texttt{?:} \ \texttt{t}_2 : \type{U}
+        \triangle | \Gamma \vdash \texttt{t}_1 \ \texttt{?:} \ \texttt{t}_2 : \type{T}
     \end{array}
 \end{array}$
 \end{center}
@@ -395,10 +501,9 @@ $\begin{array}{l}
 $\begin{array}{l}
     \typerule{T-Method}\\
     \begin{array}{@{}c}
-        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\ldots} \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' =  \overline{\type{Y} : \bot .. \type{P}} \\
-        \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \quad \quad
+        (\type{T'},\ol{T}) \to \type{T} \in \mathtt{\Pi}(\texttt{m})\quad \quad
+        \triangle' =  \overline{\type{Y} : \bot .. \type{P}} \quad \quad
+        \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \\
         \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 
@@ -406,33 +511,37 @@ $\begin{array}{l}
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) \set{ \texttt{return}\ \texttt{e}; } \ \ok \ \text{in C}
+        \mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \text{ in C with } \generics{\ol{Y \triangleleft P}}
     \end{array}
 \end{array}$
 \\[1em]
 $\begin{array}{l}
     \typerule{T-Class}\\
     \begin{array}{@{}c}
-        %\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} \\
+        \mathtt{\Pi}' = \mathtt{\Pi} \cup \set{ \texttt{m} : (\exptype{C}{\ol{X}}, \ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{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}
+        \mathtt{\Pi}' | \triangle \vdash \ol{M} \ \ok \text{ in C with} \ \generics{\ol{Y \triangleleft P}}
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \mathtt{\Pi} \vdash \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \} 
+        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \}  : \mathtt{\Pi}''
     \end{array}
 \end{array}$
-%\\[1em]
-\hfill
+\\[1em]
 $\begin{array}{l}
     \typerule{T-Program}\\
     \begin{array}{@{}c}
-        \mathtt{\Pi} = \overline{\texttt{m} : \generics{\ol{X \triangleleft \type{N}}}\ol{T} \to \type{T}}
+        \emptyset \vdash \texttt{L}_1 : \mathtt{\Pi}_1 \quad \quad 
+        \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}\\
-    \mathtt{\Pi} \vdash \overline{D}
+        \vdash \ol{L} : \mathtt{\Pi}_n
     \end{array}
 \end{array}$
 \end{center}
@@ -456,8 +565,4 @@ $\begin{array}{l}
     \end{array}
 \end{array}$
 \caption{Field access}
-\end{figure}
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "TIforWildFJ"
-%%% End:
+\end{figure}

todo-11.4.24

@@ -1,16 +0,0 @@
-- 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

@@ -1,416 +0,0 @@
-
-\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}