Same rule example

constraints.tex

@@ -291,12 +291,12 @@ cannot be used anywhere else then inside the constraints generated by the method
     \typeExpr{} &({\mtypeEnvironment} , \texttt{new}\ \type{C}(\overline{e}), \tv{a}) = \\
                 & \begin{array}{ll}
                     \textbf{let} 
-                    & \ol{\tv{r}} \ \text{fresh} \\
-                    & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \overline{e}, \ol{\tv{r}}) \\
-                    & C = \set{\ol{\tv{r}} \lessdot [\ol{\tv{a}}/\ol{X}]\ol{T}, \ol{\tv{a}} \lessdot \ol{N} \mid \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}} \\
+                    & \ol{\ntv{r}}, \ol{\ntv{a}} \ \text{fresh} \\
+                    & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \overline{e}, \ol{\ntv{r}}) \\
+                    & C = \set{\ol{\ntv{r}} \lessdot [\ol{\ntv{a}}/\ol{X}]\ol{T}, \ol{\ntv{a}} \lessdot \ol{N} \mid \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}} \\
                     {\mathbf{in}} & {
                     \overline{\consSet} \cup
-                        \set{\tv{a} \doteq \exptype{C}{\ol{a}}}}
+                        \set{\tv{a} \doteq \exptype{C}{\ol{\ntv{a}}}}}
                   \end{array} 
   \end{array}
 \end{displaymath}

unify.tex

@@ -8,6 +8,32 @@
 \section{Unify}\label{sec:unify}
 
 \subsection{Adding Wildcards to the mix}
+Input constraints originating from a completely untyped input program do not contain any existential types.
+Those are added during \unify{}.
+The only parts where existential types are created are the \rulename{Match} and \rulename{General} rules.
+Existential types can only be a supertype of normal types and never a subtype.
+Except when used as an argument to a method invocation (see discussion in chapter \ref{sec:completeness}). 
+
+\unify{} works with the principle that type terms are reduced until constraints
+of the form $\tv{a} \doteq \type{T}$ remain and we have a type solution.
+This is for example done by the \rulename{Reduce} transformation, which works according to the S-Exists subtyping rule.
+Existential types are created during the unificaiton process by the \rulename{Same} rule.
+This rule always comes with a substitution and a \rulename{Reduce} transformation.
+
+\textit{Example:}
+\begin{displaymath}
+\prftree[r]{\rulename{Reduce}}{
+\prftree[r]{\rulename{Subst}}{
+\prftree[r]{\rulename{Same}}{\exptype{List}{\type{Integer}} \lessdot \tv{r}}
+{\exptype{List}{\type{Integer}} \lessdot \tv{r},
+\tv{r} \doteq \wctype{\wildcard{X}{\ntv{u}}{\ntv{l}}}{List}{\rwildcard{X}}
+}}
+{\exptype{List}{\type{Integer}} \lessdot \wctype{\wildcard{X}{\ntv{u}}{\ntv{l}}}{List}{\rwildcard{X}}}
+}
+{\type{Integer} \lessdot \ntv{u}, \ntv{l} \lessdot \type{Integer}}
+\end{displaymath}
+
+
 %Wildcard creation. % TODO: Explain by the example from the Bad Honnef Talk
 %Wildcards are bound to a type.
 % and can therefore only be created at T <. a constraints
@@ -23,17 +49,53 @@ someList(){
 Constraints for the untyped \texttt{someList} method:
 \begin{constraintset}
 $\begin{array}{l}
-\exptype{List}{\tv{x}} \lessdot {\tv{r}}, \type{String} \lessdot {\tv{x}},
-\exptype{List}{\tv{y}} \lessdot {\tv{r}}, \type{Integer} \lessdot {\tv{y}}
+\exptype{List}{\ntv{x}} \lessdot {\ntv{r}}, \type{String} \lessdot {\ntv{x}},
+\exptype{List}{\ntv{y}} \lessdot {\ntv{r}}, \type{Integer} \lessdot {\ntv{y}}
 \end{array}$
 \end{constraintset}
 
+
+\begin{displaymath}
+\prftree[r]{\rulename{Subst}}
+{
+  \prftree[r]{\rulename{Same}}{\type{String} \lessdot \ntv{x}}
+  {\type{String} \lessdot \ntv{x}, \ntv{x} \doteq \type{String}}
+}
+{
+  \prftree[r]{\rulename{Same}}{\type{Integer} \lessdot \ntv{y}}
+  {\type{Integer} \lessdot \ntv{y}, \ntv{y} \doteq \type{Integer}}
+}
+{
+\prftree[r]{\rulename{Reduce}}{\type{String} \lessdot \type{String}, \type{Integer} \lessdot \type{Integer}, \ntv{x} \doteq \type{String}, \ntv{y} \doteq \type{Integer}}
+{\ntv{x} \doteq \type{String},\ntv{y} \doteq \type{Integer}} 
+}
+\end{displaymath}
+%After another substitution this leads to the constraints:
+%$\exptype{List}{\type{String}} \lessdot {\ntv{r}}, \exptype{List}{\type{Integer}} \lessdot {\ntv{r}}$
+
 The constraint $\type{String} \lessdot {\ntv{x}}$ is solved by applying
 \rulename{Super} and substituting $\type{String}$ for $\ntv{x}$.
+The same for $\type{Integer} \lessdot \ntv{y}$ accordingly,
+resulting in the two constraints \linebreak[2]
+$\exptype{List}{\type{Integer}} \lessdot {\ntv{r}},
+\exptype{List}{\type{String}} \lessdot {\ntv{r}}$.
+
+
+\begin{displaymath}
+\prftree[r]{\rulename{Reduce}}{
+\prftree[r]{\rulename{Subst}}{
+\prftree[r]{\rulename{Same}}{\exptype{List}{\type{Integer}} \lessdot \tv{r},\exptype{List}{\type{Integer}} \lessdot \tv{r}}
+{\exptype{List}{\type{String}} \lessdot \tv{r},
+\exptype{List}{\type{Integer}} \lessdot \tv{r},
+\tv{r} \doteq \wctype{\wildcard{X}{\ntv{u}}{\ntv{l}}}{List}{\rwildcard{X}}
+}}
+{\exptype{List}{\type{String}} \lessdot \wctype{\wildcard{X}{\ntv{u}}{\ntv{l}}}{List}{\rwildcard{X}},
+\exptype{List}{\type{Integer}} \lessdot \wctype{\wildcard{X}{\ntv{u}}{\ntv{l}}}{List}{\rwildcard{X}}}
+}
+{\type{String} \lessdot \ntv{u}, \ntv{l} \lessdot \type{String},
+\type{Integer} \lessdot \ntv{u}, \ntv{l} \lessdot \type{Integer}}
+\end{displaymath}
 
-Input constraints originating from a completely untyped input program do not contain any existential types.
-Those are added during \unify{}.
-The only parts where existential types are created are the \rulename{Match} and \rulename{General} rules.
 
 
 \subsection{Description}
@@ -1400,7 +1462,7 @@ But this renders additional problems:
 \end{itemize}
 
 
-\subsection{Completeness}
+\subsection{Completeness}\label{sec:completeness}
 It is not possible to create all super types of a type.
 The General rule only creates the ones expressable by Java syntax, which still are infinitly many in some cases \cite{TamingWildcards}.
 %thats not true. it can spawn X^T_T2.List<X> where T and T2 are types and we need to choose one inbetween them
@@ -1408,6 +1470,48 @@ Otherwise the algorithm could generate more solutions, but they have to be filte
 
 \letfj{} is not able to represent all Java programs. %TODO: this makes ist impossible for our algorithm to be complete on Java
 
+%Loss of completeness:
+% a <. b, b <c List<x>
+
+% Example
+\begin{lstlisting}
+m(l){
+  return let x = l in x.add(1);
+}
+\end{lstlisting}
+Here generality is lost.
+Constraints: $\ntv{l} \lessdot \ntv{x}, \ntv{x} \lessdotCC \exptype{List}{\wtv{x}}$
+
+Correct solution would be:
+\begin{lstlisting}
+m(List<? super Int> l){
+  return let x = l in x.add(1);
+}
+\end{lstlisting}
+
+Our solution:
+\begin{lstlisting}
+<X extends List<Integer> m(X l){
+  return let x = l in x.add(1);
+}
+m(List<? super Integer>)
+\end{lstlisting}
+$\tv{a} \lessdotCC \type{T}$ constraints allow for existential types on the left side,
+because there will be a capture conversion.
+We do not cover this and only apply capture conversion when the left side is known.
+So $\tv{a}$ will not be assigned a existential type, which explains our less general solution.
+
+If all of the program is given this may be not much of an issue.
+The $\tv{a} \lessdotCC \type{T}$ constraint is kept until the end and if the method
+is called and $\tv{a}$ gets a type, then this type can be an existential type aswell.
+
+% Problem: There are infinite subtypes to a type Pair<x,y> when capture conversion is allowed 
+
+% a <. b, b <c List<X>
+% b <. X.List<X>, X.List<X> <c List<x> (is this sound? -> yes)
+% ( is this complete? X,Y.Pair<X,Y> <c X.Pair<X,X>)
+
+
 \subsection{Implementation}
 %List this under implementation details
 Every constraint that is not in solved form and is not able to be processed by any of the rules accounts as a error constraint and renders the constraint set unsolvable