From ba8e2fadbb644985c9f90266df9e6af7c61f7f6d Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Sun, 21 Jan 2024 14:31:48 +0100
Subject: [PATCH] Add Capture Conversion during unification chapter

---
 unify.tex | 62 ++++++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 61 insertions(+), 1 deletion(-)

diff --git a/unify.tex b/unify.tex
index ea44853..286b011 100644
--- a/unify.tex
+++ b/unify.tex
@@ -63,7 +63,7 @@ Capture conversion removes a types bounding environment $\Delta$.
 Type variables used in its type parameters are now bound to a global scope and not locally anymore.
 
 With \texttt{C} being class names and \texttt{A} being wildcard names.
-The wildcard type $\wildcard{X}{U}{L}$ consist out of an upper bound $\type{U}$, a lower bound $\type{L}$
+The wildcard type $\wildcard{X}{U}{L}$ consist of an upper bound $\type{U}$, a lower bound $\type{L}$
 and a name $\mathtt{X}$.
 
 The \rulename{Normalize} rule eliminates wildcards. % TODO
@@ -1137,3 +1137,63 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
 % \end{center}
 % \caption{Common transformations}\label{fig:wildcard-rules}
 % \end{figure}
+
+
+\subsection{Capture Conversion during Unification}
+The \unify{} algorithm applies a capture conversion when needed.
+A constraint of the form $\wcNtype{\Delta'}{N} \lessdot \type{T}$,
+where $\text{fv}(\type{T}) \neq \emptyset$ is not solvable without capture conversion.
+\unify{} converts those constraints to $\type{N} \lessdot \type{T}$.
+This is only possible for subtype constraints which originated from a method call.
+
+Capture conversion only works with constraints containing free variables.
+It also introduces fresh free variables into the constraint set.
+Both have to be regulated.
+It is not allowed to substitute free type variables freely.
+The algorithm introduces a new type of variables: $\wtv{a}$.
+\unify{} treats those as free type variables.
+This makes it possible to replace a $\wtv{a}$ with a captured wildcard variable
+without having to worry about introducing free type variables at unwanted places.
+
+The challenge for a type inference algorithm is to apply capture conversion during type inference.
+Given a program 
+\begin{verbatim}
+class TypeInferenceExample{
+	m(l){
+		return swap(make(l));
+	}
+}
+\end{verbatim}
+
+During the time of the type inference algorithm the type of the parameter \texttt{l} is not known.
+Due to the call to the method \texttt{make} it is clear that it has to be a subtype of
+\texttt{List}.
+These subtype relations are expressed with constraints.
+$\tv{l} \lessdot \exptype{List}{\tv{a}}$ in this case.
+$\tv{l}$ and $\tv{a}$ are type placeholders.
+$\tv{l}$ is a type placeholder for the method parameter \texttt{l}.
+
+One correct solution for this constraint is the substitution $\tv{l} \doteq \exptype{List}{\type{Object}}$,
+which leads to the program:
+\begin{verbatim}
+	class TypeInferenceExample{
+		Pair<Object, Object> m(List<Object> l){
+			return swap(make(l));
+		}
+	}	
+\end{verbatim}
+
+But $\tv{l} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ is also a possible solution.
+Eventhough the constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\tv{a}}$
+is not solvable.
+But when we apply capture conversion to create $\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\tv{a}}$
+we can substitute $\tv{a} \doteq \rwildcard{Y}$.
+
+The \unify{} algorithm has to apply capture conversions during the unification of type constraints.
+
+But this renders additional problems:
+\begin{itemize}
+	\item Capture conversion is not allowed for every constraint.
+	\item Capture Converted variables are not allowed to leave their scope
+	\item \unify{} generates type substitution which cannot be translated to Java types.
+\end{itemize}