Restructure and Cleanup Unify

modified:   relatedwork.tex

.gitignore

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

TIforWildFJ.tex

@@ -1,5 +1,5 @@
 
-\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate]{lipics-v2021}
+\documentclass{llncs}
 %This is a template for producing LIPIcs articles. 
 %See lipics-v2021-authors-guidelines.pdf for further information.
 %for A4 paper format use option "a4paper", for US-letter use option "letterpaper"
@@ -40,6 +40,7 @@
 
 \input{prolog}
 
+\begin{document}
 \bibliographystyle{plainurl}% the mandatory bibstyle
 
 \title{Global Type Inference for Featherweight Java with Wildcards} %TODO Please add
@@ -54,16 +55,16 @@
 
 \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.'
 
-\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/
+%\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[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
+%\category{} %optional, e.g. invited paper
 
-\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
+%\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
 %\relatedversiondetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93]{Classification (e.g. Full Version, Extended Version, Previous Version}{URL to related version} %linktext and cite are optional
 
 %\supplement{}%optional, e.g. related research data, source code, ... hosted on a repository like zenodo, figshare, GitHub, ...
@@ -77,21 +78,20 @@
 
 
 
-%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
 
@@ -146,6 +146,7 @@ class Example{
 
 \include{soundness}
 %\include{termination}
+\include{relatedwork}
 
 \bibliography{martin}
 

conclusion.tex

@@ -1,10 +1,132 @@
+\section{Properties of the Algorithm}
+\begin{itemize}
+    \item 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}.
+    
+\end{itemize}
+
+%TODO: how are the challenges solved: Describe this in the last chapter with examples!
+\section{Soundness}\label{sec:soundness}
+
+\section{Completeness}\label{sec:completeness}
+The algorithm can find a solution to every program which the Unify by Plümicke finds
+a correct solution aswell.
+It will not infer intermediat type like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X},\rwildcard{X}}$.
+There is propably some loss of completeness when capture constraints get deleted.
+This happens because constraints of the form $\tv{a} \lessdotCC \exptype{C}{\wtv{x}}$ are kept as long as possible.
+Here the variable $\tv{a}$ maybe could hold a wildcard type,
+but it gets resolved to a $\generics{\type{A} \triangleleft \type{N}}$.
+This combined with a constraint $\type{N} \lessdot \wtv{x}$ looses a possible solution.
+
+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}
+
+\subsection{Discussion Pair Example}
+\begin{verbatim}
+<X> Pair<X,X> make(List<X> l){ ... }
+<X> boolean compare(Pair<X,X> p) { ... }
+
+List<?> l;
+Pair<?,?> p;
+
+compare(make(l)); // Valid
+compare(p); // Error
+\end{verbatim}
+
+Our type inference algorithm is not able to solve this example.
+When we convert this to \TamedFJ{} and generate constraints we end up with:
+\begin{lstlisting}[style=tamedfj]
+let m = let x = l in make(x) in compare(m)
+\end{lstlisting}
+\begin{constraintset}$
+\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \ntv{x},
+\ntv{x} \lessdotCC \exptype{List}{\wtv{a}}
+\exptype{Pair}{\wtv{a}, \wtv{a}} \lessdot \ntv{m}, %% TODO: Mark this constraint
+\ntv{m} \lessdotCC \exptype{Pair}{\wtv{b}, \wtv{b}}
+$\end{constraintset}
+
+$\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{m}$ 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!
+
+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}).
 As you can see by the given examples our type inference algorithm can calculate
 type solutions for programs involving wildcards.
 
-Going further we try to proof soundness and completeness for \unify{}.
+Going further we try to prove soundness and completeness for \unify{}.
 
 
 % The tricks are:

constraints.tex

@@ -1,7 +1,71 @@
-\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.
+\subsection{Capture Constraints}
+%TODO: General Capture Constraint explanation
 
+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]{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.
+The rest of 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 a ANF transformation (see \ref{sec:anfTransformation}).
+
+
+
+\section{Constraint generation}\label{chapter:constraintGeneration}
 % Method names are not unique.
 % It is possible to define the same method in multiple classes.
 % The \TYPE{} algorithm accounts for that by generating Or-Constraints.
@@ -9,22 +73,109 @@
 
 %\subsection{Well-Formedness}
 
-Constraint generation step is the same as in \cite{TIforFGJ} except for field access and method invocation.
-Here \fjtype{} generates capture constraints instead of normal subtype constraints.
 
-Subtype constraints are created according to the type rules defined in section \ref{sec:tifj}.
-The \typeExpr{} function creates constraints for a given expression.
+% But it can be easily adapted to Featherweight Java or Java.
+% We add T <. a for every return of an expression anyway. If anything returns a Generic like X it is not directly used in a method call like X <c T
 
-$\begin{array}{c}
-\typeExpr(\texttt{t}_1, \ntv{b}) = C_l \quad \quad \typeExpr(\texttt{t}_2, \ntv{c}) = C_l \quad \quad \ntv{b}, \ntv{c} \ \text{fresh}
-\\
-\hline
-\typeExpr(\texttt{t}_1 \texttt{?:} \texttt{t}_2, \tv{a}) = C_l \cup C_r \cup \set{\ntv{b} \lessdot \tv{a}, \ntv{c} \lessdot \tv{a}}
+\begin{description}
+\item[input] \TamedFJ{} program in A-Normal form
+\item[output] Constraints
+\end{description}
+
+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.
+
+%In \TamedFJ{} capture conversion is implicit.
+%To emulate Java's behaviour we assume the input program not to contain any let statements.
+%They will be added by an ANF transformation (see chapter \ref{sec:anfTransformation}).
+
+Before generating constraints the input is transformed by an ANF transformation (see section \ref{sec:anfTransformation}).
+
+%Constraints are generated on the basis of the program in A-Normal form.
+%After adding the missing type annotations the resulting program is valid under the typing rules in \cite{WildFJ}.
+
+%This is shown in chapter \ref{sec:soundness}
+
+%\section{\TamedFJ{}: Syntax and Typing}\label{sec:tifj}
+
+% The syntax forces every expression to undergo a capture conversion before it can be used as a method argument.
+% Even variables have to be catched by a let statement first.
+% This behaviour emulates Java's implicit capture conversion.
+
+\subsection{ANF transformation}\label{sec:anfTransformation}
+\newcommand{\anf}[1]{\ensuremath{\tau}(#1)}
+%https://en.wikipedia.org/wiki/A-normal_form)
+Featherweight Java's syntax involves no \texttt{let} statement
+and terms can be nested freely similar to Java's syntax.
+Our calculus \TamedFJ{} uses let statements to explicitly apply capture conversion to wildcard types,
+but we don't know which expressions will spawn wildcard types because there are no type annotations yet.
+To emulate Java's behaviour we have to preemptively add capture conversion in every suitable place.
+%To convert it to \TamedFJ{} additional let statements have to be added.
+This is done by a \textit{A-Normal Form} \cite{aNormalForm} transformation shown in figure \ref{fig:anfTransformation}.
+After this transformation every method invocation is preceded by let statements which perform capture conversion on every argument before passing them to the method.
+See the example in listings \ref{lst:anfinput} and \ref{lst:anfoutput}.
+\begin{figure}
+\begin{minipage}{0.45\textwidth}
+\begin{lstlisting}[style=fgj,caption=\TamedFJ{} example,label=lst:anfinput]
+m(l, v){
+    return l.add(v);
+}
+\end{lstlisting}
+    \end{minipage}%
+    \hfill
+    \begin{minipage}{0.5\textwidth}
+\begin{lstlisting}[style=tfgj,caption=A-Normal form,label=lst:anfoutput]
+m(l, v) = 
+    let x1 = l in
+        let x2 = v in x1.add(x2)
+\end{lstlisting}
+\end{minipage}
+\end{figure}
+
+\begin{figure}
+    \begin{center}
+$\begin{array}{lrcl}
+%\text{ANF}
+& \anf{\expr{x}} & = & \expr{x} \\
+& \anf{\texttt{new} \ \type{C}(\overline{t})} & = & \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}}) \\
+& \anf{t.f} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \expr{x}.f \\
+& \anf{t.\texttt{m}(\overline{t})} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \expr{x}.\texttt{m}(\overline{\expr{x}}) \\
+& \anf{t_1 \elvis{} t_2} & = & \anf{t_1} \elvis{} \anf{t_2} \\
+& \anf{\texttt{let}\ x = \expr{t}_1 \ \texttt{in}\ \expr{t}_2} & = & \texttt{let}\ x = \anf{\expr{t}_1} \ \texttt{in}\ \anf{\expr{t}_2} 
+\end{array}$
+\end{center}
+\caption{ANF Transformation}\label{fig:anfTransformation}
+\end{figure}
+
+\begin{figure}
+  \center
+$
+\begin{array}{lrcl}
+%\hline
+\text{Terms} & t & ::= & \expr{x} \\
+& & \ \ | &  \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}_c}) \\
+& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \expr{x}_c.f \\
+& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \expr{x}_c.\texttt{m}(\overline{\expr{x}_c}) \\
+& & \ \ | & t \elvis{} t \\
+%\hline
 \end{array}
 $
+\caption{Syntax of a \TamedFJ{} program in A-Normal Form}\label{fig:anf-syntax}
+\end{figure}
 
-The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
-Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
+\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.
@@ -33,25 +184,12 @@ A normal type placeholder cannot hold types containing free variables.
 Normal type placeholders are assigned types which are also expressible with Java syntax.
 So no types like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ or $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
 
-Type variables declared in the class header are passed to \unify{}.
+It is possible to feed the \unify{} algorithm a set of free variables with predefined bounds.
+This is used for class generics see figure \ref{fig:constraints-for-classes}.
+The \fjtype{} function returns a set of constraints aswell as an initial environment $\Delta$
+containing the generics declared by this class.
 Those type variables count as regular types and can be held by normal type placeholders.
 
-
-There are two different types of constraints:
-\begin{description}
-\item[$\lessdot$] \textit{Example:}
-
-$\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}$
-
-\noindent
-Those two constraints imply that we have to find a type replacement for type variable $\tv{a}$,
-which is a supertype of $\exptype{List}{String}$ aswell as $\exptype{List}{Integer}$.
-This paper describes a \unify{} algorithm to solve these constraints and calculate a type solution $\sigma$.
-For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
-\item[$\lessdotCC$] TODO
-% The \fjtype{} algorithm assumes capture conversions for every method parameter.
-\end{description}
-
 %Why do we need a constraint generation step?
 %% The problem is NP-Hard
 %% a method call, does not know which type it will produce
@@ -59,48 +197,37 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
 
 %NO equals constraints during the constraint generation step!
 \begin{figure}[tp]
-  \begin{align*}
-    % 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}{\il{T}} && \text{class type (with type variables)} \\
-    % Constraints
-    \simpleCons &::= \type{T} \lessdot \type{U} && \text{subtype constraint}\\
-    \orCons{} &::= \set{\set{\overline{\simpleCons_1}}, \ldots, \set{\overline{\simpleCons_n}}} && \text{or-constraint}\\
-    \constraint &::= \simpleCons \mid \orCons && \text{constraint}\\
-    \consSet &::= \set{\constraints} && \text{constraint set}\\
-    % Method assumptions:
-    \methodAssumption &::= \exptype{C}{\ol{X} \triangleleft \ol{N}}.\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.}
+  \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{}}
   \label{fig:syntax-constraints}
 \end{figure}
 
 \begin{figure}[tp]
   \begin{gather*}
     \begin{array}{@{}l@{}l}
-      \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\ol{X} \triangleleft \ol{N}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, K \, \overline{M} \}}) =\\
+      \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\overline{\type{X} \triangleleft \type{N}}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\
               & \begin{array}{ll@{}l}
-\textbf{let} & \forall \texttt{m} \in \ol{M}: \tv{a}_\texttt{m}, \ol{\tv{a}_m} \ \text{fresh} \\
-             & \ol{\methodAssumption} = \begin{array}[t]{l}
-                \set{ \mv{m'} : (\exptype{C}{\ol{X} \triangleleft \ol{N}} \to \ol{\tv{a}} \to \tv{a}) \mid
-                  \mv{m'} \in \ol{M} \setminus \set{\mv{m}}, \, \tv{a}\, \ol{\tv{a}}\ \text{fresh} } \\
-\ \cup \, \set{\mv{m} : (\exptype{C}{\ol{X} \triangleleft \ol{N}} \to \ol{\tv{a}_m} \to \tv{a}_\mv{m})}
-\end{array}
- \\
-              & C_m = \typeExpr(\mtypeEnvironment \cup \set{\mv{this} :
-                \exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}_m} }, \texttt{e}, \tv{a}_\texttt{m}) \\
-\textbf{in} 
-              & { ( \mtypeEnvironment \cup \ol{\methodAssumption}, \,
-                \bigcup_{\texttt{m} \in \ol{M}} C_m )
-                } 
+\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}
+                \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{gather*}
@@ -108,39 +235,6 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
   \label{fig:constraints-for-classes}
 \end{figure}
 
-% \textbf{Method Assumptions}
-
-% %$\Pi$ is a set of method assumptions used by the $\fjtype{}$ algorithm.
-
-% % \begin{verbatim}
-% % class Example<X> {
-% %   <Y> Y m(Example<Y> p){ ... }
-% % }
-% % \end{verbatim}
-
-% In Featherweight Java a method type is bound to a specific class.
-% The class \texttt{Example} shown above contains one method \texttt{m}:
-
-% \begin{displaymath}
-% \textit{mtype}({\texttt{m}, \exptype{Example}{\type{X}}}) = \generics{\type{Y}} \ \exptype{Example}{\type{Y}} \to \type{Y}
-% \end{displaymath}
-
-% $\Pi$ is a set of method assumptions used by the $\fjtype{}$ algorithm.
-% It's a map of method types to method names.
-% Every method name has a set of possible types,
-% because there could be more than one method with the same name in a program consisting out of multiple classes.
-% To simplify the syntax of method assumptions, we add the inheriting class type to the parameter list:
-
-% \begin{displaymath}
-% \Pi = \set{ \texttt{m} : \generics{\type{X}, \type{Y}} \ (\exptype{Example}{\type{X}}, \exptype{Example}{\type{Y}}) \to \type{Y}}
-% \end{displaymath}
-
-% \begin{verbatim}
-% class Example<X> { }
-
-% <X, Y> Y m(Example<X> this, Example<Y> p){ ... }
-% \end{verbatim}
-
 \begin{displaymath}
   \begin{array}{@{}l@{}l}
     \typeExpr{} &({\mtypeEnvironment} , \texttt{e}.\texttt{f}, \tv{a}) = \\
@@ -164,33 +258,39 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
   \end{array}
 \end{displaymath}
 
-The set of method assumptions returned by the \textit{mtypes} function is used to generate the constraints for a method call expression:
-
-There are two kinds of method calls.
-The ones to already typed methods and calls to untyped methods.
+\begin{displaymath}
+  \begin{array}{@{}l@{}l}
+    \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}, \expr{e}_1, \tv{e}_1)\\
+                    & \consSet_2 = \typeExpr({\mtypeEnvironment} \cup \set{\expr{x} : \tv{x}}, \expr{e}_2, \tv{e}_2)\\
+                    & \constraint =
+                      \set{
+                      \tv{e}_1 \lessdot \tv{x}, \tv{e}_2 \lessdot \tv{a}
+                      }\\
+                    {\mathbf{in}} & {
+                      \consSet_1 \cup \consSet_2 \cup \set{\constraint}}
+                  \end{array} 
+  \end{array}
+\end{displaymath}
 
 \begin{displaymath}
   \begin{array}{@{}l@{}l}
-      \typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a}) = \\
+      \typeExpr{} & ({\mtypeEnvironment} , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\
       & \begin{array}{ll}
       \textbf{let}
       & \tv{r}, \ol{\tv{r}} \text{ fresh} \\
-      & \consSet_R = \typeExpr(({\mtypeEnvironment} ;
-        \overline{\localVarAssumption}), \texttt{e}, \tv{r})\\
-      & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \ol{e}, \ol{\tv{r}})  \\
-      & \begin{array}{@{}l@{}l}
-        \constraint = \orCons\set{ & 
-                  \begin{array}[t]{l}
-                    [\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdotCC \exptype{C}{\ol{X}},
-                    \overline{\tv{r}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a}, 
-                    \ol{Y} \lessdot \ol{N} \}
-                  \end{array}\\
-            & \ |\ 
-            (\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T}) \in 
-                {\mtypeEnvironment} %, \, |\ol{T}| = |\ol{e}|
-            , \, \overline{\wtv{a}} \text{ fresh}}
-        \end{array}\\
-      \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T})
+      & \constraint = [\overline{\wtv{b}}/\ol{Y}]\set{
+                    \ol{S} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a}, 
+                    \ol{Y} \lessdot \ol{N} }\\
+      \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}
+      \end{array}
+                    
       \end{array}
       \end{array}
   \end{displaymath}
@@ -199,95 +299,93 @@ The ones to already typed methods and calls to untyped methods.
 \textbf{Example:}
 \begin{verbatim}
 class Class1{
-  <X> X m(List<X> lx, List<? extends X> lt){ ... }
-  List<? extends String> wGet(){ ... }
-  List<String> get() { ... }
+  <A> A head(List<X> l){ ... }
+  List<? extends String> get() { ... }
 }
 
 class Class2{
   example(c1){
-    return c1.m(c1.get(), c1.wGet());
+    return c1.head(c1.get());
   }
 }
 \end{verbatim}
 %This example comes with predefined type annotations.
-We assume the class \texttt{Class1} has already been processed by our type inference algorithm,
-which has lead to the given type annotations for \texttt{Class1}.
-Now we call the $\fjtype{}$ function with the class \texttt{Class2} and the method assumptions for the preceeding class:
+We assume the class \texttt{Class1} has already been processed by our type inference algorithm
+leading to the following type annotations:
+%Now we call the $\fjtype{}$ function with the class \texttt{Class2} and the method assumptions for the preceeding class:
 \begin{displaymath}
 \mtypeEnvironment =  \left\{\begin{array}{l}
-    \type{Class1}.\texttt{m}: \generics{\type{X} \triangleleft \type{Object}} \ 
-      (\exptype{List}{\type{X}}, \, \wctype{\wildcard{A}{\type{X}}{\bot}}{List}{\wildcard{A}{\type{X}}{\bot}}) \to \type{X}, \\
-     \type{Class1}.\texttt{wGet}: () \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\wildcard{A}{\type{Object}}{\type{String}}}, \\
-     \type{Class1}.\texttt{get}: () \to \exptype{List}{\type{String}}
+    \texttt{m}: \generics{\type{A} \triangleleft \type{Object}} \ 
+      (\type{Class1},\, \exptype{List}{\type{A}}) \to \type{X}, \\
+     \texttt{get}: (\type{Class1}) \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\rwildcard{A}}
 \end{array} \right\} 
 \end{displaymath}
 
-The result of the $\typeExpr{}$ function is the constraint set
-\begin{displaymath}
-C = \left\{ \begin{array}{l}
-\tv{c1} \lessdot \type{Class1}, \\
-\tv{p1} \lessdot \exptype{List}{\wtv{x}}, \\
-\exptype{List}{\type{String}} \lessdot \tv{p1}, \\
-\tv{p2} \lessdot \wctype{\wildcard{A}{\wtv{x}}{\bot}}{List}{\rwildcard{A}}, \\
-\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{p2} 
-\end{array} \right\}
-\end{displaymath}
+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.
 
+\begin{minipage}{0.45\textwidth}
+  \begin{lstlisting}[style=tamedfj]
+class Class2 {
+  example(c1) = let x = c1 in
+    let xp = x.get() in x.m(xp);
+}
+\end{lstlisting}
+      \end{minipage}%
+      \hfill
+      \begin{minipage}{0.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}
 
-The first parameter of a method assumption is the receiver type $\type{T}_r$.
-\texttt{Class1} for this example.
-Therefore the $(\tv{c1} \lessdot \type{Class1})$ constraint.
-The type variable $\tv{c1}$ is assigned to the parameter \texttt{c1} of the \texttt{example} method.
+Following is a possible solution for the given constraint set:
 
-or a simplified version:
+\begin{minipage}{0.55\textwidth}
+  \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);
+}
+\end{lstlisting}
+      \end{minipage}%
+      \hfill
+      \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}
 
-\begin{displaymath}
-C = \left\{ \begin{array}{l}
-\tv{c1} \lessdot \type{Class1}, \\
-\exptype{List}{\type{String}} 
- \lessdot \exptype{List}{\wtv{x}}, \\
-\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}
- \lessdot \wctype{\wildcard{A}{\wtv{x}}{\bot}}{List}{\rwildcard{A}}
-\end{array} \right\}
-\end{displaymath}
+For $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$ to be a correct solution for $\tv{xp}$
+the constraint $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{a}}$
+must be satisfied.
+This is possible, because we deal with a capture constraint.
+The $\lessdotCC$ constraint allows the left side to undergo a capture conversion
+which leads to $\exptype{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{a}}$.
+Now a substitution of the wildcard placeholder $\wtv{a}$ with $\rwildcard{A}$ leads to a satisfied constraint set.
 
-
-$\wtv{x}$ is a type variable we use for the generic $\type{X}$. It is flagged as a free type variable.
-%TODO: Do an example where wildcards are inserted and we need capture conversion
-
-\unify{} returns the solution $(\sigma = \set{ \tv{x} \to \type{String} })$
-
-% \\[1em]
-% \noindent
-% \textbf{Example:}
-% \begin{verbatim}
-% class Class1 {
-%   <X> Pair<X, X> make(List<X> l){ ... }
-%   <Y> boolean compare(Pair<Y,Y> p) { ... }
-
-%   example(l){
-%     return compare(make(l));
-%   }
-% }
-% \end{verbatim}
-
-% The method call \texttt{make(l)} generates the constraints
-% \begin{displaymath}
-%   \tv{l} \lessdot \exptype{List}{\tv{x}}, \exptype{Pair}{\tv{x}, \tv{x}} \lessdot \tv{m}
-% \end{displaymath}
-% with $\tv{l}$ being the type placeholder for the variable \texttt{l}
-% and $\tv{m}$ is the type variable for the return type of the method call.
-% $\tv{m}$ is then used as the parameter for the \texttt{compare} method:
-% \begin{displaymath}
-%   \tv{m} \lessdot \exptype{Pair}{\tv{y}, \tv{y}}
-% \end{displaymath}
-% Note the conversion of the generic parameters \texttt{X} and \texttt{Y} to type variables $\tv{x}$ and $\tv{y}$.
-
-
-
-% Step 3 of the \unify{} algorithm has to look for every possible supertype of $\exptype{Pair}{\tv{x}, \tv{x}}$,
-% when processing the $\exptype{Pair}{\tv{x}, \tv{x}} \lessdot \tv{m}$ constraint.
+The wildcard placeholders are not used as parameter or return types of methods.
+Or as types for variables introduced by let statements.
+They are only used for generic method parameters during a method invocation.
+Type placeholders which are not flagged as wildcard placeholders ($\wtv{a}$) can never hold a free variable or a type containing free variables.
+This practice hinders free variables to leave their scope.
+The free variable $\rwildcard{A}$ generated by the capture conversion on the type $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$
+cannot be used anywhere else then inside the constraints generated by the method call \texttt{x.m(xp)}.
 
 \begin{displaymath}
   \begin{array}{@{}l@{}l}
@@ -317,12 +415,12 @@ $\wtv{x}$ is a type variable we use for the generic $\type{X}$. It is flagged as
     \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}} \\
+                    & \ol{\ntv{r}}, \ol{\ntv{a}} \ \text{fresh} \\
+                    & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \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{a}}}}
+                        \set{\tv{a} \doteq \exptype{C}{\ol{\ntv{a}}}}}
                   \end{array} 
   \end{array}
 \end{displaymath}

martin.bib

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

prolog.tex

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

relatedwork.tex

@@ -0,0 +1,76 @@
+
+\section{Related Work}
+Igarashi et al \cite{FJ} define Featherweight Java
+and its generic sibling, Featherweight Generic Java. Their language is
+a functional calculus reduced to the bare essentials, they develop the full metatheory, they
+support generics, and study the type erasing transformation used by
+the Java compiler. Stadelmeier et. al. extends this approach by global type
+inference \cite{TIforFGJ}.
+
+\subsection{Wildcards in formal Java models}
+Wildcards are first described in a research paper in \cite{addingWildcardsToJava}. In
+\cite{TEP05} the Featherweight Java-Calculus \textsf{Wild~ FJ} is introduced. It
+contains a formal description of wildcards. The Java Language Specification
+\cite{GoJoStBrBuSm23}  refers to \textsf{Wild~FJ} for the introduction of
+wildcards. In \cite{aModelForJavaWithWildcards} a formal model based of explicite existential types
+is introduced and proven as sound. Additionally, for a subset of Java a
+translation to the formal model is given, such that this subset is proven as
+sound. In \cite{WildcardsNeedWitnessProtection} another core calculus is
+introduced, which is proven as 
+sound, too. In this paper it is shown that the unsoundness of Java which is
+discovered in \cite{AT16} is avoidable, even in the absence of nullness-aware type
+system. In \cite{TamingWildcards} finally a framework is presented which combines
+use-site variance (wildcards as in Java) and definition-site variance (as in Scala). For
+instance, it can be used to add use-site variance to Scala and extend the Java
+type system to infer the definition-site variance.
+
+Our calculus is mixture ...
+
+\subsection{Type inference}
+Some object-oriented languages like Scala, C\#, and Java perform
+\emph{local} type inference \cite{PT98,OZZ01}. Local type
+inference means that missing type annotations are recovered using only
+information from adjacent nodes in the syntax tree without long distance
+constraints. For instance, the type of a variable initialized with a
+non-functional expression or the return type of a method can be
+inferred. However, method argument types, in particular for recursive
+methods, cannot be inferred by local type inference.
+
+Milner's algorithm $\mathcal{W}$ \cite{DBLP:journals/jcss/Milner78} is
+the gold standard for global type inference for languages with
+parametric polymorphism, which is used by ML-style languages. The fundamental idea
+of the algorithm is to enforce type equality by many-sorted type
+unification \cite{Rob65,MM82}. This approach is effective and results
+in so-called principal types because many-sorted unification is
+unitary, which means that there is at most one most general result.
+
+Pl\"umicke \cite{Plue07_3} presents a first attempt to adopt Milner's
+approach to Java. However, the presence of subtyping means that type
+unification is no longer unitary, but still finitary. Thus, there is
+no longer a single most general type, but any type is an instance of a
+finite set of maximal types (for more details see Section
+\ref{sec:unification}). Further work by the same author
+\cite{plue15_2,plue17_2},
+refines this approach by moving to a constraint-based algorithm and by
+considering lambda expressions and Scale-like function types.
+
+Pluemicke has a different approach to introduce wildcards in \cite{plue09_1}. He
+allows wildcards as any subsitution for type variables and disclaim the
+capture conversion. Instead he extended
+the subtyping ordering such that for $\theta \sub \theta' \sub \theta''$ holds
+indeed the transitiv closure of $\QMextends{\theta} \sub \theta'$ and $\theta' \sub
+\QMsuper{\theta''}$ but not the reflexive closure. He gave a type unification
+algorithm for this type system, which he proved as sound and complete. 
+
+The problem of his type system is in the lossing reflexivity as shown in
+example \ref{intro-example1}. 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,7 +1,5 @@
 \section{Soundness}
 
-\newcommand{\CC}{\text{CC}}
-
 \begin{lemma}
 A sound TypelessFJ program is also sound under LetFJ type rules.
 \begin{description}
@@ -154,7 +152,7 @@ By structural induction over the expression $\texttt{e}$.
     % $\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
+    % by proving 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
 
@@ -329,18 +327,17 @@ If there is a solution for a constraint set $C$, then there is also a solution f
 % 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}\label{lemma:unifySoundness}
-The \unify{} algorithm only produces correct output.
+\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[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
-\item[Then] there exists a $\sigma'$ with:
-$\sigma \subseteq \sigma'$ and
-$\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
-and $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$ where $\overline{\sigma(\type{S'}) = \wcNtype{\Delta}{N}}$,
-otherwise $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \sigma'(\type{T'})}$
-% and $\sigma(\type{T'}) = \sigma(\type{T'})$.
-
+\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', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$
+\end{itemize}
 \end{description}
 \end{lemma}
 
@@ -378,6 +375,7 @@ $\Delta \vdash  \sigma(C') \implies \Delta \vdash \sigma(C)$
 \begin{description}
 \item[AddDelta] $C$ is not changed
 \item[GenDelta] by definition, S-Var-Left, and S-Trans %The generated type variable is unique due to the solved form property. %and the solved form property (no $\tv{a}$ in $C$)
+\item[GenDelta'] same as GenDelta by setting $\sigma'(\wtv{b}) = \rwildcard{B}$
 \item[GenSigma] by definition and S-Refl.
 % holds for $\set{\tv{a} \doteq \type{G}}$ by definition.
 % Holds for $C$ by assumption and because $\tv{a} \notin C$ by solved form definition ($[\type{G}/\tv{a}]C = C$).
@@ -388,6 +386,8 @@ $\Delta \vdash  \sigma(C') \implies \Delta \vdash \sigma(C)$
 \item[Settle] Assumption, S-Trans
 \item[Super] S-Extends ($\vdash \wctype{\Delta}{C}{\ol{T}} <: \wctype{\Delta}{D}{[\ol{T}/\ol{X}]\ol{N}}$), S-Trans
 \item[\generalizeRule{}] by Assumption, because $C \subset C'$
+\item[Same] by S-Exists
+\item[SameW] %TODO
 \item[Adapt] Assumption, S-Extends, S-Trans
 \item[Adopt] Assumption, because $C \subset C'$
 %\item[Capture, Reduce] are always applied together. We have to destinct between two cases:
@@ -424,7 +424,7 @@ Therefore we can say that $\Delta, \Delta', \overline{\Delta} \vdash \sigma'(\ex
 % List<X> <. Y.List<Y>, free variables are either in 
 If $\text{fv}(\exptype{C}{\ol{S}}) = \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists.
 Otherwise 
-$\Delta' \vdash \CC{}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$
+$\Delta' \vdash \text{CC}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$
 holds with any $\Delta'$ so that $(\text{fv}(\exptype{C}{\ol{S}}) \cup \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) ) \subseteq \text{dom}(\Delta') $.
 \item[Match] Assumption, S-Trans
 \item[Trim] Assumption and S-Exists
@@ -432,7 +432,8 @@ holds with any $\Delta'$ so that $(\text{fv}(\exptype{C}{\ol{S}}) \cup \text{fv}
 \item[Circle] S-Refl
 \item[Swap] by definition
 \item[Erase] S-Refl
-\item[Equals] %by definition
+\item[Equals] by definition \ref{def:equal}
+%by definition
 %TODO
 % Unify does never contain wildcard environments with unused wildcards. Therefore after N <: N' and N' <: N, both types have the same wildcard environment
 

tRules.tex

@@ -1,32 +1,43 @@
-\section{Syntax and Typing}\label{sec:tifj}
 
-The input syntax for our algorithm is shown in figure \ref{fig:syntax}
+\section{\TamedFJ{}}\label{sec:tifj}
+%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
+
+The input to our algorithm is a typeless version of Featherweight Java.
+The syntax is shown in figure \ref{fig:syntax}
 and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}.
+Method parameters and return types are optional.
+We still require type annotations for fields and generic class parameters.
+This is a design choice by us,
+as we consider them as data declarations which are given by the programmer.
+% They are inferred in for example \cite{plue14_3b}
+Note the \texttt{new} expression not requiring generic parameters,
+which are also inferred by our algorithm.
+The method call naturally has type inferred generic parameters aswell.
+We add the elvis operator ($\elvis{}$) to the syntax mainly to showcase applications involving wildcard types.
+The syntax is described in figure \ref{fig:syntax} with optional type annotations highlighted in yellow.
+It is possible to exclude all optional types.
+\TamedFJ{} is a subset of the calculus defined by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection}.
+%The language is designed to showcase type inference involving existential types.
+The idea is for our type inference algorithm to calculate all missing types and output a fully and correctly typed \TamedFJ{} program,
+which by default is also a correct Featherweight Java program (see chapter \ref{sec:soundness}).
 
-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{verbatim}
-
-%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.
+\noindent
+\textit{Notes:}
+\begin{itemize}
+\item 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}.
+%\textit{Note:}
+\item The typing rules for expressions shown in figure \ref{fig:expressionTyping} refrain from restricting polymorphic recursion.
+Type inference for polymorphic recursion is undecidable \cite{wells1999typability} and when proving completeness like in \cite{TIforFGJ} the calculus
+needs to be restricted in that regard.
+Our algorithm is not complete (see discussion in chapter \ref{sec:completeness}) and without the respective proof we can keep the \TamedFJ{} calculus as simple as possible
+and as close to it's Featherweight Java correspondent \cite{WildcardsNeedWitnessProtection} as possible.
+Our soundness proof works either way.
+\end{itemize}
 
 %Additional features like overriding methods and method overloading can be added by copying the respective parts from there.
 %Additional features can be easily added by generating the respective constraints (Plümicke hier zitieren)
@@ -38,32 +49,37 @@ Additional language constructs can be added by implementing the respective const
 % on overriding methods, because their type is already determined.
 % Allowing overriding therefore has no implication on our type inference algorithm.
 
+% The output is a valid Featherweight Java program.
+% We use the syntax of the version introduced in \cite{WildcardsNeedWitnessProtection}
+% calling it \letfj{} for that it is a Featherweight Java variant including \texttt{let} statements.
+
+\newcommand{\highlight}[1]{\begingroup\fboxsep=0pt\colorbox{yellow}{$\displaystyle #1$}\endgroup}
 \begin{figure}
+\par\noindent\rule{\textwidth}{0.4pt}
+\center
 $
 \begin{array}{lrcl}
-\hline
+%\hline
 \text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
 \text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
 \text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
 \text{Type variable contexts} &  \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
 \text{Class declarations} &  D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\
-\text{Method declarations} &  \texttt{M} & ::= & \texttt{m}(\overline{x}) = t \\
-\text{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
+\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{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
+%\hline
 \end{array}
 $
-\caption{Input Syntax}\label{fig:syntax}
+\par\noindent\rule{\textwidth}{0.4pt}
+\caption{Input Syntax with optional type annotations}\label{fig:syntax}
 \end{figure}
 
-% Each class type has a set of wildcard types $\overline{\Delta}$ attached to it.
-% The type $\wctype{\overline{\Delta}}{C}{\ol{T}}$ defines a set of wildcards $\overline{\Delta}$,
-% which can be used inside the type parameters $\ol{T}$.
-
 \begin{figure}[tp]
 \begin{center}
 $\begin{array}{l}
@@ -121,7 +137,7 @@ $\begin{array}{l}
         \Delta', \Delta \vdash [\ol{T}/\ol{\type{X}}]\ol{L} <: \ol{T} \quad \quad
         \Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\
         \text{fv}(\ol{T}) \subseteq \text{dom}(\Delta, \Delta') \quad
-        \text{dom}(\Delta') \cap \text{fv}(\wctype{\ol{\wildcard{X}{U}{L}}}{C}{\ol{S}}) = \emptyset
+        \text{dom}(\Delta') \cap \text{fv}(\wcNtype{\ol{\wildcard{X}{U}{L}}}{N}) = \emptyset
         \\
         \hline
     \vspace*{-0.3cm}\\
@@ -196,56 +212,115 @@ $\begin{array}{l}
 $\begin{array}{l}
     \typerule{T-Field}\\
     \begin{array}{@{}c}
-        \Delta | \Gamma \vdash \texttt{e} : \type{T} \quad \quad 
-        \Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
+        \Delta | \Gamma \vdash \expr{v} : \type{T} \quad \quad 
+        \Delta \vdash \type{T} <: \wcNtype{}{N} \quad \quad
         \textit{fields}(\type{N}) = \ol{U\ f} \\
-\Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
-\text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
-\Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
-        \\
         \hline
     \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash \texttt{e}.\texttt{f}_i : \type{S}
+        \Delta | \Gamma \vdash \expr{v}.\texttt{f}_i : \type{U}_i
     \end{array}
 \end{array}$
 \\[1em]
+% $\begin{array}{l}
+%     \typerule{T-Field}\\
+%     \begin{array}{@{}c}
+%         \Delta | \Gamma \vdash \texttt{e} : \type{T} \quad \quad 
+%         \Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
+%         \textit{fields}(\type{N}) = \ol{U\ f} \\
+% \Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
+% \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
+% \Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%         \Delta | \Gamma \vdash \texttt{e}.\texttt{f}_i : \type{S}
+%     \end{array}
+% \end{array}$
+% \\[1em]
+% $\begin{array}{l}
+%     \typerule{T-New}\\
+%     \begin{array}{@{}c}
+%         \Delta, \overline{\Delta} \vdash  \exptype{C}{\ol{T}} \ \ok \quad \quad
+%         \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
+%         \Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
+%         \Delta \vdash  \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
+%         \Delta, \overline{\Delta} \vdash  \overline{\type{N}} <: \overline{\type{U}} \quad \quad
+%         \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
+%         \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
+%         \Delta \vdash \type{T},  \overline{\wcNtype{\Delta}{N}} \ \ok
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%         \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}}
+%     \end{array}
+% \end{array}$
+% \\[1em] 
 $\begin{array}{l}
     \typerule{T-New}\\
     \begin{array}{@{}c}
         \Delta, \overline{\Delta} \vdash  \exptype{C}{\ol{T}} \ \ok \quad \quad
-        \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
-        \Delta | \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
+        \Delta \vdash  \overline{\type{S}} <: \overline{\type{U}} \\
+        \Delta | \Gamma \vdash \overline{\expr{v} : \type{S}} \quad \quad
+        \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} 
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}}
+        \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{v}) : \exptype{C}{\ol{T}}
+    \end{array}
+\end{array}$
+\hfill
+% $\begin{array}{l}
+%     \typerule{T-Call}\\
+%     \begin{array}{@{}c}
+%         \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
+%         \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
+%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
+%         \\
+%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
+%         \Delta | \Gamma \vdash  \texttt{e}, \ol{e} : \ol{T} \quad \quad
+%         \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
+%         \\
+%         \Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
+%         \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
+%         \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
+%         \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%         \Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T}
+%     \end{array}
+% \end{array}$
+% \\[1em]
+$\begin{array}{l}
+    \typerule{T-Call}\\
+    \begin{array}{@{}c}
+        \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
+        \Delta \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
+        \\
+        \Delta \vdash \ol{S} \ \ok \quad \quad
+        \Delta | \Gamma \vdash  \expr{v}, \ol{v} : \ol{T} \quad \quad
+        \Delta \vdash \ol{T} <: [\ol{S}/\ol{X}]\ol{U} 
+        \\
+        \hline
+    \vspace*{-0.3cm}\\
+        \Delta | \Gamma \vdash \expr{v}.\texttt{m}(\ol{v}) : \type{T}
     \end{array}
 \end{array}$
 \\[1em]
 $\begin{array}{l}
-    \typerule{T-Call}\\
+    \typerule{T-Let}\\
     \begin{array}{@{}c}
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
-        \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
+        \Delta | \Gamma \vdash \expr{t}_1 : \type{T}_1 \quad \quad
+        \Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}
         \\
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
-        \Delta | \Gamma \vdash  \texttt{e}, \ol{e} : \ol{T} \quad \quad
-        \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
-        \\
-        \Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
-        \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
+        \Delta, \Delta' | \Gamma, \expr{x} : \wcNtype{}{N} \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
-        \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
+        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T}
+        \Delta | \Gamma \vdash \texttt{let}\ \expr{x} = \expr{t}_1 \ \texttt{in} \ \expr{t}_2 : \type{T}
     \end{array}
 \end{array}$
 \\[1em]
@@ -271,9 +346,10 @@ $\begin{array}{l}
 $\begin{array}{l}
     \typerule{T-Method}\\
     \begin{array}{@{}c}
-        (\type{T'},\ol{T}) \to \type{T} \in \mathtt{\Pi}(\texttt{m})\quad \quad
-        \triangle' =  \overline{\type{Y} : \bot .. \type{P}} \quad \quad
-        \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \\
+        \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
         \text{dom}(\triangle) = \ol{X} \quad \quad
         %\texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \ \{ \ldots \} \\
         \mathtt{\Pi} | \triangle, \triangle' | \ol{x : T}, \texttt{this} : \exptype{C}{\ol{X}} \vdash \texttt{e} : \type{S} \quad \quad 
@@ -281,38 +357,33 @@ $\begin{array}{l}
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \text{ in C with } \generics{\ol{Y \triangleleft P}}
+        \mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) \set{ \texttt{return}\ \texttt{e}; } \ \ok \ \text{in C}
     \end{array}
 \end{array}$
 \\[1em]
 $\begin{array}{l}
     \typerule{T-Class}\\
     \begin{array}{@{}c}
-        \mathtt{\Pi}' = \mathtt{\Pi} \cup \set{ \texttt{m} : (\type{T'_m}, \ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M}} \quad \quad
-        \forall \texttt{m} \in \ol{M}: \Delta \vdash \exptype{C}{\ol{X}} <: \type{T'_m}\\
-        \mathtt{\Pi}'' = \mathtt{\Pi} \cup \set{ \texttt{m} :
-            \generics{\ol{X \triangleleft \type{N}}, \ol{Y \triangleleft P}}(\exptype{C}{\ol{X}},\ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M} } \\
+        %\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} \\
         \triangle = \overline{\type{X} : \bot .. \type{U}} \quad \quad
         \triangle \vdash \ol{U}, \ol{T}, \type{N} \ \ok \quad \quad
-        \mathtt{\Pi}' | \triangle \vdash \ol{M} \ \ok \text{ in C with} \ \generics{\ol{Y \triangleleft P}}
+        \mathtt{\Pi} | \triangle \vdash \ol{M} \ \ok \text{ in C}
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \}  : \mathtt{\Pi}''
+        \mathtt{\Pi} \vdash \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \} 
     \end{array}
 \end{array}$
-\\[1em]
+%\\[1em]
+\hfill
 $\begin{array}{l}
     \typerule{T-Program}\\
     \begin{array}{@{}c}
-        \emptyset \vdash \texttt{L}_1 : \mathtt{\Pi}_1 \quad \quad 
-        \mathtt{\Pi}_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 
+        \mathtt{\Pi} = \overline{\texttt{m} : \generics{\ol{X \triangleleft \type{N}}}\ol{T} \to \type{T}}
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \vdash \ol{L} : \mathtt{\Pi}_n
+    \mathtt{\Pi} \vdash \overline{D}
     \end{array}
 \end{array}$
 \end{center}
@@ -335,4 +406,5 @@ $\begin{array}{l}
         \text{fields}(\exptype{C}{\ol{T}}) = \ol{U\ g}, [\ol{T}/\ol{X}]\ol{S\ f}
     \end{array}
 \end{array}$
+\caption{Field access}
 \end{figure}

todo-11.4.24

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