From 72dff3fa36b6dad971d540be4dbe05eb87000613 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Sat, 4 May 2024 13:56:55 +0200
Subject: [PATCH] Finish someList example

---
 unify.tex | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

diff --git a/unify.tex b/unify.tex
index 0c70c91..2e80f36 100644
--- a/unify.tex
+++ b/unify.tex
@@ -74,13 +74,15 @@ $\begin{array}{l}
 %$\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,
+\rulename{Super} and afterwards substituting $\type{String}$ for $\ntv{x}$,
+same for $\type{Integer} \lessdot \ntv{y}$,
 resulting in the two constraints \linebreak[2]
-$\exptype{List}{\type{Integer}} \lessdot {\ntv{r}},
-\exptype{List}{\type{String}} \lessdot {\ntv{r}}$.
-
-
+$\exptype{List}{\type{Integer}} \lessdot {\ntv{r}}$ \linebreak[2] and \linebreak[2]
+$\exptype{List}{\type{String}} \lessdot {\ntv{r}}$.
+Now comes the part where \unify{} creates existential types by applying the \rulename{Same} transformation.
+An existential type is created with fresh type placeholders as upper and lower bound.
+After a substitution all $\tv{r}$ are replaced with this new existential type.
+\unify{} can now determine type replacements for the freshly created bounds $\tv{u}$ and $\tv{l}$.
 \begin{displaymath}
 \prftree[r]{\rulename{Reduce}}{
 \prftree[r]{\rulename{Subst}}{
@@ -96,7 +98,15 @@ $\exptype{List}{\type{Integer}} \lessdot {\ntv{r}},
 \type{Integer} \lessdot \ntv{u}, \ntv{l} \lessdot \type{Integer}}
 \end{displaymath}
 
+In this example a correct solution is $\sigma(\tv{u}) = \type{Object}$ and $\sigma(\tv{l}) = \bot$.
+Remember that the substitution for the type placeholder $\tv{r}$ is $\wctype{\wildcard{X}{\ntv{u}}{\ntv{l}}}{List}{\rwildcard{X}}$
+leading to \texttt{List<?>} as a return type for the \texttt{someList} method after applying $\sigma$.
 
+\begin{lstlisting}
+List<? extends Object> someList(){
+  return new List("String") :? new List(42);
+}
+\end{lstlisting}
 
 \subsection{Description}
 The \unify{} algorithm tries to find a solution for a set of constraints like