Restructure and Cleanup Unify

modified:   relatedwork.tex

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)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% %Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\EventEditors{John Q. Open and Joan R. Access}
+% \EventEditors{John Q. Open and Joan R. Access}
-\EventNoEds{2}
+% \EventNoEds{2}
-\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
+% \EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
-\EventShortTitle{CVIT 2016}
+% \EventShortTitle{CVIT 2016}
-\EventAcronym{CVIT}
+% \EventAcronym{CVIT}
-\EventYear{2016}
+% \EventYear{2016}
-\EventDate{December 24--27, 2016}
+% \EventDate{December 24--27, 2016}
-\EventLocation{Little Whinging, United Kingdom}
+% \EventLocation{Little Whinging, United Kingdom}
-\EventLogo{}
+% \EventLogo{}
-\SeriesVolume{42}
+% \SeriesVolume{42}
-\ArticleNo{23}
+% \ArticleNo{23}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\begin{document}
 
 \maketitle
 
@@ -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}
+\subsection{Capture Constraints}
-% Our type inference algorithm is split into two parts.
+%TODO: General Capture Constraint explanation
-% A constraint generation step \textbf{TYPE} and a \unify{} step.
 
+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.
@@ -13,27 +77,105 @@
 % 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{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 same as in \cite{TIforFGJ} except for field access and method invocation.
+This step is mostly the same as in \cite{TIforFGJ} except for field access and method invocation.
-We will focus on those parts.
+We will focus on those two parts where also the new capture constraints and wildcard type placeholders are introduced.
-Here the new capture constraints and wildcard type placeholders are introduced.
 
-Generally subtype constraints for an expression mirror the subtype relations in the premise of the respective type rule introduced in section \ref{sec:tifj}
+%In \TamedFJ{} capture conversion is implicit.
-Unknown types at the time of the constraint generation step are replaced with type placeholders.
+%To emulate Java's behaviour we assume the input program not to contain any let statements.
-\begin{verbatim}
+%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){
-  let x = x in x.add(v)
+    return l.add(v);
 }
-\end{verbatim}
+\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}
 
-The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
+\begin{figure}
-Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
+    \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}
+
+\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.
@@ -42,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
@@ -68,42 +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*}
+  \center
-    % Type
+\begin{tabular}{lcll}
-    \type{T}, \type{U} &::= \tv{a} \mid \wtv{a} \mid \mv{X} \mid {\wcNtype{\Delta}{N}} && \text{types and type placeholders}\\
+    $C $ &$::=$ &$\overline{c}$ & Constraint set \\
-    \type{N} &::= \exptype{C}{\ol{T}} && \text{class type (with type variables)} \\
+    $c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \lessdotCC \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
-    % Constraints
+    $\type{T}, \type{U}, \type{L} $ & $::=$ & $\tv{a} \mid \gtype{G}$ & Type placeholder or Type \\
-    \constraint &::= \type{T} \lessdot \type{U} \mid \type{T} \lessdotCC \type{U} && \text{Constraint}\\
+    $\tv{a}$ & $::=$ & $\ntv{a} \mid \wtv{a}$ & Normal and wildcard type placeholder \\
-    \consSet &::= \set{\constraints} && \text{constraint set}\\
+    $\gtype{G}$ & $::=$ & $\type{X} \mid \ntype{N}$ & Wildcard, or Class Type \\
-    % Method assumptions:
+    $\ntype{N}, \ntype{S}$ & $::=$ & $\wctype{\triangle}{C}{\ol{T}} $ & Class Type \\
-    \methodAssumption &::= \texttt{m} : \exptype{}{\ol{Y}
+    $\triangle$ & $::=$ & $\overline{\wtype{W}}$ & Wildcard Environment \\
-                        \triangleleft \ol{P}}\ \ol{\type{T}} \to \type{T}  &&
+    $\wtype{W}$ & $::=$ & $\wildcard{X}{U}{L}$ & Wildcard \\
-                                                                \text{method
+\end{tabular}
-                                                                type assumption}\\
+  \caption{Syntax of types and constraints used by \fjtype{} and \unify{}}
-    \localVarAssumption &::= \texttt{x} : \itype{T} && \text{parameter
-                                                       assumption}\\
-    \mtypeEnvironment & ::= \overline{\methodAssumption} &
-                & \text{method type environment} \\
-    \typeAssumptionsSymbol &::= ({\mtypeEnvironment} ; \overline{\localVarAssumption}) 
-  \end{align*}
-  \caption{Syntax of constraints and type assumptions}
   \label{fig:syntax-constraints}
 \end{figure}
 
 \begin{figure}[tp]
   \begin{gather*}
     \begin{array}{@{}l@{}l}
-      \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\ol{X} \triangleleft \ol{N}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \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} & \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} } \\
-              \textbf{in} 
+              & \Delta = \set{ \overline{\wildcard{X}{\type{N}}{\bot}} } \\
-                  & \begin{array}[t]{l}
+              & 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}
+                  \end{array} \\
+              \textbf{in} 
+                  & (\Delta, C)
                 \end{array}
     \end{array}
   \end{gather*}
@@ -291,12 +415,12 @@ cannot be used anywhere else then inside the constraints generated by the method
     \typeExpr{} &({\mtypeEnvironment} , \texttt{new}\ \type{C}(\overline{e}), \tv{a}) = \\
                 & \begin{array}{ll}
                     \textbf{let} 
-                    & \ol{\tv{r}} \ \text{fresh} \\
+                    & \ol{\ntv{r}}, \ol{\ntv{a}} \ \text{fresh} \\
-                    & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \overline{e}, \ol{\tv{r}}) \\
+                    & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \overline{e}, \ol{\ntv{r}}) \\
-                    & C = \set{\ol{\tv{r}} \lessdot [\ol{\tv{a}}/\ol{X}]\ol{T}, \ol{\tv{a}} \lessdot \ol{N} \mid \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}} \\
+                    & C = \set{\ol{\ntv{r}} \lessdot [\ol{\ntv{a}}/\ol{X}]\ol{T}, \ol{\ntv{a}} \lessdot \ol{N} \mid \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}} \\
                     {\mathbf{in}} & {
                     \overline{\consSet} \cup
-                        \set{\tv{a} \doteq \exptype{C}{\ol{a}}}}
+                        \set{\tv{a} \doteq \exptype{C}{\ol{\ntv{a}}}}}
                   \end{array} 
   \end{array}
 \end{displaymath}

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},
@@ -65,14 +67,39 @@ 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={A. Martelli and U. Montanari},
+author = {Martelli, Alberto and Montanari, Ugo},
-    title={An Efficient Unification Algorithm},
+title = {An Efficient Unification Algorithm},
-    journal={ACM Transactions on Programming Languages and Systems},
+year = {1982},
-    volume={4},
+issue_date = {April 1982},
-    pages={258-282},
+publisher = {Association for Computing Machinery},
-    year={1982}}
+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},
@@ -466,3 +511,61 @@ 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

@@ -11,14 +11,21 @@
   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}
@@ -71,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}
 
@@ -97,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}}
@@ -105,7 +116,7 @@
 \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}}
@@ -121,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]{\ensuremath{\underline{\tv{#1}}}}
-\newcommand{\ntv}[1]{\tv{#1}}
+%\newcommand{\ntv}[1]{\tv{#1}}
 \newcommand{\wcstore}{\ensuremath{\Delta}}
 
 %\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}_?}}

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
 
@@ -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

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.
+\noindent
-The input language is designed to showcase type inference involving existential types.
+\textit{Notes:}
-Method call rule T-Call is the most interesting part, because it emulates the behaviour of a Java method call,
+\begin{itemize}
-where existential types are implicitly \textit{opened} and \textit{closed}.
+\item The calculus does not include method overriding for simplicity reasons.
-
-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.
 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.
+%\textit{Note:}
-\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}.
+\item The typing rules for expressions shown in figure \ref{fig:expressionTyping} refrain from restricting polymorphic recursion.
-Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
+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,200 +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 syntax forces every expression to undergo a capture conversion before it can be used as a method argument.
+% The output is a valid Featherweight Java program.
-Even variables have to be catched by a let statement first.
+% We use the syntax of the version introduced in \cite{WildcardsNeedWitnessProtection}
-This behaviour emulates Java's implicit capture conversion.
+% 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{\expr{x}}) = t \\
+\text{Method declarations} &  \texttt{M} & ::= & \highlight{\generics{\overline{\type{X} \triangleleft \type{N}}}}\ \highlight{\type{T}}\ \texttt{m}(\overline{\highlight{\type{T}}\ \expr{x}}) \{ \texttt{return} \ \expr{e}; \} \\
-\text{Terms} & t & ::= & \expr{x} \\
+\text{Terms} & \expr{e} & ::= & \expr{x} \\
-& & \ \ | &  \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}_c}) \\
+& & \ \ | & \texttt{new} \ \type{C}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
-& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \expr{x}_c.f \\
+& & \ \ | & \expr{e}.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}) \\
+& & \ \ | & \expr{e}.\texttt{m}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
-& & \ \ | & t \elvis{} t \\
+& & \ \ | & \texttt{let}\ \expr{x} \highlight{: \wcNtype{\Delta}{N}} = \expr{e} \ \texttt{in} \ \expr{e}\\
+& & \ \ | & \expr{e} \elvis{} \expr{e}\\
 \text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
-\hline
+%\hline
 \end{array}
 $
-\caption{\TamedFJ{} Syntax}\label{fig:syntax}
+\par\noindent\rule{\textwidth}{0.4pt}
+\caption{Input Syntax with optional type annotations}\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}
@@ -289,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}\\
@@ -460,18 +308,15 @@ $\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} : \wctype{}{C}{\ol{X}} \vdash \expr{t}_2 : \type{T}_2 \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
+        \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
+        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok
         \\
         \hline
     \vspace*{-0.3cm}\\
@@ -501,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
+        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\ldots} \quad \quad 
-        \triangle' =  \overline{\type{Y} : \bot .. \type{P}} \quad \quad
+        \generics{\ol{Y \triangleleft \type{N}}}(\exptype{C}{\ol{X}},\ol{T}) \to \type{T} \in \mathtt{\Pi}(\texttt{m}) \quad \quad
-        \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \\
+        \triangle' =  \overline{\type{Y} : \bot .. \type{P}} \\
+        \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \quad \quad
         \text{dom}(\triangle) = \ol{X} \quad \quad
         %\texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \ \{ \ldots \} \\
         \mathtt{\Pi} | \triangle, \triangle' | \ol{x : T}, \texttt{this} : \exptype{C}{\ol{X}} \vdash \texttt{e} : \type{S} \quad \quad 
@@ -511,37 +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} : (\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} \\
-        \mathtt{\Pi}'' = \mathtt{\Pi} \cup \set{ \texttt{m} :
-            \generics{\ol{X \triangleleft \type{N}}, \ol{Y \triangleleft P}}(\exptype{C}{\ol{X}},\ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M} } \\
         \triangle = \overline{\type{X} : \bot .. \type{U}} \quad \quad
         \triangle \vdash \ol{U}, \ol{T}, \type{N} \ \ok \quad \quad
-        \mathtt{\Pi}' | \triangle \vdash \ol{M} \ \ok \text{ in C with} \ \generics{\ol{Y \triangleleft P}}
+        \mathtt{\Pi} | \triangle \vdash \ol{M} \ \ok \text{ in C}
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \}  : \mathtt{\Pi}''
+        \mathtt{\Pi} \vdash \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \} 
     \end{array}
 \end{array}$
-\\[1em]
+%\\[1em]
+\hfill
 $\begin{array}{l}
     \typerule{T-Program}\\
     \begin{array}{@{}c}
-        \emptyset \vdash \texttt{L}_1 : \mathtt{\Pi}_1 \quad \quad 
+        \mathtt{\Pi} = \overline{\texttt{m} : \generics{\ol{X \triangleleft \type{N}}}\ol{T} \to \type{T}}
-        \mathtt{\Pi}_1 \vdash \texttt{L}_2 : \mathtt{\Pi}_1 \quad \quad 
-        \ldots \quad \quad 
-        \mathtt{\Pi}_{n-1} \vdash \texttt{L}_n : \mathtt{\Pi}_n \quad \quad 
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \vdash \ol{L} : \mathtt{\Pi}_n
+    \mathtt{\Pi} \vdash \overline{D}
     \end{array}
 \end{array}$
 \end{center}

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)