Comments

.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

@@ -36,6 +36,7 @@
 \usepackage{cancel}
 \usepackage{tcolorbox}
 \usepackage{arydshln}
+\usepackage{dashbox}
 
 \input{prolog}
 
@@ -101,126 +102,7 @@ TODO: Abstract
 
 \input{introduction}
 
-%We could do a translation from Java to \wildFJ explaining implicit capture conversion
-
-\section{Soundness of Typing}
-
-
-We show soundness with the type rules statet in \cite{WildcardsNeedWitnessProtection}.
-A correct \FGJGT{} program can be converted to a correct \wildFJ{} program.
-
-\begin{figure}
-$\begin{array}{rcl}
-    | \texttt{x} |
-    & = & \texttt{x} \\
-    | \texttt{let} \ \texttt{x} : \type{T} = \texttt{e},\, \ol{x} : \ol{T} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x}) |
-    & = & |\texttt{e}|.\texttt{m}(\ol{|e|}) \\
-    | \texttt{let} \ \texttt{x} : \type{T} = \texttt{e}\ \texttt{in}\ \texttt{x}.\texttt{f} |
-    & = & |\texttt{e}|.\texttt{f} \\
-    | \texttt{e} \elvis{} \texttt{e} |
-    & = & |\texttt{e}| \elvis{} |\texttt{e}| \\
-\end{array}$
-\caption{Erasure} \label{fig:erasure}
-\end{figure}
-
-% A constraint Pair<A,B> <. a, then a has infinite possibilities:
-% a =. X.Pair<X,X>
-% a =. X,Y.Pair<X,Y>
-% a =. X.Pair<Pair<X,X>,X>
-% a =. X,Y.Pair<Pair<X,Y>,X>
-% a =. X,Y.Pair<Pair<X,Y>,Y>
-
-% There is no way to try out every single one of them.
-
-Starting with the parameters of the method we gradually add every expression which only contains already captured expressions.
-
-We have a typed expression
-
-$|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} : \type{T} = \texttt{x in}$
-$|\texttt{e.f}, \texttt{r}| = |\texttt{e}, x| \texttt{let} r = x.\texttt{f} \ \texttt{in}$ 
-$|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} = \texttt{x in}$
-%TODO: write the transform rules:
-% |e.f, ret| = |e, r| let ret = r.f in
-% |x, ret| = let ret = x in
-% |e.m(e_), ret| = |e, r| |e_, a_| let ret = r.m(a_) in
-
-Erasure functions:
-$|\texttt{x}| = \texttt{let r} : \wcNtype{\Delta}{N} = \texttt{x in r}$
-
-$\texttt{x} \longmapsto \texttt{let}\ \texttt{xx} : \type{T} = \texttt{x in xx}$
-$\texttt{x}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in xf}$
-
-$\begin{array}{l}
-\texttt{e} \longmapsto \texttt{let}\ \texttt{xe} : \type{T} = \texttt{e}' \ \texttt{in xe} \\ 
-\hline
-\vspace*{-0.4cm}\\
-\texttt{e}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in x}.f
-\end{array}$
-
-Example:
-m(a, b) = a.m(b.f);
-
-let xa = a in let xb = b in let xf = xb.f in let xm = xa.m(xf) in xm
-
-% TODO: Now we have to proof that there is a LetFJ program for every TIFJ program!
-% |let xr : T = x1.m(x2) in e| = [x1.m(x2)/xr]|e| 
-% |let xf : T = x1.f in e| = [x1.f/xf]|e|
-% |let xr : T = x in e| = [xr/x]|e|
-% |new C(x)| = new C(x)
-
-% | let xr : T' = x in let xf : T = xr.f | = x.f
-
-
-% let x : T' = e' in x = |e|
-% ---------------------------------
-% | let xr : T' = x in let xf : T = xr.f | = x.f
-
-
-
-% let x : T' = e' in x = |e|
-% -----------
-% = 
-
-We need a language which only has let statemnts and expressions on capture converted variables
-
-The idea is to use wildcard placeholders inside the method. Also in the bounds of wildcards.
-This makes it possible to replace wildcards with free variables by setting upper and lower bound to that free variable.
-Free variables then can flow freely inside the method body.
-We have to show that a type solution implies that there is a possible transformation to a correct typed letFJ program.
-If there is a possible method type then there must exist a let configuration.
-% By starting with the parameter types and capturing them. Afterwards every capture creates free variables which are used inside
-% TODO: Proof!
-
-The normal type placeholders represent denotable types.
-
-%TODO: the type rules stay the same. We generate let statements in a fashion which removes all wildcard types.
-% what about wildcards getting returned by untyped methods? they can also be captured
-% TODO: try soundness proof on the original type rules!
-
-Removing of extensive wildcards:
-$
-\wctype{\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{X}, \rwildcard{Y}}
-\lessdot \wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}} \\
-\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \wtv{x}, \rwildcard{Y} \doteq \wtv{x} \\
-\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \rwildcard{Y} \\
-\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
-\implies \wctype{\wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{Y}, \rwildcard{Y}}, \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
-$
-
-%e.f leads to constraints: r <c C<x> with return type equals the field type T.
-%   T can contain free variables from r. but also it can be used in another constraint and get free variables from inner let statements
-%   X.C<X> <c C<x> -> then T contains X variables
-
-% let x1 = p1, x2 = p2 in
-%  let r1  = x1 in let r2 = p2 in let f1 = r2.f in let r3 = x1 in let m2 = r3.m2() let ret = r1.m(f1,m2)
-%   in ret
-
-What about method invocation with no type yet. m2 :: a -> a 
-they are also encased in let expression so the return type can be capture converted.
-Those methods and the parameter types of the current method are the only things not typed.
-All the other types cannot change their type. The captured wildcards can only flow from top to bottom.
-The return type of untyped methods has to be well-formed and cannot contain free variables.
-Therefore no free variables will flow into those types.
+%\input{letfjTransformation}
 
 \input{tRules}
 
@@ -228,172 +110,6 @@ Therefore no free variables will flow into those types.
 
 \input{constraints}
 
-\section{Capture Conversion}
-The input to our type inference algorithm does not contain let statements.
-Those are added after computing a type solution.
-Let statements act as capture conversion and only have to be applied in method calls involving wildcard types.
-
-\begin{figure} 
-  \begin{minipage}{0.45\textwidth}
-\begin{lstlisting}[style=fgj]
-<X> List<X> clone(List<X> l);
-example(p){
-  return clone(p);
-}
-\end{lstlisting}
-    \end{minipage}%
-    \hfill
-    \begin{minipage}{0.5\textwidth}
-\begin{lstlisting}[style=tfgj]
-(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){
-  return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in
-   clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
-}
-\end{lstlisting}
-    \end{minipage}
-\caption{Type inference adding capture conversion}\label{fig:addingLetExample}
-  \end{figure}
-
-Figure \ref{fig:addingLetExample} shows a let statement getting added to the typed output.
-The method \texttt{clone} cannot be called with the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
-After a capture conversion \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$ with $\rwildcard{X}$ being a free variable.
-Afterwards we have to find a supertype of $\exptype{List}{\rwildcard{X}}$, which does not contain free variables
-($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in this case).
-
-During the constraint generation step most types are not known yet and are represented by a type placeholder.
-During a methodcall like the one in the \texttt{example} method in figure \ref{fig:ccExample} the type of the parameter \texttt{p}
-is not known yet.
-The type \texttt{List<?>} would be one possibility as a parameter type for \texttt{p}.
-To make wildcards work for our type inference algorithm \unify{} has to apply capture conversions if necessary.
-
-The type placeholder $\tv{r}$ is the return type of the \texttt{example} method.
-One possible type solution is $\tv{p} \doteq \tv{r} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$,
-which leads to:
-\begin{verbatim}
-List<?> example(List<?> p){
-  return clone(p);
-}
-\end{verbatim}
-
-But by substituting $\tv{p} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in the constraint
-$\tv{p} \lessdot \exptype{List}{\wtv{x}}$ leads to
-$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{x}}$.
-
-To make this typing possible we have to introduce a capture conversion via a let statement:
-$\texttt{return}\ (\texttt{let}\ \texttt{x} : \wctype{\rwildcard{X}}{List}{\rwildcard{X}} = \texttt{p}\ \texttt{in} \
-\texttt{clone}\generics{\rwildcard{X}}(x) : \wctype{\rwildcard{X}}{List}{\rwildcard{X}})$
-
-Inside the let statement the variable \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$
-
-$
-\begin{array}[c]{l}
-\wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \rwildcard{G}}\\
-                   \hline
-[\type{G}/\wtv{a}]\wildcardEnv \vdash [\type{G}/\wtv{a}]C  \cup \set{\tv{a} \doteq \type{G}} 
-\end{array}
-$
-
-This spawns additional problems.
-%TODO
-%we need the constraint set to be a list
-%not on every constraint CC is allowed. The unify algorithm does not know the context in which a constraint was generated
-%free type variables cannot leave the scope of the method call
-
-\begin{figure} 
-\begin{minipage}{0.45\textwidth}
-\begin{verbatim}
-<X> List<X> clone(List<X> l){...}
-
-example(p){
-  return clone(p);
-}
-\end{verbatim}
-  \end{minipage}%
-  \hfill
-  \begin{minipage}{0.35\textwidth}
-\begin{constraintset}
-    \textbf{Constraints:}\\
-    $
-  \tv{p} \lessdot \exptype{List}{\wtv{x}}, \\
-\tv{p} \lessdot \tv{r}, \\
-\tv{p} \lessdot \type{Object}, 
-\tv{r} \lessdot \type{Object}
-    $
-\end{constraintset}
-  \end{minipage}
-
-\caption{Type inference example}\label{fig:ccExample}
-\end{figure}
-
-In addition with free variables this leads to unwanted behaviour.
-Take the constraint
-$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ for example.
-After a capture conversion from $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ to $\exptype{List}{\rwildcard{Y}}$ and a substitution $\wtv{a} \doteq \rwildcard{Y}$
-we get
-$\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$.
-Which is correct if we apply capture conversion to the left side:
-$\exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$
-If the input constraints did not intend for this constraint to undergo a capture conversion then \unify{} would produce an invalid
-type solution due to:
-$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \nless: \exptype{List}{\rwildcard{X}}$
-The reason for this is the \texttt{S-Exists} rule's premise
-$\text{dom}(\Delta') \cap \text{fv}(\exptype{List}{\rwildcard{X}}) = \emptyset$.
-
-Additionally free variables are not allowed to leave the scope of a capture conversion
-introduced by a let statement.
-%TODO we combat both of this with wildcard type placeholders (? flag)
-
-Type placeholders which are not flagged as possible free variables ($\wtv{a}$) can never hold a free variable or a type containing free variables.
-Constraint generation places these standard place holders at method return types and parameter types.
-\begin{lstlisting}[style=fgj]
-<X> List<X> clone(List<X> l);
-(*@$\red{\tv{r}}$@*) example((*@$\red{\tv{p}}$@*) p){
-  return clone(p);
-}
-\end{lstlisting}
-This prevents type solutions that contain free variables in parameter and return types.
-When calling a method which already has a type annotation we have to consider adding a capture conversion in form of a let statement.
-The constraint $\tv{p} \lessdot \exptype{List}{\wtv{x}}$ signals the \unify{} algorithm that here a capture conversion is possible.
-$\sigma(\tv{p}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, \sigma(\tv{r}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, $ is a possible solution.
-But only when adding a capture conversion:
-\begin{lstlisting}[style=fgj]
-<X> List<X> clone(List<X> l);
-(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){
-  return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
-}
-\end{lstlisting}
-\unify{}'s type solution for constraints involving free variables only holds under special circumstances.
-Constraint $\tv{p} \lessdot \exptype{List}{\wtv{x}}$ only holds when a capture conversion is applied to the left side:
-$\Delta, \Delta' \vdash CC(\sigma(\tv{p})) <: \sigma(\exptype{List}{\wtv{x}})$
-and there is a an environment $\Delta'$ holding all type variables used inside the subtype relation.
-This is done by packing the method call inside a let statement, which performs a capture conversion on all expressions used as parameters.
-%TODO: Explain (do soundness and TYPE algorithm first)
-
-A type solution of the \unify{} algorithm only guarantees correct subtyping for constraints not containing free variables.
-Constraints like $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ only guarantee
-$\Delta, \Delta' \vdash \sigma(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) <: \sigma(\exptype{List}{\wtv{a}})$ when
-adding a $\Delta'$ environment and applying a capture conversion on the left side.
-In this case the type solution would be $\tv{a} \to \rwildcard{X}$ leading to:
-$\Delta, \set{\rwildcard{X}} \vdash \exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$
-
-This is the reason input constraints containing free variables cannot be stored in a set.
-$\wtv{a} \lessdot \wtv{b}$ is not the same as $\wtv{a} \lessdot \wtv{b}$.
-Both constraints will end up the same after a substitution for both placeholders $\tv{a}$ and $\tv{b}$.
-But afterwards a capture conversion is applied, which can generate different types on the left sides.
-\begin{itemize}
-  \item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Y}}$ 
-  \item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Z}}$ 
-\end{itemize}
-
-
-Also the subtype relation is not symmetric for types involving free type variables.
-$\type{T} \lessdot \type{S}$ and $\type{S} \lessdot \type{T}$ doesnt mean $\type{T} = \type{S}$, because we apply a capture conversion on every constraint.
-Only for constraints without free variables symmetry is given.
-
-% Can untyped methods also get a capture conversion? NO!
-
-%TODO: Explain why capture conversion is needed (also in respect to martins algorithm)
-
 \input{Unify}
 
 \section{Limitations}

constraints.tex

@@ -9,9 +9,32 @@
 
 %\subsection{Well-Formedness}
 
+
+% 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
+
+The constraint generation works on the \TamedFJ{} language.
+This step is mostly same as in \cite{TIforFGJ} except for field access and method invocation.
+We will focus on those parts.
+Here the new capture constraints and wildcard type placeholders are introduced.
+
+Generally subtype constraints for an expression mirror the subtype relations in the premise of the respective type rule introduced in section \ref{sec:tifj}
+Unknown types at the time of the constraint generation step are replaced with type placeholders.
+\begin{verbatim}
+m(l, v){
+  let x = x in x.add(v)
+}
+\end{verbatim}
+
 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.
+
 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.
 Here captured variables can flow freely.
@@ -48,14 +71,12 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
   \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)} \\
+    \type{N} &::= \exptype{C}{\ol{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}\\
+    \constraint &::= \type{T} \lessdot \type{U} \mid \type{T} \lessdotCC \type{U} && \text{Constraint}\\
     \consSet &::= \set{\constraints} && \text{constraint set}\\
     % Method assumptions:
-    \methodAssumption &::= \exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \exptype{}{\ol{Y}
+    \methodAssumption &::= \texttt{m} : \exptype{}{\ol{Y}
                         \triangleleft \ol{P}}\ \ol{\type{T}} \to \type{T}  &&
                                                                 \text{method
                                                                 type assumption}\\
@@ -65,28 +86,24 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
                 & \text{method type environment} \\
     \typeAssumptionsSymbol &::= ({\mtypeEnvironment} ; \overline{\localVarAssumption}) 
   \end{align*}
-  \caption{Syntax of constraints and type assumptions.}
+  \caption{Syntax of constraints and type assumptions}
   \label{fig:syntax-constraints}
 \end{figure}
 
 \begin{figure}[tp]
   \begin{gather*}
     \begin{array}{@{}l@{}l}
-      \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\ol{X} \triangleleft \ol{N}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, K \, \overline{M} \}}) =\\
+      \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\ol{X} \triangleleft \ol{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} } \\
+              \textbf{in} 
+                  & \begin{array}[t]{l}
+                \set{ \typeExpr(\mtypeEnvironment \cup \ol{\methodAssumption} \cup \set{\mv{this} :
+              \exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}} }, \texttt{e}, \tv{a})
+               \\ \quad \quad \quad \quad \mid \set{ \mv{m}(\ol{x}) = \expr{e} }  \in \ol{M},\, \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \in \ol{\methodAssumption}}
+                  \end{array}
                 \end{array}
     \end{array}
   \end{gather*}
@@ -94,39 +111,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}) = \\
@@ -138,7 +122,8 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
                       \orCons\set{
                       \set{ &
                       \tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}} ,
-                      [\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} , \ol{\wtv{a}} \lessdot [\overline{\wtv{a}}/\ol{X}]\ol{N}
+                      [\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} ,
+                      \ol{\wtv{a}} \lessdot [\overline{\wtv{a}}/\ol{X}]\ol{N}
                       } \\
                       & \quad \mid \mv{T}\ \mv{f} \in \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}
                         , \, \overline{\wtv{a}} \text{ fresh}
@@ -149,203 +134,134 @@ 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.
-
-LetFJ version: %TODO: or use the old version with \lessdotCC constraints. then there is no problem with \Delta'
-% or only use the \lessdotCC with X.C<X> and C<X> on both sides
-% what to do with ? <c X constraints? Just ignore them! they result in X <. X and can be ignored
-% generate a function which converts method types and parameter types to constraints of the form a <. X.C<X>, C<X> <. C<x>
-% add the free variables to \Delta' proof that they cannot escape the scope (they have to be treated differently than \Delta')
 \begin{displaymath}
   \begin{array}{@{}l@{}l}
-      \typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}})) = \\
-      & \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}
-                    %TODO: add \ol{\wildcard{X}{\wtv{u}}{\wtv{l}}} to \Delta'
-                    [\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdot \wctype{\ol{\wildcard{X}{\wtv{u}}{\wtv{l}}}}{C}{\ol{X}},  \exptype{C}{\ol{X}} \lessdot \exptype{C}{\ol{X}},
-                    %[\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdotCC \exptype{C}{\ol{X}},
-                    \overline{\tv{r}} \lessdot \ol{T},
-                    \ol{X} \lessdot \ol{N}, 
-                    \ol{Y} \lessdot \ol{N'} \}
-                  \end{array}\\
-            & \ |\ 
-            (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\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}, \, \overline{\wtv{b}} \text{ fresh} }
-        \end{array}\\
-      \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T})
-      \end{array}
-      \end{array}
-  \end{displaymath}
-
-Java version:
-\begin{displaymath}
-  \begin{array}{@{}l@{}l}
-      \typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}})) = \\
-      & \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} \lessdot \wctype{\ol{\wildcard{X}{\ntv{u}}{\ntv{l}}}}{C}{\ol{X}},  \wctype{\ol{\wildcard{X}{\ntv{u}}{\ntv{l}}}}{C}{\ol{X}} \lessdotCC \exptype{C}{\ol{X}},
-                    [\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdotCC \exptype{C}{\ol{X}},
-                    \overline{\tv{r}} \lessdotCC \ol{T},
-                    \ol{X} \lessdot \ol{N}, 
-                    \ol{Y} \lessdot \ol{N'} \}
-                  \end{array}\\
-            & \ |\ 
-            (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\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}, \, \overline{\wtv{b}} \text{ fresh} }
-        \end{array}\\
-      \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T})
-      \end{array}
-      \end{array}
-  \end{displaymath}
-% \begin{displaymath}
-%       \typeExpr{}' ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a} ) = \
-%       \typeExpr{} ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \wtv{b} ) \cup \set{ \wtv{b} \lessdot \tv{a}}
-%   \end{displaymath}
-
-\begin{displaymath}
-  \typeExpr{}' ({\mtypeEnvironment} , \texttt{return e;}, \tv{a} ) = \
-  \typeExpr{} ({\mtypeEnvironment} , \texttt{e}, \wtv{b} ) \cup \set{ \wtv{b} \lessdot \tv{a}} \quad \quad \tv{a}, \wtv{b} \ \text{fresh}
+    \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} ) = \\
-%     & \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} \lessdot \exptype{C}{\ol{X}},
-%                   \overline{\tv{r}} \lessdot \ol{T},
-%                   \type{T} \lessdot \tv{a}, 
-%                   \ol{X} \lessdot \ol{N}, 
-%                   \ol{Y} \lessdot \ol{N'} \}
-%                 \end{array}\\
-%           & \ |\ 
-%           (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N'}}\overline{\type{T}} \to \type{T}) \in 
-%               {\mtypeEnvironment}
-%           , \, \overline{\wtv{a}} \text{ fresh}, \, \overline{\wtv{b}} \text{ fresh} }
-%       \end{array}\\
-%     \mathbf{in} & \consSet_R \cup \overline{\consSet} \cup \constraint
-%     \end{array}
-%     \end{array}
-% \end{displaymath}
+
+\begin{displaymath}
+  \begin{array}{@{}l@{}l}
+      \typeExpr{} & ({\mtypeEnvironment} , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\
+      & \begin{array}{ll}
+      \textbf{let}
+      & \tv{r}, \ol{\tv{r}} \text{ fresh} \\
+      & \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}
 \\[1em]
 \noindent
 \textbf{Example:}
 \begin{verbatim}
 class Class1{
-  <X> X m(List<X> lx, List<? extends X> lt){ ... }
-  List<? extends String> wGet(){ ... }
-  List<String> get() { ... }
+  <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}

introduction.tex

@@ -7,55 +7,53 @@
 \section{Type Inference for Java}
 %The goal is to find a correct typing for a given Java program.
 Type inference for Java has many use cases and could be used to help programmers by inserting correct types for them,
-Finding better type solutions for already typed Java programs (for example more generical ones),
+finding better type solutions for already typed Java programs (for example more generical ones),
 or allowing to write typeless Java code which is then type infered and thereby type checked by our algorithm.
 The algorithm proposed in this paper can determine a correct typing for the untyped Java source code example shown in figure \ref{fig:intro-example-typeless}.
 Our algorithm is also capable of finding solutions involving wildcards as shown in figure \ref{fig:intro-example-typed}.
 
 %This paper extends a type inference algorithm for Featherweight Java \cite{TIforFGJ} by adding wildcards.
 %The last step to create a type inference algorithm compatible to the Java type system.
-The algorithm presented in this paper is a slightly improved version of the one in \cite{TIforFGJ} including wildcard support.
+The algorithm presented in this paper is a improved version of the one in \cite{TIforFGJ} including wildcard support.
 %a modified version of the \unify{} algorithm presented in \cite{plue09_1}.
 The input to the type inference algorithm is a Featherweight Java program (example in figure \ref{fig:nested-list-example-typeless}) conforming to the syntax shown in figure \ref{fig:syntax}.
 The \fjtype{} algorithm calculates constraints based on this intermediate representation,
 which are then solved by the \unify{} algorithm
 resulting in a correctly typed program (see figure \ref{fig:nested-list-example-typed}).
 
+\begin{itemize}
+\item
+We introduce the language \tifj{} (chapter \ref{sec:tifj}).
+A Featherweight Java derivative including Generics, Wildcards and Type Inference.
+\item
 We support capture conversion and Java style method calls.
 This requires existential types in a form which is not denotable by Java syntax \cite{aModelForJavaWithWildcards}.
-The algorithm is able find the correct type for the method \texttt{m} in the following example:
-\begin{verbatim}
-    <X> Pair<X,X> make(List<X> l)
-    Boolean compare(Pair<X,X> p)
-
-    List<?> b;
-    Boolean m() = this.compare(this.make(b));
-\end{verbatim}
-
-
+\item
 We present a novel approach to deal with existential types and capture conversion during constraint unification.
-The algorithm is split in two parts. A constraint generation step and an unification step.
-
+\item The algorithm is split in two parts. A constraint generation step and an unification step.
+Input language and constraint generations can be extended without altering the unification part.
+\item
 We proof soundness and aim for a good compromise between completeness and time complexity.
-Our algorithm finds a correct type solution for the following example, where the Java local type inference fails:
-\begin{verbatim}
-class SuperPair<A,B>{
-    A a;
-    B b;
-}
-class Pair<A,B> extends SuperPair<B,A>{
-    A a;
-    B b;
+\end{itemize}
+% Our algorithm finds a correct type solution for the following example, where the Java local type inference fails:
+% \begin{verbatim}
+% class SuperPair<A,B>{
+%     A a;
+%     B b;
+% }
+% class Pair<A,B> extends SuperPair<B,A>{
+%     A a;
+%     B b;
 
-    <X> X choose(X a, X b){ return b; }
+%     <X> X choose(X a, X b){ return b; }
 
-    String m(List<? extends Pair<Integer, String>> a, List<? extends Pair<Integer, String>> b){
-        return choose(choose(a,b).value.a,b.value.b);
-    }
-}
-\end{verbatim}
+%     String m(List<? extends Pair<Integer, String>> a, List<? extends Pair<Integer, String>> b){
+%         return choose(choose(a,b).value.a,b.value.b);
+%     }
+% }
+% \end{verbatim}
 
-\begin{figure}[tp]
+\begin{figure}%[tp]
       \begin{subfigure}[t]{\linewidth}
 \begin{lstlisting}[style=fgj]
 class List<A> {
@@ -120,12 +118,7 @@ class Example {
       %\label{fig:intro-example-code}
 \end{figure}
 
-
-%TODO
-% The goal is to proof soundness in respect to the type rules introduced by \cite{aModelForJavaWithWildcards}
-% and \cite{WildcardsNeedWitnessProtection}.
-
-\begin{figure}[tp]
+\begin{figure}%[tp]
       \begin{subfigure}[t]{0.49\linewidth}
     \begin{lstlisting}[style=fgj]
 genList() {
@@ -165,83 +158,18 @@ List<?> genList() {
 % \texttt{List<Object>} is not a valid return type for the method \texttt{genList}.
 % The type inference algorithm has to find the correct type involving wildcards (\texttt{List<?>}).
 
-\subsection{Global Type Inference}
-A global type inference algorithm works on an input with no type annotations at all.
-%TODO: Describe global type inference and lateron why it is so hard to 
-Global type inference means that there are no type annotations at all.
-\begin{verbatim}
-m(l) {
-    return l.add(l);
-}
-\end{verbatim}
-
-$\tv{l} \lessdotCC \exptype{List}{\wtv{x}}, \tv{l} \lessdotCC \wtv{x}$
-
-
-No capture conversion for methods in the same class:
-Given two methods without type annotations like
-\begin{verbatim}
-// m :: () -> r
-m() = new List<String>() :? new List<Integer>();
-
-// id :: (a) -> a
-id(a) = a
-\end{verbatim}
-
-and a method call \texttt{id(m())} would lead to the constraints:
-$\exptype{List}{\type{String}} \lessdot \ntv{r},
-\exptype{List}{\type{Integer}} \lessdot \ntv{r},
-\ntv{r} \lessdot \ntv{a}$
-
-In this example capture conversion is not applicable,
-because the \texttt{id} method is not polymorphic.
-The type solution provided by \unify{} for this constraint set is:
-$\sigma(\ntv{r}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, 
-\sigma(\ntv{a}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$
-\begin{verbatim}
-List<?> m() = new List<String>() :? new List<Integer>();
-List<?> id(List<?> a) = a
-\end{verbatim}
-
-The following example has the \texttt{id} method already typed and the method \texttt{m}
-extended by a recursive call \texttt{id(m())}:
-\begin{verbatim}
-<A> List<A> id(List<A> a) = a
-
-m() = new List<String>() :? new List<Integer>() :? id(m());
-\end{verbatim}
-Now the constraints make use of a $\lessdotCC$ constraint:
-$\exptype{List}{\type{String}} \lessdot \ntv{r},
-\exptype{List}{\type{Integer}} \lessdot \ntv{r},
-\ntv{r} \lessdotCC \exptype{List}{\wtv{a}}$
-
-After substituting $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\ntv{r}$ like in the example before
-we get the constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$.
-Due to the $\lessdotCC$ \unify{} is allowed to perform a capture conversion yielding
-$\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
-\textit{Note:} The wildcard placeholder $\wtv{a}$ is allowed to hold free variables whereas a normal placeholder like $\ntv{r}$
-is never assigned a type containing free variables.
-Therefore \unify{} sets $\wtv{a} \doteq \rwildcard{X}$, completing the constraint set and resulting in the type solution:
-\begin{verbatim}
-List<?> m() = new List<String>() :? new List<Integer>() :? id(m());
-\end{verbatim}
-
-
 \subsection{Java Wildcards}
-Wildcards are expressed by a \texttt{?} in Java and can be used as parameter types.
-Wildcards can be formalized as existential types \cite{WildFJ}.
-\texttt{List<? extends Object>} and \texttt{List<? super String>} are both wildcard types
-denoted in our syntax by $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$ and
-$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
-
+Wildcards are expressed by a \texttt{?} in Java and can be used as type parameters.
 Wildcards add variance to Java type parameters.
 Generally Java has invariant subtyping for polymorphic types.
 A \texttt{List<String>} is not a subtype of \texttt{List<Object>} for example
 even though it seems intuitive with \texttt{String} being a subtype of \texttt{Object}.
 
+Wildcards can be formalized as existential types \cite{WildFJ}.
+\texttt{List<? extends Object>} and \texttt{List<? super String>} are both wildcard types
+denoted in our syntax by $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$ and
+$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
 
-$\exptype{List}{String} <: \wctype{\wildcard{X}{\bot}{\type{Object}}}{List}{\rwildcard{X}}$
-means \texttt{List<String>} is a subtype of \texttt{List<? extend Object>}.
 The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound at the same time,
 and a type they are bound to.
 In this case the name is $\rwildcard{X}$ and it's bound to the the type \texttt{List}.
@@ -249,63 +177,301 @@ In this case the name is $\rwildcard{X}$ and it's bound to the the type \texttt{
 Those properties are needed to formalize capture conversion.
 Polymorphic method calls need to be wraped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}.
 In Java this is done implicitly in a process called capture conversion.
-When calling a polymorphic method like \texttt{<X> List<X> m(List<X> l1, List<X> l2)} with a \texttt{List<?>}
-it is not possible to substitute \texttt{?} for \texttt{X}.
-This would lead to the method header \texttt{List<?> m(List<?> l1, List<?> l2)}
-where now a method invocation with \texttt{List<String>} and \texttt{List<Integer>} would be possible,
-because both are subtypes of \texttt{List<?>}.
-Capture conversion solves this problem by generating a fresh type variable for every wildcard.
-Calling \texttt{<X> X head(List<X> l1)} with the type \texttt{List<?>} ($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$)
-creates a fresh type variable $\rwildcard{Y}$ resulting in 
-$\generics{\rwildcard{Y}}\texttt{head}(\exptype{List}{\rwildcard{Y}})$
-with $\rwildcard{Y}$ being used as generic parameter \texttt{X}.
-The $\rwildcard{Y}$ in $\exptype{List}{\rwildcard{Y}}$ is a free variable now.
 
-%TODO: Read taming wildcards and see if we solve some of the problems presented in section 5 and 6
+%show input and a correct letFJ representation
+%TODO: first show local type inference and explain lessdotCC constraints. then show example with global TI
+\begin{figure}[h]
+\begin{subfigure}[t]{0.47\textwidth}
+\centering
+\begin{lstlisting}[style=tfgj, caption=Valid Java program, label=lst:addExample]
+<A> List<A> add(List<A> l, A v) ...
 
-% Additionally they can hold a upper or lower bound restriction like \texttt{List<? super String>}.
-% Our representation of this type is: $\wctype{\wildcard{X}{\type{String}}{\type{Object}}}{List}{\rwildcard{X}}$
-% Every wildcard has a name ($\rwildcard{X}$ in this case) and an upper and lower bound (respectively \texttt{Object} and \texttt{String}).
+List<? super String> l = ...;
+add(l, "String");
+\end{lstlisting}
+\end{subfigure}\hfill
+\begin{subfigure}[t]{0.47\textwidth}
+\centering
+\begin{lstlisting}[style=letfj, caption=\letfj{} representation, label=lst:addExampleLet]
+<A> List<A> add(List<A> l, A v)
 
-% \subsection{Extensibility} % NOTE: this thing is useless, because final local variables do not need to contain wildcards
-% In \cite{WildcardsNeedWitnessProtection} capture converson is made explicit with \texttt{let} statements.
-% We chain let statements in a way that emulates Java behaviour. Allowing the example in \cite{aModelForJavaWithWildcards}
-% % TODO: Explain the advantage of constraints and how we control the way capture conversion is executed
-% But it would be also possible to alter the constraint generation step to include additional features.
-% Final variables or effectively final variables could be expressed with a 
+let l2 : (*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = l
+    in <X>add(l2, "String");
+\end{lstlisting}
+\end{subfigure}
+\end{figure}
+
+The Example in listing \ref{lst:addExample} is a valid Java program. Here Java uses local type inference \cite{JavaLocalTI}
+to determine the type parameters to the \texttt{add} method call.
+In \letfj{} there is no local type inference and all type parameters for a method call are mandatory (see listing \ref{lst:addExampleLet}).
+If wildcards are involved the so called capture conversion has to be done manually via let statements.
+%A let statement \emph{opens} an existential type.
+In the body of the let statement the \textit{capture type} $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$
+becomes $\exptype{List}{\rwildcard{X}}$ and the wildcard $\wildcard{X}{\type{Object}}{\type{String}}$ is free and can be used as
+a type parameter to \texttt{<X>add(...)}.
+%This is a valid Java program where the type parameters for the polymorphic method \texttt{add}
+%are determined by local type inference.
+
+One problem is the divergence between denotable and expressable types in Java \cite{semanticWildcardModel}.
+A wildcard in the Java syntax has no name and is bound to its enclosing type:
+$\exptype{List}{\exptype{List}{\type{?}}}$ equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
+During type checking \emph{intermediate types}
+%like $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$
+%or $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$
+can emerge, which have no equivalent in the Java syntax.
+%Our type inference algorithm uses existential types internally but spawns type solutions compatible with Java.
+
+Example: % This program is not typable with the Type Inference algorithm from Plümicke
+\begin{lstlisting}[style=java,label=shuffleExample,caption=Intermediate Types Example]
+class List<X> extends Object {...}
+class List2D<X> extends List<List<X>> {...}
+
+<X> void shuffle(List<List<X>> list) {...}
+
+List<List<?>> l = ...;
+List2D<?> l2d = ...;
+
+shuffle(l); // Error
+shuffle(l2d); // Valid
+\end{lstlisting}
+Java is using local type inference to allow method invocations which are not describable with regular Java types.
+The \texttt{shuffle} method in this case is invoked with the type $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$
+which is a subtype of $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
+After capture conversion \texttt{l2d'} has the type $\exptype{List}{\exptype{List}{\rwildcard{X}}}$
+and \texttt{shuffle} can be invoked with the type parameter $\rwildcard{X}$:
+\begin{lstlisting}[style=letfj]
+let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in <X>shuffle(l2d')
+\end{lstlisting}
+
+\subsection{Global Type Inference}
+
+\begin{description}
+    \item[input] \tifj{} program
+    \item[output] type solution
+    \item[postcondition] the type solution applied to the input must yield a valid \letfj{} program
+\end{description}
+
+The input to our type inference algorithm is a modified version of the \letfj{}\cite{WildcardsNeedWitnessProtection} calculus (see chapter \ref{sec:tifj}).
+First \fjtype{} generates constraints
+and afterwards \unify{} computes a solution for the given constraint set.
+Constraints consist out of subtype constraints $(\type{T} \lessdot \type{T})$ and capture constraints $(\type{T} \lessdotCC \type{T})$.
+\textit{Note:} a type $\type{T}$ can either be a named type, a type placeholder or a wildcard type placeholder.
+A subtype constraint is satisfied if the left side is a subtype of the right side according to the rules in figure \ref{fig:subtyping}.
+\textit{Example:} $\exptype{List}{\ntv{a}} \lessdot \exptype{List}{\type{String}}$ is fulfilled by replacing type placeholder $\ntv{a}$ with the type $\type{String}$.
+Subtype constraints and type placeholders act the same as the ones used in \emph{Type Inference for Featherweight Generic Java} \cite{TIforFGJ}.
+The novel capture constraints and wildcard placeholders are needed for method invocations involving wildcards.
+
+\begin{recap}\textbf{TI for FGJ without Wildcards:}
+\TFGJ{} generates subtype constraints $(\type{T} \lessdot \type{T})$ consisting of named types and type placeholders.
+For example the method invocation \texttt{concat(l, new Object())} generates the constraints
+$\tv{l} \lessdot \exptype{List}{\tv{a}}, \type{Object} \lessdot \tv{a}$.
+Subtyping without the use of wildcards is invariant \cite{FJ}:
+Therefore the only possible solution for the type placeholder $\tv{a}$ is $\tv{a} \doteq \type{Object}$. % in Java and Featherweight Java.
+The correct type for the variable \texttt{l} is $\exptype{List}{\type{Object}}$ (or a direct subtype).
+%- usually the type of e must be subtypes of the method parameters
+%- in case of a polymorphic method: type placeholders resemble type parameters
+The type inference algorithm for Featherweight Generic Java \cite{TIforFGJ} (called \TFGJ{}) is complete and sound:
+It is able to find a type solution for a Featherweight Generic Java program, which has no type annotations at all,
+if there is any.
+It's only restriction is that no polymorphic recursion is allowed.
+\end{recap}
+%
+Lets have a look at the constraints generated by \fjtype{} for the example in listing \ref{lst:addExample}:
+\begin{constraintset}
+\begin{center}
+$\begin{array}{c}
+\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}, \, \type{String} \lessdotCC \wtv{a}
+\\
+\hline
+\textit{Capture Conversion:}\ \wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
+\\
+\hline
+\textit{Solution:}\ \wtv{a} \doteq \rwildcard{Y} \implies \wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}, \, \type{String} \lessdot \rwildcard{Y}
+\end{array}
+$
+\end{center}
+\end{constraintset}
+%
+Capture Constraints $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ allow for a capture conversion,
+which converts a constraint of the form $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ to $(\exptype{C}{\rwildcard{X}} \lessdot \type{T})$
+%These constraints are used at places where a capture conversion via let statement can be added.
+
+%Why do we need the lessdotCC constraints here?
+The type of \texttt{l} can be capture converted by a let statement if needed (see listing \ref{lst:addExampleLet}).
+Therefore we assign the constraint $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$
+which allows \unify{} to do a capture conversion to $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
+The captured wildcard $\rwildcard{X}$ gets a fresh name and is stored in the wildcard environment of the \unify{} algorithm.
+
+
+\textit{Note:} The constraint $\type{String} \lessdot \rwildcard{Y}$ is satisfied
+because $\rwildcard{Y}$ has $\type{String}$ as lower bound.
+
+
+For the example shown in listing \ref{shuffleExample} the method call \texttt{shuffle(l2d)} creates the constraints:
+\begin{constraintset}
+\begin{center}
+    $
+    \begin{array}{l}
+    \wctype{\rwildcard{X}}{List2D}{\rwildcard{X}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
+    \\
+    \hline
+    \wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
+    \\
+    \hline
+    \textit{Capture Conversion:}\ 
+    \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\wtv{x}}}
+    \\
+    \hline
+    \textit{Solution:} \wtv{x} \doteq \rwildcard{X} \implies \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\rwildcard{X}}}
+    \end{array}
+    $
+\end{center}
+\end{constraintset}
+
+The method call \texttt{shuffle(l)} is invalid however,
+because \texttt{l} has the type
+$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
+There is no solution for the subtype constraint:
+$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$
+
+% No capture conversion for methods in the same class:
+% Given two methods without type annotations like
 % \begin{verbatim}
-% <X> concat(List<X> l1, List<X> l2){...}
+% // m :: () -> r
+% m() = new List<String>() :? new List<Integer>();
+
+% // id :: (a) -> a
+% id(a) = a
 % \end{verbatim}
-% \begin{minipage}{0.50\textwidth}
-% Java:
+
+% and a method call \texttt{id(m())} would lead to the constraints:
+% $\exptype{List}{\type{String}} \lessdot \ntv{r},
+% \exptype{List}{\type{Integer}} \lessdot \ntv{r},
+% \ntv{r} \lessdotCC \ntv{a}$
+
+% In this example capture conversion is not applicable,
+% because the \texttt{id} method is not polymorphic.
+% The type solution provided by \unify{} for this constraint set is:
+% $\sigma(\ntv{r}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, 
+% \sigma(\ntv{a}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$
 % \begin{verbatim}
-% final List<?> l = ...;
-% concat(l, l);
+% List<?> m() = new List<String>() :? new List<Integer>();
+% List<?> id(List<?> a) = a
 % \end{verbatim}
-% \end{minipage}%
-% \begin{minipage}{0.50\textwidth}
-% Featherweight Java:
+
+% The following example has the \texttt{id} method already typed and the method \texttt{m}
+% extended by a recursive call \texttt{id(m())}:
 % \begin{verbatim}
-% let l : X.List<X> = ... in
-%     concat(l, l)
+% <A> List<A> id(List<A> a) = a
+
+% m() = new List<String>() :? new List<Integer>() :? id(m());
 % \end{verbatim}
-% \end{minipage}
+% Now the constraints make use of a $\lessdotCC$ constraint:
+% $\exptype{List}{\type{String}} \lessdot \ntv{r},
+% \exptype{List}{\type{Integer}} \lessdot \ntv{r},
+% \ntv{r} \lessdotCC \exptype{List}{\wtv{a}}$
+
+% After substituting $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\ntv{r}$ like in the example before
+% we get the constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$.
+% Due to the $\lessdotCC$ \unify{} is allowed to perform a capture conversion yielding
+% $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
+% \textit{Note:} The wildcard placeholder $\wtv{a}$ is allowed to hold free variables whereas a normal placeholder like $\ntv{r}$
+% is never assigned a type containing free variables.
+% Therefore \unify{} sets $\wtv{a} \doteq \rwildcard{X}$, completing the constraint set and resulting in the type solution:
+% \begin{verbatim}
+% List<?> m() = new List<String>() :? new List<Integer>() :? id(m());
+% \end{verbatim}
+
+\subsection{\TamedFJ{} and \letfj{}}
+%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.
+Methods are declared without parameter or return types.
+We still keep 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 no 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:inputSyntax}.
 
 
+\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}) \{ \texttt{return}\ 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:inputSyntax}
+\end{figure}
+
+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.
+Our output syntax is shown in figure \ref{fig:outputSyntax}
+which is actually a subset of \letfj{}, because we omit \texttt{null} types.
+
+\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} & ::= & \generics{\overline{\type{X} \triangleleft \type{N}}}\type{T}\ \texttt{m}(\overline{\type{T}\ \expr{x}}) = \expr{e} \\
+\text{Terms} & \expr{e} & ::= & \expr{x} \\
+& & \ \ | & \texttt{new} \ \exptype{C}{\ol{T}}(\overline{\expr{e}})\\
+& & \ \ | & \expr{e}.f\\
+& & \ \ | & \expr{e}.\texttt{m}\generics{\ol{T}}(\overline{\expr{e}})\\
+& & \ \ | & \texttt{let}\ \expr{x} : \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{Output Syntax}\label{fig:outputSyntax}
+\end{figure}
+
+
+The output of our type inference algorithm is a valid \letfj{} program.
+Before generating constraints the input is transformed to \TamedFJ{}.
+After adding the missing type annotations the resulting program is a valid \letfj{} program.
+%This is shown in chapter \ref{sec:soundness}
+Capture conversion is only needed for wildcard types,
+but we don't know which expressions will spawn wildcard types because there are no type annotations yet.
+We preemptively enclose every expression in a let statement before using it as a method argument.
+
+We need the let statements to deal with possible Wildcard types.
+
+
+The syntax used in our examples is the standard Featherweight Java syntax.
 
 
 \subsection{Challenges}\label{challenges}
 %TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
 
 
-One problem is the divergence between denotable and expressable types in Java \cite{semanticWildcardModel}.
-A wildcard in the Java syntax has no name and is bound to its enclosing type.
-\texttt{List<List<?>>} equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
-During type checking intermediate types like $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$
-or $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ can emerge, which have no equivalent in the Java syntax.
-Our type inference algorithm uses existential types internally but spawns type solutions compatible with Java.
-
-
 The introduction of wildcards adds additional challenges.
 % we cannot replace every type variable with a wildcard
 Type variables can also be used as type parameters, for example
@@ -330,19 +496,11 @@ Knowing that the type \texttt{String} is a subtype of any type the wildcard \tex
 it is safe to pass \texttt{"String"} for the first parameter of the function.
 
 \begin{verbatim}
-<A> List<A> add(A a, List<A> la) {}
+<A> List<A> add(List<A> l, A v) {}
 
-    List<? super String> list = ...;
-    add("String", list);
+List<? super String> list = ...;
+add(list, "String");
 \end{verbatim}
-The constraints representing this code snippet are:
-
-\begin{displaymath}
-    \type{String} \lessdotCC \wtv{a},\,
-\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}
-\end{displaymath}
-
-Here $\sigma(\tv{a}) = \rwildcard{X}$ is a valid solution.
 \end{example}
 
 \item \begin{example}\label{intro-example2}
@@ -350,117 +508,229 @@ This example displays an incorrect Java program.
 The method call to \texttt{concat} with two wildcard lists is unsound.
 Each list could be of a different kind and therefore the \texttt{concat} cannot succeed.
 \begin{verbatim}
-<A> List<A> concat(List<A> l1, List<A> l2) {}
+<A> List<A> concat(List<A> l1, List<A> l2) { ... }
 
-    List<?> list = ... ;
-    concat(list, list);
+List<?> list = ... ;
+concat(list, list);
 \end{verbatim}
-The constraints for this example are:
 
-$\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}, \\
-\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
-%$\exptype{List}{?} \lessdot \exptype{List}{\tv{a}},
-%\exptype{List}{?} \lessdot \exptype{List}{\tv{a}}$
 
-Remember that the given constraints cannot have a valid solution.
-%This is due to the fact that the wildcard variables cannot leave their scope.
-In this example the \unify{} algorithm should not replace $\tv{a}$ with the captured wildcard $\rwildcard{X}$.
+% $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}, \\
+% \wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
 \end{example}
 
-\item 
-\unify{} can only remove wildcards, but never add wildcards to an existing type.
-Java subtyping is invariant.
-The type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ cannot be a subtype of $\exptype{List}{\tv{a}}$
+% \item 
+% \unify{} morphs a constraint set into a correct type solution
+% gradually assigning types to type placeholders during that process.
+% Solved constraints are removed and never considered again.
+% In the following example \unify{} solves the constraint generated by the expression
+% \texttt{l.add(l.head())} first, which results in $\ntv{l} \lessdot \exptype{List}{\wtv{a}}$.
+% \begin{verbatim}
+% anyList() = new List<String>() :? new List<Integer>()
 
-\unify{} morphs a constraint set into a correct type solution
-gradually assigning types to type placeholders during that process.
-Solved constraints are removed and never considered again.
-In the following example \unify{} solves the constraint generated by the expression
-\texttt{l.add(l.head())} first, which results in $\ntv{l} \lessdot \exptype{List}{\wtv{a}}$.
-\begin{verbatim}
-List<?> l = ...;
+% add(anyList(), anyList().head());
+% \end{verbatim}
+% The type for \texttt{l} can be any kind of list, but it has to be a invariant one.
+% Assigning a \texttt{List<?>} for \texttt{l} is unsound, because the type list hiding behind
+% \texttt{List<?>} could be a different one for the \texttt{add} call than the \texttt{head} method call.
+% An additional constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
+% is solved by removing the wildcard $\rwildcard{X}$ if possible.
 
-m2() {
-  l.add(l.head());
+\item \textbf{No principal method type:}
+We tried to skip capture conversion and the capture constraints entirely.
+But \letfj{}'s type system does not imply a principal typing for methods \cite{principalTypes}.
+The problem is that a principal type of a method should have the most general parameter types and the most specific return type.
+\begin{lstlisting}[caption=Return type depends on argument types,label=principalTypeExample]
+class SpecialPair<X, Y extends X> extends Pair<X,Y>{}
+
+
+<X,Y> Pair<X,Y> id(Pair<X,Y> in){
+  return in;
 }
-\end{verbatim}
-The type for \texttt{l} can be any kind of list, but it has to be a invariant one.
-Assigning a \texttt{List<?>} for \texttt{l} is unsound, because the type list hiding behind
-\texttt{List<?>} could be a different one for the \texttt{add} call than the \texttt{head} method call.
-An additional constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
-is solved by removing the wildcard $\rwildcard{X}$ if possible.
+
+<X, Y extends X> void receive(Pair<X,Y> in){}
+
+Pair<?, ?> l;
+SpecialPair<?,?> lSpecial;
+
+id(l); // this has to work
+receive(id(lSpecial)); // and this too
+\end{lstlisting}
+
+By means of subtyping we are able to create types like
+$\wctype{\rwildcard{X}, \wildcard{Y}{\rwildcard{X}}{\bot}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$
+as a direct supertype of \texttt{SpecialPair<?,?>},
+which is now compatible with the \texttt{receive} method.
+The call \texttt{receive(id(lSpecial))} is correct whereas the return type of the \texttt{id} method
+does not imply so.
+
+If we look at this in the context of global type inference and assume that there are no type annotations for \texttt{l} and \texttt{lSpecial}.
+We can neither apply capture conversion during the constraint generation step, because the parameter types are not known yet
+and we also can't assume a most generic type for the parameter types, because the the needed return type is not known either.
+Take the example in figure \ref{fig:principalTI}.
+As soon as the type of $\tv{lSpecial}$ is resolved \unify{} can determine the type of $\tv{id}$
+and then solve the constraints $\tv{id} \lessdotCC \exptype{Pair}{\wtv{e}, \wtv{f}}, \wtv{f} \lessdot \wtv{e}$.
+%TODO: explain how type variables are named after their respective variables and methods
+Capture Conversion cannot be applied before the argument type ($\tv{lSpecial}$ in this case) is known.
+Trying to give $\tv{lSpecial}$ a most general type like \texttt{Pair<?,?>} won't work either (see listing \ref{principalTypeExample}).
+
+\begin{figure}
+\begin{minipage}{0.40\textwidth}
+\begin{lstlisting}[style=tfgj]
+// l and lSpecial are untyped 
+id(l);
+receive(id(lSpecial));
+\end{lstlisting}
+\end{minipage}%
+\hfill
+\begin{minipage}{0.59\textwidth}
+\begin{constraintset}
+$
+\tv{l} \lessdotCC \exptype{Pair}{\wtv{a}, \wtv{b}}, \\
+\tv{lSpecial} \lessdotCC \exptype{Pair}{\wtv{c}, \wtv{d}}, 
+\exptype{Pair}{\wtv{c}, \wtv{d}} \lessdot \tv{id}, \\
+\tv{id} \lessdotCC \exptype{Pair}{\wtv{e}, \wtv{f}},
+\wtv{f} \lessdot \wtv{e}
+$
+\end{constraintset}
+\end{minipage}
+\caption{Principal Type problem}\label{fig:principalTI}
+\end{figure}
+% TODO: make Unify to resolve C<X> <. a as a =. X.C<X>
+
+% A method has infinte possibilities of being called and there is no most general type.
+% P<X,Y> m(C<X> c, C<Y> c2)
+% depending on 
+% A.P<A,A> <. A,B.P<A,B>
+
+% % During the method call it is not sure what kind of return type is needed from the method.
+% % The method P<A,B> make(A a, B b) 
+% % The type A,B.P<A,B> cannot be a subtype of P<X,X>
+% % But if A^X_X and B^X_X
+% % Could a constraint C<X> <. a? be expanded to a? = X^u?_l?.C<X>
 
 
 \end{itemize}
 
+%TODO: Move this part. or move the third challenge some underneath.
 The \unify{} algorithm only sees the constraints with no information about the program they originated from.
-The main challenge was to find an algorithm which computes $\sigma(\tv{a}) = \rwildcard{X}$ for example \ref{intro-example1} but not for example \ref{intro-example2}.
-% Solution: A type variable can only take one type and not a wildcard type.
-    % A wildcard type is only treated like a wildcard while his definition is in scope (during the reduce rule)
+The main challenge was to find an algorithm which computes $\sigma(\wtv{a}) = \rwildcard{X}$ for example \ref{intro-example1} but not for example \ref{intro-example2}.
 
+%TODO
+% The goal is to proof soundness in respect to the type rules introduced by \cite{aModelForJavaWithWildcards}
+% and \cite{WildcardsNeedWitnessProtection}.
 
 % \subsection{Capture Conversion}
+% The \texttt{let} statements in \TamedFJ{} act as capture conversion for wildcard types.
+
+% \begin{figure} 
+% \begin{minipage}{0.45\textwidth}
+% \begin{lstlisting}[style=tfgj]
+% <X> List<X> clone(List<X> l);
+% example(p){
+%   return clone(p);
+% }
+% \end{lstlisting}
+%     \end{minipage}%
+%     \hfill
+%     \begin{minipage}{0.5\textwidth}
+% \begin{lstlisting}[style=letfj]
+% <X> List<X> clone(List<X> l);
+% (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p) = 
+%   let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in
+%    clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
+% \end{lstlisting}
+%     \end{minipage}
+% \caption{Type inference adding capture conversion}\label{fig:addingLetExample}
+%   \end{figure}
+
+% Figure \ref{fig:addingLetExample} shows a let statement getting added to the typed output.
+% The method \texttt{clone} cannot be called with the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
+% After a capture conversion \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$ with $\rwildcard{X}$ being a free variable.
+% Afterwards we have to find a supertype of $\exptype{List}{\rwildcard{X}}$, which does not contain free variables
+% ($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in this case).
+
+% During the constraint generation step most types are not known yet and are represented by a type placeholder.
+% During a methodcall like the one in the \texttt{example} method in figure \ref{fig:ccExample} the type of the parameter \texttt{p}
+% is not known yet.
+% The type \texttt{List<?>} would be one possibility as a parameter type for \texttt{p}.
+% To make wildcards work for our type inference algorithm \unify{} has to apply capture conversions if necessary.
+
+% The type placeholder $\tv{r}$ is the return type of the \texttt{example} method.
+% One possible type solution is $\tv{p} \doteq \tv{r} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$,
+% which leads to:
 % \begin{verbatim}
-% <A> List<A> add(A a, List<A> la) {}
-
-% List<? super String> list = ...;
-
-% add("String", list);
+% List<?> example(List<?> p){
+%   return clone(p);
+% }
 % \end{verbatim}
-% The constraints representig this code snippet are:
-% $\type{String} \lessdot \tv{a},
-% \wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\tv{a}}$
-% Under the hood the typechecker has to find a replacement for the generic method parameter \texttt{A}.
 
-% Java allows a method \texttt{<A> List<A> add(A a, List<A> la)} to be called with
-% \texttt{String} and \texttt{List<? super String>}.
-% A naive approach would be to treat wildcards like any other type and replace \texttt{A}
-% with \texttt{? super String}.
-% Generating the method type \texttt{List<? super String> add(? super String a, List<? super String> la)}.
+% But by substituting $\tv{p} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in the constraint
+% $\tv{p} \lessdotCC \exptype{List}{\wtv{x}}$ leads to
+% $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$.
 
-% This does not work for a method like
-% \texttt{<A> void merge(List<A> l1, List<A> l2)}.
-% It is crucial for this method to be called with two lists of the same type.
-% Substituting a wildcard for the generic \texttt{A} leads to
-% \texttt{void merge(List<?> l1, List<?> l2)},
-% which is unsound.
+% To make this typing possible we have to introduce a capture conversion via a let statement:
+% $\texttt{return}\ (\texttt{let}\ \texttt{x} : \wctype{\rwildcard{X}}{List}{\rwildcard{X}} = \texttt{p}\ \texttt{in} \
+% \texttt{clone}\generics{\rwildcard{X}}(x) : \wctype{\rwildcard{X}}{List}{\rwildcard{X}})$
 
-% Capture conversion utilizes the fact that instantiated classes always have an actual type.
-% \texttt{new List<String>()} and \texttt{new List<Object>()} are
-% valid instances.
-% \texttt{new List<? super String>()} is not.
-% Every type $\wcNtype{\Delta}{N}$ contains an underlying instance of a type $\type{N}$.
-% Knowing this fact allows to make additional assumptions.
+% Inside the let statement the variable \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$
 
-% \wildFJ{} type rules allow for generic parameters to be replaced by wildcard types.
-% This is possible because wildcards are split into two parts.
-% Their declaration at the environment part $\Delta$ of a type $\wcNtype{\Delta}{N}$
-% and their actual use in the body of the type $\type{N}$.
-% Replacing the generic \texttt{A} in the type \texttt{List<A>}
-% by a wildcard $\type{X}$ will not generate the type \texttt{List<?>}.
-% \texttt{List<?>} is the equivalent of $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\type{X}}$.
-% The generated type here is $\exptype{List}{\type{X}}$, which has different subtype properties.
-% There is no information about what the type $\exptype{List}{\type{X}}$ actually is.
-% It has itself as a subtype and for example a type like $\exptype{ArrayList}{\type{X}}$.
 
-% A method call for example only works with values, which are correct instances of classes.
-% Capture conversion automatically converts wildcard type to a concrete class type,
-% which then can be used as a parameter for a method call.
+% This spawns additional problems.
 
-% In \wildFJ{} this is done via let statements.
+% \begin{figure} 
+% \begin{minipage}{0.45\textwidth}
+% \begin{verbatim}
+% <X> List<X> clone(List<X> l){...}
 
-% Written in FJ syntax: $\type{N}$ is a initialized type and
-% $\wcNtype{\Delta}{N}$ is a type containing wildcards $\Delta$.
+% example(p){
+%   return clone(p);
+% }
+% \end{verbatim}
+%   \end{minipage}%
+%   \hfill
+%   \begin{minipage}{0.35\textwidth}
+% \begin{constraintset}
+%     \textbf{Constraints:}\\
+%     $
+%   \tv{p} \lessdotCC \exptype{List}{\wtv{x}}, \\
+% \tv{p} \lessdot \tv{r}, \\
+% \tv{p} \lessdot \type{Object}, 
+% \tv{r} \lessdot \type{Object}
+%     $
+% \end{constraintset}
+%   \end{minipage}
 
-% It is crucial for the wildcard names to never be used twice.
-% Otherwise the members of a list with type $\wctype{\type{X}}{List}{\type{X}}$ and
-% a list with type $\wctype{\type{X}}{List}{\type{X}}$ would be the same. $\type{X}$ in fact.
+% \caption{Type inference example}\label{fig:ccExample}
+% \end{figure}
 
-% The let statement adds wildcards to the environment.
-% Those wildcards are not allowed to escape the scope of the let statement.
-% Which is a problem for our type inference algorithm.
-
-% The capture converted version of the type $\wctype{\rwildcard{X}}{Box}{\rwildcard{X}}$ is
-% $\exptype{Box}{\rwildcard{X}}$.
-% The captured type is only used as an intermediate type during a method call.
+% In addition with free variables this leads to unwanted behaviour.
+% Take the constraint
+% $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ for example.
+% After a capture conversion from $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ to $\exptype{List}{\rwildcard{Y}}$ and a substitution $\wtv{a} \doteq \rwildcard{Y}$
+% we get
+% $\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$.
+% Which is correct if we apply capture conversion to the left side:
+% $\exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$
+% If the input constraints did not intend for this constraint to undergo a capture conversion then \unify{} would produce an invalid
+% type solution due to:
+% $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \nless: \exptype{List}{\rwildcard{X}}$
+% The reason for this is the \texttt{S-Exists} rule's premise
+% $\text{dom}(\Delta') \cap \text{fv}(\exptype{List}{\rwildcard{X}}) = \emptyset$.
 
+% Capture constraints cannot be stored in a set.
+% $\wtv{a} \lessdotCC \wtv{b}$ is not the same as $\wtv{a} \lessdotCC \wtv{b}$.
+% Both constraints will end up the same after a substitution for both placeholders $\tv{a}$ and $\tv{b}$.
+% But afterwards a capture conversion is applied, which can generate different types on the left sides.
+% \begin{itemize}
+%   \item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Y}}$ 
+%   \item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Z}}$ 
+% \end{itemize}
+% 
+% Wildcards are not reflexive. A box of type $\wctype{\rwildcard{X}}{Box}{\rwildcard{X}}$
+% is able to hold a value of any type. It could be a $\exptype{Box}{String}$ or a $\exptype{Box}{Integer}$ etc.
+% Also two of those boxes do not necessarily contain the same type.
+% But there are situations where it is possible to assume that.
+% For example the type $\wctype{\rwildcard{X}}{Pair}{\exptype{Box}{\rwildcard{X}}, \exptype{Box}{\rwildcard{X}}}$
+% is a pair of two boxes, which always contain the same type.
+% Inside the scope of the \texttt{Pair} type, the wildcard $\rwildcard{X}$ stays the same.

letfjTransformation.tex

@@ -0,0 +1,121 @@
+
+%We could do a translation from Java to \wildFJ explaining implicit capture conversion
+
+\section{Soundness of Typing}
+
+
+We show soundness with the type rules statet in \cite{WildcardsNeedWitnessProtection}.
+A correct \FGJGT{} program can be converted to a correct \wildFJ{} program.
+
+\begin{figure}
+$\begin{array}{rcl}
+    | \texttt{x} |
+    & = & \texttt{x} \\
+    | \texttt{let} \ \texttt{x} : \type{T} = \texttt{e},\, \ol{x} : \ol{T} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x}) |
+    & = & |\texttt{e}|.\texttt{m}(\ol{|e|}) \\
+    | \texttt{let} \ \texttt{x} : \type{T} = \texttt{e}\ \texttt{in}\ \texttt{x}.\texttt{f} |
+    & = & |\texttt{e}|.\texttt{f} \\
+    | \texttt{e} \elvis{} \texttt{e} |
+    & = & |\texttt{e}| \elvis{} |\texttt{e}| \\
+\end{array}$
+\caption{Erasure} \label{fig:erasure}
+\end{figure}
+
+% A constraint Pair<A,B> <. a, then a has infinite possibilities:
+% a =. X.Pair<X,X>
+% a =. X,Y.Pair<X,Y>
+% a =. X.Pair<Pair<X,X>,X>
+% a =. X,Y.Pair<Pair<X,Y>,X>
+% a =. X,Y.Pair<Pair<X,Y>,Y>
+
+% There is no way to try out every single one of them.
+
+Starting with the parameters of the method we gradually add every expression which only contains already captured expressions.
+
+We have a typed expression
+
+$|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} : \type{T} = \texttt{x in}$
+$|\texttt{e.f}, \texttt{r}| = |\texttt{e}, x| \texttt{let} r = x.\texttt{f} \ \texttt{in}$ 
+$|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} = \texttt{x in}$
+%TODO: write the transform rules:
+% |e.f, ret| = |e, r| let ret = r.f in
+% |x, ret| = let ret = x in
+% |e.m(e_), ret| = |e, r| |e_, a_| let ret = r.m(a_) in
+
+Erasure functions:
+$|\texttt{x}| = \texttt{let r} : \wcNtype{\Delta}{N} = \texttt{x in r}$
+
+$\texttt{x} \longmapsto \texttt{let}\ \texttt{xx} : \type{T} = \texttt{x in xx}$
+$\texttt{x}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in xf}$
+
+$\begin{array}{l}
+\texttt{e} \longmapsto \texttt{let}\ \texttt{xe} : \type{T} = \texttt{e}' \ \texttt{in xe} \\ 
+\hline
+\vspace*{-0.4cm}\\
+\texttt{e}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in x}.f
+\end{array}$
+
+Example:
+m(a, b) = a.m(b.f);
+
+let xa = a in let xb = b in let xf = xb.f in let xm = xa.m(xf) in xm
+
+% TODO: Now we have to proof that there is a LetFJ program for every TIFJ program!
+% |let xr : T = x1.m(x2) in e| = [x1.m(x2)/xr]|e| 
+% |let xf : T = x1.f in e| = [x1.f/xf]|e|
+% |let xr : T = x in e| = [xr/x]|e|
+% |new C(x)| = new C(x)
+
+% | let xr : T' = x in let xf : T = xr.f | = x.f
+
+
+% let x : T' = e' in x = |e|
+% ---------------------------------
+% | let xr : T' = x in let xf : T = xr.f | = x.f
+
+
+
+% let x : T' = e' in x = |e|
+% -----------
+% = 
+
+We need a language which only has let statemnts and expressions on capture converted variables
+
+The idea is to use wildcard placeholders inside the method. Also in the bounds of wildcards.
+This makes it possible to replace wildcards with free variables by setting upper and lower bound to that free variable.
+Free variables then can flow freely inside the method body.
+We have to show that a type solution implies that there is a possible transformation to a correct typed letFJ program.
+If there is a possible method type then there must exist a let configuration.
+% By starting with the parameter types and capturing them. Afterwards every capture creates free variables which are used inside
+% TODO: Proof!
+
+The normal type placeholders represent denotable types.
+
+%TODO: the type rules stay the same. We generate let statements in a fashion which removes all wildcard types.
+% what about wildcards getting returned by untyped methods? they can also be captured
+% TODO: try soundness proof on the original type rules!
+
+Removing of extensive wildcards:
+$
+\wctype{\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{X}, \rwildcard{Y}}
+\lessdot \wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}} \\
+\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \wtv{x}, \rwildcard{Y} \doteq \wtv{x} \\
+\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \rwildcard{Y} \\
+\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
+\implies \wctype{\wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{Y}, \rwildcard{Y}}, \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
+$
+
+%e.f leads to constraints: r <c C<x> with return type equals the field type T.
+%   T can contain free variables from r. but also it can be used in another constraint and get free variables from inner let statements
+%   X.C<X> <c C<x> -> then T contains X variables
+
+% let x1 = p1, x2 = p2 in
+%  let r1  = x1 in let r2 = p2 in let f1 = r2.f in let r3 = x1 in let m2 = r3.m2() let ret = r1.m(f1,m2)
+%   in ret
+
+What about method invocation with no type yet. m2 :: a -> a 
+they are also encased in let expression so the return type can be capture converted.
+Those methods and the parameter types of the current method are the only things not typed.
+All the other types cannot change their type. The captured wildcards can only flow from top to bottom.
+The return type of untyped methods has to be well-formed and cannot contain free variables.
+Therefore no free variables will flow into those types.

martin.bib

@@ -388,4 +388,81 @@ numpages = {14},
 keywords = {existential types, joins, parametric types, single-instantiation inheritance, subtyping, type inference, wildcards}
 }
 
+@inproceedings{10.1145/1449764.1449804,
+author = {Smith, Daniel and Cartwright, Robert},
+title = {Java type inference is broken: can we fix it?},
+year = {2008},
+isbn = {9781605582153},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+url = {https://doi.org/10.1145/1449764.1449804},
+doi = {10.1145/1449764.1449804},
+abstract = {Java 5, the most recent major update to the Java Programming Language, introduced a number of sophisticated features, including a major extension to the type system. While the technical details of these new features are complex, much of this complexity is hidden from the typical Java developer by an ambitious type inference mechanism. Unfortunately, the extensions to the Java 5 type system were so novel that their technical details had not yet been thoroughly investigated in the research literature. As a result, the Java 5 compiler includes a pragmatic but flawed type inference algorithm that is, by design, neither sound nor locally complete. The language specification points out that neither of these failures is catastrophic: the correctness of potentially-unsound results must be verified during type checking; and incompleteness can usually be worked around by manually providing the method type parameter bindings for a given call site.This paper dissects the type inference algorithm of Java 5 and proposes a signficant revision that is sound and able to calculate correct results where the Java 5 algorithm fails. The new algorithm is locally complete with the exception of a difficult corner case. Moreover, the new algorithm demonstrates that several arbitrary restrictions in the Java type system---most notably the ban on lower-bounded type parameter declarations and the limited expressibility of intersection types---are unnecessary. We hope that this work will spur the evolution of a more coherent, more comprehensive generic type system for Java.},
+booktitle = {Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications},
+pages = {505–524},
+numpages = {20},
+keywords = {bounded quantification, generics, intersection types, parameterized types, polymorphic methods, subtyping, type argument inference, type inference, union types, wildcards},
+location = {Nashville, TN, USA},
+series = {OOPSLA '08}
+}
+
+  
+
+@article{JavaLocalTI,
+author = {Smith, Daniel and Cartwright, Robert},
+title = {Java type inference is broken: can we fix it?},
+year = {2008},
+issue_date = {September 2008},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {43},
+number = {10},
+issn = {0362-1340},
+url = {https://doi.org/10.1145/1449955.1449804},
+doi = {10.1145/1449955.1449804},
+abstract = {Java 5, the most recent major update to the Java Programming Language, introduced a number of sophisticated features, including a major extension to the type system. While the technical details of these new features are complex, much of this complexity is hidden from the typical Java developer by an ambitious type inference mechanism. Unfortunately, the extensions to the Java 5 type system were so novel that their technical details had not yet been thoroughly investigated in the research literature. As a result, the Java 5 compiler includes a pragmatic but flawed type inference algorithm that is, by design, neither sound nor locally complete. The language specification points out that neither of these failures is catastrophic: the correctness of potentially-unsound results must be verified during type checking; and incompleteness can usually be worked around by manually providing the method type parameter bindings for a given call site.This paper dissects the type inference algorithm of Java 5 and proposes a signficant revision that is sound and able to calculate correct results where the Java 5 algorithm fails. The new algorithm is locally complete with the exception of a difficult corner case. Moreover, the new algorithm demonstrates that several arbitrary restrictions in the Java type system---most notably the ban on lower-bounded type parameter declarations and the limited expressibility of intersection types---are unnecessary. We hope that this work will spur the evolution of a more coherent, more comprehensive generic type system for Java.},
+journal = {SIGPLAN Not.},
+month = {oct},
+pages = {505–524},
+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}
+}
 

prolog.tex

@@ -4,17 +4,24 @@
 \lstset{language=Java,
   showspaces=false,
   showtabs=false,
-  breaklines=true,
+  %breaklines=true,
   showstringspaces=false,
-  breakatwhitespace=true,
+  %breakatwhitespace=true,
   basicstyle=\ttfamily\fontsize{8}{9.6}\selectfont, %\footnotesize
   escapeinside={(*@}{@*)},
-  captionpos=b,
+  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}}
 
+\newtheorem{recap}[note]{Recap}
 
+\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{>} }}
@@ -98,8 +105,11 @@
 \newcommand{\localVarAssumption}{\ensuremath{\mathtt{\eta}}}
 \newcommand{\expandLB}{\textit{expandLB}}
 
+\newcommand{\letfj}{\emph{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 , }
@@ -111,7 +121,8 @@
 \newcommand{\wtypestore}[3]{\ensuremath{#1 = \wtype{#2}{#3}}}
 %\newcommand{\wtype}[2]{\ensuremath{[#1\ #2]}}
 \newcommand{\wtv}[1]{\ensuremath{\tv{#1}_?}}
-\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
+%\newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
+\newcommand{\ntv}[1]{\tv{#1}}
 \newcommand{\wcstore}{\ensuremath{\Delta}}
 
 %\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}_?}}
@@ -133,7 +144,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}}
 

soundness.tex

@@ -329,18 +329,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 +377,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$).
@@ -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,4 +1,4 @@
-\section{Syntax and Typing}
+\section{Syntax and Typing}\label{sec:tifj}
 
 The input syntax for our algorithm is shown in figure \ref{fig:syntax}
 and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}.
@@ -8,6 +8,18 @@ The input language is designed to showcase type inference involving existential
 Method call rule T-Call is the most interesting part, because it emulates the behaviour of a Java method call,
 where existential types are implicitly \textit{opened} and \textit{closed}.
 
+Example: %TODO
+\begin{verbatim}
+class List<A> {
+    A head;
+    List<A> tail;
+
+    add(v) = new List(v, this);
+}
+\end{verbatim}
+
+%The 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.
@@ -26,6 +38,10 @@ 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.
+Even variables have to be catched by a let statement first.
+This behaviour emulates Java's implicit capture conversion.
+
 \begin{figure}
 $
 \begin{array}{lrcl}
@@ -35,19 +51,183 @@ $
 \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} & ::= & \generics{\ol{X \triangleleft T}} \type{T} \ \texttt{m}(\overline{\type{T}\ x}) = t \\
-\text{Terms} & t & ::= & x \\
-& & \ \ | & \texttt{new} \ \exptype{C}{\ol{T}}(\overline{t})\\
-& & \ \ | & t.f\\
-& & \ \ | & t.\generics{\ol{T}}\texttt{m}(\overline{t})\\
-& & \ \ | & t \elvis{} t\\
-\text{Variable contexts} & \Gamma & ::= & \overline{x:\type{T}}\\
+\text{Method declarations} &  \texttt{M} & ::= & \texttt{m}(\overline{\expr{x}}) = t \\
+\text{Terms} & t & ::= & \expr{x} \\
+& & \ \ | &  \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}_c}) \\
+& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \expr{x}_c.f \\
+& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \expr{x}_c.\texttt{m}(\overline{\expr{x}_c}) \\
+& & \ \ | & t \elvis{} t \\
+\text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
 \hline
 \end{array}
 $
-\caption{Input Syntax}\label{fig:syntax}
+\caption{\TamedFJ{} Syntax}\label{fig:syntax}
 \end{figure}
 
+% \begin{figure}
+% $
+% \begin{array}{lrcl}
+% \hline
+% \text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
+% \text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
+% \text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
+% \text{Type variable contexts} &  \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
+% \text{Class declarations} &  D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\
+% \text{Method declarations} &  \texttt{M} & ::= & \texttt{m}(\overline{\expr{x}}) = t \\
+% \text{Values} & v & ::= & \expr{x} \\
+% \text{Terms} & t & ::= & v \\
+% & & \ \ | & \texttt{let} \ \expr{x} = \texttt{new} \ \type{C}(\overline{v}) \ \texttt{in} \ t \\
+% & & \ \ | & \texttt{let} \ \expr{x} = v.f \ \texttt{in} \ t \\
+% & & \ \ | & \texttt{let} \ \expr{x} = v.\texttt{m}(\overline{v}) \ \texttt{in} \ t \\
+% & & \ \ | & \texttt{let} \ \expr{x} = v \elvis{} v \ \texttt{in} \ t \\
+% \text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
+% \hline
+% \end{array}
+% $
+% \caption{Input Syntax}\label{fig:syntax}
+% \end{figure}
+
+% \begin{figure}
+% $
+% \begin{array}{lrcl}
+% \hline
+% \text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
+% \text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
+% \text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
+% \text{Type variable contexts} &  \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
+% \text{Class declarations} &  D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\
+% \text{Method declarations} &  \texttt{M} & ::= & \texttt{m}(\overline{\expr{x}}) = t \\
+% \text{Terms} & t & ::= & \expr{x} \\
+% & & \ \ | & \texttt{let} \ \expr{x} = t \ \texttt{in} \ t \\
+% & & \ \ | & \expr{x}.f \\
+% & & \ \ | & \expr{x}.\texttt{m}(\overline{\expr{x}}) \\
+% & & \ \ | & t \elvis{} t \\
+% \text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
+% \hline
+% \end{array}
+% $
+% \caption{Input Syntax}\label{fig:syntax}
+% \end{figure}
+
+
+% \begin{figure}
+% $
+% \begin{array}{lrcl}
+% \hline
+% \text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
+% \text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
+% \text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
+% \text{Type variable contexts} &  \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
+% \text{Class declarations} &  D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\
+% \text{Method declarations} &  \texttt{M} & ::= & \texttt{m}(\overline{x}) = t \\
+% \text{Terms} & t & ::= & x \\
+% & & \ \ | & \texttt{new} \ \type{C}(\overline{t})\\
+% & & \ \ | & t.f\\
+% & & \ \ | & t.\texttt{m}(\overline{t})\\
+% & & \ \ | & t \elvis{} t\\
+% \text{Variable contexts} & \Gamma & ::= & \overline{x:\type{T}}\\
+% \hline
+% \end{array}
+% $
+% \caption{Input Syntax}\label{fig:syntax}
+% \end{figure}
+
+\subsection{ANF transformation}
+\newcommand{\anf}[1]{\ensuremath{\tau}(#1)}
+%https://en.wikipedia.org/wiki/A-normal_form)
+Featherweight Java's syntax involves no \texttt{let} statement
+and terms can be nested freely.
+This is similar to Java's syntax.
+To convert it to \TamedFJ{} additional let statements have to be added.
+This is done by a \textit{A-Normal Form} \cite{aNormalForm} transformation shown in figure \ref{fig:anfTransformation}.
+The input of this transformation is a Featherweight Java program in the syntax given \ref{fig:inputSyntax}
+and the output is a \TamedFJ{} program.
+
+\textit{Example:}\\
+\noindent
+\begin{minipage}{0.45\textwidth}
+\begin{lstlisting}[style=fgj,caption=Featherweight Java]
+m(l, v){
+    return l.add(v);
+}
+\end{lstlisting}
+    \end{minipage}%
+    \hfill
+    \begin{minipage}{0.5\textwidth}
+\begin{lstlisting}[style=tfgj,caption=\TamedFJ{} representation]
+m(l, v) = 
+    let x1 = l in
+        let x2 = v in x1.add(x2)
+\end{lstlisting}
+\end{minipage}
+
+
+% $
+% \begin{array}{|lrcl|l}
+% \hline
+% & & & \textbf{Featherweight Java Terms}\\
+% \text{Terms} & t & ::=
+% & \expr{x}
+% \\
+% & & \ \ |
+% & \texttt{new} \ \type{C}(\overline{t})
+% \\
+% & & \ \ |
+% & t.f
+% \\
+% & & \ \ | 
+% & t.\texttt{m}(\overline{t})
+% \\
+% & & \ \ | 
+% & t \elvis{} t\\
+% %
+% \hline
+% \end{array}
+% $
+
+\begin{figure}
+    \begin{center}
+$\begin{array}{lrcl}
+%\text{ANF}
+& \anf{\expr{x}} & = & \expr{x} \\
+& \anf{\texttt{new} \ \type{C}(\overline{t})} & = & \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}}) \\
+& \anf{t.f} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \expr{x}.f \\
+& \anf{t.\texttt{m}(\overline{t})} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \expr{x}.\texttt{m}(\overline{\expr{x}}) \\
+& \anf{t_1 \elvis{} t_2} & = & \anf{t_1} \elvis{} \anf{t_2}
+\end{array}$
+\end{center}
+\caption{ANF Transformation}\label{fig:anfTransformation}
+\end{figure}
+
+% $
+% \begin{array}{lrcl|l}
+% \hline
+% & & & \textbf{Featherweight Java} & \textbf{A-Normal form}  \\
+% \text{Terms} & t & ::=
+% & \expr{x}
+% & \expr{x}
+% \\
+% & & \ \ |
+% & \texttt{new} \ \type{C}(\overline{t})
+% & \texttt{let}\ \overline{x} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{x})
+% \\
+% & & \ \ |
+% & t.f
+% & \texttt{let}\ x = t \ \texttt{in}\ x.f
+% \\
+% & & \ \ | 
+% & t.\texttt{m}(\overline{t})
+% & \texttt{let}\ x_1 = t \ \texttt{in}\ \texttt{let}\ \overline{x} = \overline{t} \ \texttt{in}\ x_1.\texttt{m}(\overline{x})
+% \\
+% & & \ \ | 
+% & t \elvis{} t
+% & t \elvis{} t\\
+% %
+% \hline
+% \end{array}
+% $
+
+
 % Each class type has a set of wildcard types $\overline{\Delta}$ attached to it.
 % The type $\wctype{\overline{\Delta}}{C}{\ol{T}}$ defines a set of wildcards $\overline{\Delta}$,
 % which can be used inside the type parameters $\ol{T}$.
@@ -184,125 +364,118 @@ $\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}$
-\\[1em] % TODO: we need subtyping for FJ without let statements. Problem is \Delta \vdash T witnessed. The \Delta here contains all the let statements beforehand.
-% TODO: maybe do a rule which adds let statements at any place! Goal: a program which Unify calculates a type for is also correct under our type laws and can be converted to LefFJ
-% motivation: do not use normal types as intermediate types. Keep a Pair<X,X> as that and not convert to X,Y.Pair<X,Y>
-% it is possible because the parameters of the method are normal types. we can start capture converting them
-% is it possible to say there exists any \Delta which makes the method body possible?
+\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}
-        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\type{T}} \ \ok \quad \quad
-        \Delta \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
-        \generics{\ol{X \triangleleft U'}} \type{N} \to \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} : \type{T}_r \mid \Delta_G \quad \quad
-        \Delta | \Gamma \vdash \ol{e} : \ol{T} \mid \overline{\Delta_G} \quad \quad
-        \Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
-        \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
-        \\
-        \overline{\Delta_G}, \Delta_G, \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} \mid \Delta', \overline{\Delta}
-    \end{array}
-\end{array}$
-\\[1em]
-$\begin{array}{l}
-    \typerule{T-Call}\\
-    \begin{array}{@{}c}
-        \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
+        \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 \texttt{e}, \ol{e} : \ol{T} \mid \overline{\Delta'} \quad \quad
-        \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}} \quad \quad
-        \Delta \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T}
+        \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 \texttt{e}.\texttt{m}(\ol{e}) : \type{T} \mid \overline{\Delta}, \overline{\Delta'}
-    \end{array}
-\end{array}$
-% \Delta is not allowed to have wildcards depending on eachother. X^Y, Y^T for example
-\\[1em]
-$\begin{array}{l}
-    \typerule{T-Call}\\
-    \begin{array}{@{}c}
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
-        \generics{\ol{X \triangleleft U'}} \type{N} \to \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} : \type{T}_r \quad \quad
-        \Delta | \Gamma \vdash \ol{e} : \ol{T} \quad \quad
-        \Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
-        \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
-        \\
-        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \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}
+        \Delta | \Gamma \vdash \expr{v}.\texttt{m}(\ol{v}) : \type{T}
     \end{array}
 \end{array}$
 \\[1em]
 $\begin{array}{l}
-    \typerule{T-Call}\\
+%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, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
-        \generics{\ol{X \triangleleft U'}} \type{N} \to \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \quad \quad
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok 
+        \Delta | \Gamma \vdash \expr{t}_1 : \type{T}_1 \quad \quad
+        %\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 | \Gamma \vdash \ol{e} : \ol{T} \quad \quad
-        \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}} \quad \quad 
-        \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
-        \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
+        \Delta, \Delta' | \Gamma, \expr{x} : \wctype{}{C}{\ol{X}} \vdash \expr{t}_2 : \type{T}_2 \quad \quad
+        \Delta, \Delta' \vdash  \type{T}_2 <: \type{T} \quad \quad
+        % \text{dom}(\Delta') \subseteq \text{fv}(\type{N})  \quad \quad
+        \Delta \vdash \type{T}, \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{X}} \ \ok
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash \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]
@@ -325,28 +498,10 @@ $\begin{array}{l}
 
 \begin{figure}
 \begin{center}
-    $\begin{array}{l}
-        \typerule{T-Method}\\
-% TODO: do a rule that forbids variables in Delta which are not introduced by a capture conversion
-        \begin{array}{@{}c}
-            \exptype{C}{\ol{X}} \to \ol{T} \to \type{T} \in \mathtt{\Pi}(\texttt{m})\quad \quad
-            \triangle' =  \overline{\type{Y} : \bot .. \type{P}} \quad \quad
-            \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \\
-            \text{dom}(\triangle) = \ol{X} \quad \quad
-            %\texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \ \{ \ldots \} \\
-            \mathtt{\Pi} | \triangle, \triangle', \overline{\triangle} | \ol{x : T}, \texttt{this} : \exptype{C}{\ol{X}} \vdash \texttt{e} : \type{S} \mid \overline{\Delta} \quad \quad 
-            \triangle \vdash \type{S} <: \type{T}
-            \\
-            \hline
-        \vspace*{-0.3cm}\\
-            \mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \text{ in C with } \generics{\ol{Y \triangleleft P}}
-        \end{array}
-    \end{array}$
-    \\[1em]
 $\begin{array}{l}
     \typerule{T-Method}\\
     \begin{array}{@{}c}
-        \exptype{C}{\ol{X}} \to \ol{T} \to \type{T} \in \mathtt{\Pi}(\texttt{m})\quad \quad
+        (\type{T'},\ol{T}) \to \type{T} \in \mathtt{\Pi}(\texttt{m})\quad \quad
         \triangle' =  \overline{\type{Y} : \bot .. \type{P}} \quad \quad
         \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \\
         \text{dom}(\triangle) = \ol{X} \quad \quad
@@ -363,9 +518,9 @@ $\begin{array}{l}
 $\begin{array}{l}
     \typerule{T-Class}\\
     \begin{array}{@{}c}
-        \mathtt{\Pi}' = \mathtt{\Pi} \cup \set{ \exptype{C}{\ol{X}}.\texttt{m} : \ol{T}_\texttt{m} \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M}} \\
-        \mathtt{\Pi}'' = \mathtt{\Pi} \cup \set{ \exptype{C}{\ol{X}}.\texttt{m} :
-            \generics{\ol{X \triangleleft \type{N}}, \ol{Y \triangleleft P}}\ol{T}_\texttt{m} \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M} } \\
+        \mathtt{\Pi}' = \mathtt{\Pi} \cup \set{ \texttt{m} : (\exptype{C}{\ol{X}}, \ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M}} \\
+        \mathtt{\Pi}'' = \mathtt{\Pi} \cup \set{ \texttt{m} :
+            \generics{\ol{X \triangleleft \type{N}}, \ol{Y \triangleleft P}}(\exptype{C}{\ol{X}},\ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M} } \\
         \triangle = \overline{\type{X} : \bot .. \type{U}} \quad \quad
         \triangle \vdash \ol{U}, \ol{T}, \type{N} \ \ok \quad \quad
         \mathtt{\Pi}' | \triangle \vdash \ol{M} \ \ok \text{ in C with} \ \generics{\ol{Y \triangleleft P}}
@@ -409,4 +564,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}