Explain let scoping in unify

introduction.tex

@@ -509,11 +509,23 @@ The method call to \texttt{concat} with two wildcard lists is unsound.
 Each list could be of a different kind and therefore the \texttt{concat} cannot succeed.
 \begin{verbatim}
 <A> List<A> concat(List<A> l1, List<A> l2) { ... }
+List<?> getList() { ... }
 
-List<?> list = ... ;
-concat(list, list);
+concat(getList(), getList());
 \end{verbatim}
 
+The \letfj{} representation in listing \ref{letfjConcatFail} clarifies this.
+Inside the let statement the variables hold the types
+$\set{ \texttt{x1} : \exptype{List}{\rwildcard{X}}, \texttt{x2} : \exptype{List}{\rwildcard{Y}}}$.
+For the method call \texttt{concat(x1, x2)} no replacement for the generic \texttt{A}
+exists to satisfy
+$\exptype{List}{\type{A}} <: \exptype{List}{\type{X}},
+\exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$.
+\begin{lstlisting}[style=letfj,caption=Incorrect method call,label=letfjConcatFail]
+let x1 : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = getList() in
+  let x2 : (*@$\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}$@*) = getList() in
+    concat(x1, x2)
+\end{lstlisting}
 
 % $\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}}$
@@ -536,79 +548,30 @@ concat(list, list);
 % An additional constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
 % is solved by removing the wildcard $\rwildcard{X}$ if possible.
 
-\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>{}
+\item \textbf{Capture Conversion during \unify{}:}
+The return type of a generic method call depends on its argument types.
+A method like \texttt{String trim(String s)} will always return a \type{String} type.
+However the return type of \texttt{<A> A head(List<A> l)} is a generic variable \texttt{A} and only shows
+its actual type when the type of the argument list \texttt{l} is known.
+The same goes for capture conversion, which can only be applied for a method call
+when the argument types are given.
+At the start of our global type inference algorithm no types are assigned yet.
+During the course of the \unify{} algorithm more and more types emerge.
+As soon as enough type information is given \unify{} can conduct a capture conversion if needed.
+The constraints where this is possible are marked as capture constraints.
 
+Type information flows top down.
+Argument types of a method invocation impact its return type.
+But knowing the return type does not imply distinct argument types.
+The code in listing \ref{principalTypeExample} shows a nested method call
+\texttt{receive(copy(lSpecial))}.
+We know from the argument types of \texttt{receive} -which are given- that the \texttt{copy} method
+needs to return a type of the form $\exptype{Pair}{\type{X}, \type{Y}}$
+where \type{X} and \type{Y} can be any types as long as \type{Y} is a subtype of \type{X}.
+Without wildcards this would leave us with a clue what the type should look like.
 
-<X,Y> Pair<X,Y> id(Pair<X,Y> in){
-  return in;
-}
-
-<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>
-
+%TODO: simplify this example. lSpeial <. List<x> and List<x> <. id is sufficient
+% The unify algorithm needs to resolve l <c List<x?> to l <. X.List<X>, X.List<X> <c List<x?>
 
 \end{itemize}
 

prolog.tex

@@ -97,7 +97,7 @@
 \newcommand{\constraints}{\ensuremath{\mathit{\overline{c}}}}
 \newcommand{\itype}[1]{\ensuremath{\mathit{#1}}}
 \newcommand{\il}[1]{\ensuremath{\overline{\itype{#1}}}}
-\newcommand{\type}[1]{\mathtt{#1}}
+\newcommand{\type}[1]{\ensuremath{\mathtt{#1}}}
 \newcommand{\anyType}[1]{\mathit{#1}}
 \newcommand{\gType}[1]{\texttt{#1}}
 \newcommand{\mtypeEnvironment}{\ensuremath{\Pi}}

tRules.tex

@@ -132,7 +132,7 @@ $
 % \caption{Input Syntax}\label{fig:syntax}
 % \end{figure}
 
-\subsection{ANF transformation}\ref{sec:anfTransformation}
+\subsection{ANF transformation}\label{sec:anfTransformation}
 \newcommand{\anf}[1]{\ensuremath{\tau}(#1)}
 %https://en.wikipedia.org/wiki/A-normal_form)
 Featherweight Java's syntax involves no \texttt{let} statement

unify.tex

@@ -115,14 +115,47 @@ The vital part are the \rulename{Subst} and \rulename{Normalize} rules.
 They assert that a normal type placeholder is never replaced by a type containing free variables.
 \rulename{Normalize} replaces Wildcard placeholders with normal placeholders right before they get substituted by \rulename{Subst}.
 The idea is to keep the possibility of replacing a wildcard placeholder with a free variable as long as possible.
-As soon as they appear in a $\ntv{a} \doteq \type{T}$ constraint they can no longer be replaced by free variables.
+As soon as they appear in a $\ntv{a} \doteq \type{T}$ constraint they have to be replaced with normal placeholders.
 
 A type solution for a normal type placeholder will never contain free variables.
 This is needed to guarantee well-formed type solutions and also keep free variables inside their scope.
 
+\begin{example}{Free variables must not leave the scope of the surrounding \texttt{let} statement}
+
+\noindent
+\begin{minipage}{0.40\textwidth}
 \begin{lstlisting}
-let y = { let x = v in v.get() } in y.get()
-\end{lstlisting} %TODO: explain: here y has to be a type without free variables.
+m(l) = let v = l in v.get()
+\end{lstlisting} 
+\end{minipage}%
+\hfill
+\begin{minipage}{0.59\textwidth}
+\begin{constraintset}
+$\tv{l} \lessdot \tv{v}, \tv{v} \lessdotCC \exptype{List}{\wtv{x}},
+\wtv{x} \lessdot \tv{r}$
+\end{constraintset}
+\end{minipage}
+Lets assume the variables \texttt{l} and \texttt{v}
+get the type $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$ assigned to them.
+After application of the \rulename{Capture} and \rulename{SubstWC} rules the constraint set looks like this:
+
+$\begin{array}[c]{l}
+\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}, \wtv{x} \lessdot \ntv{r}
+  \\
+\hline
+\vspace*{-0.4cm}\\
+\wildcard{X}{\type{Object}}{\type{String}} \vdash \wtv{x} \doteq \rwildcard{X}, \rwildcard{X} \lessdot \ntv{r}
+\end{array}
+$
+
+Replacing $\tv{r}$ with $\rwildcard{X}$ would solve the constraint set but lead to the method type
+
+\texttt{X m(List<? super String> l)} which makes no sense.
+The normal type placeholder $\ntv{r}$ has to be replaced by a type without free type variables
+($\ntv{r} \doteq \type{Object}$) leading to
+
+\texttt{Object m(List<? super String> l)}.
+\end{example}
 
 \subsection{Algorithm}
 
@@ -438,18 +471,14 @@ C \cup [\type{U}/\type{A}]\set{\ntv{a} \doteq \type{T}, \type{L} \doteq \type{U}
 There are n different rules to deal with $\type{N} \lessdot \type{N}$ constraints.
 Prepare, Capture, Reduce, Trim, Clear, Exclude, Adapt
 
+% % TODO: 
+% a <c C<X> 
+% -------------
+% a <. X.C<X>, X.C<X> <c C<X>
 
-a <c C<x?>
-x? =. X
-a <c C<X>
-
-a <c C<X> 
--------------
-a <. X.C<X>, X.C<X> <c C<X>
-
-a <. C<X>
----------
-a <. C<U>, U = L
+% a <. C<X>
+% ---------
+% a <. C<U>, U = L
 
 %The capture constraints are preserved when applying the \rulename{Upper} rule.
 % This is legal: a T <c S constraint indicates a let-statement can be inserted. Therefore there must exist a type T' with T <. T' <c S