Add LessdotCC introduction

introduction.tex

@@ -172,32 +172,55 @@ m(l) {
 
 $\tv{l} \lessdotCC \exptype{List}{\wtv{x}}, \tv{l} \lessdotCC \wtv{x}$
 
-% One possible solution:
-% \begin{verbatim}
-% List<Object> m(List<Object> l) {
-%     return l.add(l);
-% }
-% \end{verbatim}
 
-% No capture conversion for methods in the same class:
-% \begin{verbatim}
-% m() = new List<String>() :? new List<Integer>();
-% id(a) = a
+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(m())
-% \end{verbatim}
-% id will get type List<?> -> List<?>
-% % explain polymorphic recursion here
-% % no capture conversion needed
+// id :: (a) -> a
+id(a) = a
+\end{verbatim}
 
-% The id method is pre typed:
-% \begin{verbatim}
-% <A> List<A> id(List<A> a) = a
+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}
 
-% m() = new List<String>() :? new List<Integer>() :? id(m());
-% \end{verbatim}
-% constraint m :: p -> r
-% % Wildcards are only deleted in unify, never generated.
 
 \subsection{Java Wildcards}
 Wildcards are expressed by a \texttt{?} in Java and can be used as parameter types.
@@ -207,9 +230,10 @@ denoted in our syntax by $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwil
 $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
 
 Wildcards add variance to Java type parameters.
-In Java a \texttt{List<String>} is not a subtype of \texttt{List<Object>}
+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}.
-Here wildcards come into play.
+
 
 $\exptype{List}{String} <: \wctype{\wildcard{X}{\bot}{\type{Object}}}{List}{\rwildcard{X}}$
 means \texttt{List<String>} is a subtype of \texttt{List<? extend Object>}.
@@ -338,6 +362,30 @@ Remember that the given constraints cannot have a valid solution.
 In this example the \unify{} algorithm should not replace $\tv{a}$ with the captured wildcard $\rwildcard{X}$.
 \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}}$
+
+\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 = ...;
+
+m2() {
+  l.add(l.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.
+
+
 \end{itemize}
 
 The \unify{} algorithm only sees the constraints with no information about the program they originated from.