From 5cd90a9593280aa9c27d1af7dd25551d0da86e09 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Mon, 6 May 2024 12:11:57 +0200
Subject: [PATCH] Start Wildcard elimination example

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

diff --git a/unify.tex b/unify.tex
index 2e80f36..dfe4f12 100644
--- a/unify.tex
+++ b/unify.tex
@@ -108,6 +108,22 @@ List<? extends Object> someList(){
 }
 \end{lstlisting}
 
+\subsection{Wildcard Elimination Example}
+\begin{lstlisting}
+  <X> List<X> concat(List<X> l, List<X> l2){ ... }
+  someList(){
+    return new List("String") :? new List(42);
+  }
+
+  concat(someList(), someList());
+\end{lstlisting}
+
+Let's add an additional method call to the previous example.
+The \texttt{concat} method takes two lists of the same generic type.
+\texttt{concat} cannot be invoked with two existential lists.
+%TODO: Explain capture conversion
+
+
 \subsection{Description}
 The \unify{} algorithm tries to find a solution for a set of constraints like
 $\set{\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}}$.