introduction.tex

@@ -509,23 +509,11 @@ 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() { ... }
 
-concat(getList(), getList());
+List<?> list = ... ;
+concat(list, list);
 \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}}$
@@ -548,30 +536,79 @@ let x1 : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = getList() in
 % 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{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.
+\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>{}
 
-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.
 
-%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?>
+<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>
+
 
 \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]{\ensuremath{\mathtt{#1}}}
+\newcommand{\type}[1]{\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}\label{sec:anfTransformation}
+\subsection{ANF transformation}\ref{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,47 +115,14 @@ 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 have to be replaced with normal placeholders.
+As soon as they appear in a $\ntv{a} \doteq \type{T}$ constraint they can no longer be replaced by free variables.
 
 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}
-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}
+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.
 
 \subsection{Algorithm}
 
@@ -471,14 +438,18 @@ 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<X>
-% ---------
-% a <. C<U>, U = L
+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
 
 %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