From 24cfd8cb759c9376d904bff5d88e8efafc32020c Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <stan@hb.dhhbw-stuttgart.de>
Date: Wed, 10 Apr 2024 17:40:49 +0200
Subject: [PATCH] Rephrase Triple example

---
 introduction.tex | 84 +++++++++++++++++++++++-------------------------
 1 file changed, 41 insertions(+), 43 deletions(-)

diff --git a/introduction.tex b/introduction.tex
index 800171e..2b9fa3b 100644
--- a/introduction.tex
+++ b/introduction.tex
@@ -561,6 +561,47 @@ As soon as enough type information is given \unify{} can conduct a capture conve
 The constraints where this is possible are marked as capture constraints.
 
 \section{Discussion Pair Example}
+\begin{verbatim}
+<X> Pair<X,X> make(List<X> l){ ... }
+<X> boolean compare(Pair<X,X> p) { ... }
+
+List<?> l;
+Pair<?,?> p;
+
+compare(make(l)); // Valid
+compare(p); // Error
+\end{verbatim}
+
+Our type inference algorithm is not able to solve this example.
+When we convert this to \TamedFJ{} and generate constraints we end up with:
+\begin{lstlisting}[style=tamedfj]
+let m = let x = l in make(x) in compare(m)
+\end{lstlisting}
+\begin{constraintset}$
+\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \ntv{x},
+\ntv{x} \lessdotCC \exptype{List}{\wtv{a}}
+\exptype{Pair}{\wtv{a}, \wtv{a}} \lessdot \ntv{m}, %% TODO: Mark this constraint
+\ntv{m} \lessdotCC \exptype{Pair}{\wtv{b}, \wtv{b}}
+$\end{constraintset}
+
+$\ntv{x}$ will get the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and
+from the constraint
+$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
+\unify{} deducts $\wtv{a} \doteq \rwildcard{X}$ leading to 
+$\exptype{Pair}{\rwildcard{X}, \rwildcard{X}} \lessdot \ntv{m}$.
+
+Finding a supertype to $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ is the crucial part.
+The correct substition for $\ntv{m}$ would be $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$.
+But this leads to additional branching inside the \unify{} algorithm and increases runtime.
+%We refrain from using that type, because it is not denotable with Java syntax.
+%Types used for normal type placeholders should be expressable Java types. % They are not!
+
+The prefered way of dealing with this example in our opinion would be the addition of a multi-let statement to the syntax.
+
+\begin{lstlisting}[style=letfj]
+let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = l, m = make(x) in compare(make(x))
+\end{lstlisting}
+
 We can make it work with a special rule in the \unify{}.
 But this will only help in this specific example and not generally solve the issue.
 A type $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ has atleast two immediate supertypes:
@@ -599,49 +640,6 @@ $
 \end{constraintset}
 
 
-\begin{verbatim}
-<X> Pair<X,X> make(List<X> l){ ... }
-<X> boolean compare(Pair<X,X> p) { ... }
-
-List<?> l;
-Pair<?,?> p;
-
-compare(make(l)); // Valid
-compare(p); // Error
-\end{verbatim}
-
-Our type inference algorithm is not able to solve this example.
-When we convert this to \TamedFJ{} and generate constraints we end up with:
-\begin{lstlisting}[style=tamedfj]
-let m = let x = l in make(x) in compare(m)
-\end{lstlisting}
-\begin{constraintset}$
-\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \ntv{x},
-\ntv{x} \lessdotCC \exptype{List}{\wtv{a}}
-\exptype{Pair}{\wtv{a}, \wtv{a}} \lessdot \ntv{m}, %% TODO: Mark this constraint
-\ntv{m} \lessdotCC \exptype{Pair}{\wtv{b}, \wtv{b}}
-$\end{constraintset}
-
-$\ntv{x}$ will get the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and
-from the constraint
-$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
-\unify{} deducts $\wtv{a} \doteq \rwildcard{X}$ leading to 
-$\exptype{Pair}{\rwildcard{X}, \rwildcard{X}} \lessdot \ntv{m}$.
-
-Finding a supertype to $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ is the crucial part.
-The correct substition for $\ntv{m}$ would be $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$.
-We refrain from using that type, because it is not denotable with Java syntax.
-Types used for normal type placeholders should be expressable Java types.
-
-The prefered way of dealing with this example in our opinion would be the addition of a multi-let statement to the syntax.
-
-
-\begin{lstlisting}[style=letfj]
-let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = l in let m = make(x) in compare(m)
-\end{lstlisting}
-
-
-
 \end{itemize}
 
 %TODO: Move this part. or move the third challenge some underneath.