From 2e0909dceaa1ccc9850a6e674f45f85805e86ab3 Mon Sep 17 00:00:00 2001
From: Andreas Stadelmeier <andi@paulus.haus>
Date: Fri, 26 Apr 2024 22:50:48 +0200
Subject: [PATCH] Cleanup. Add Unify example why free variables are not allowed
 to leave scope

---
 vortrag.tex | 334 ++++++++++++++++++++++++++++++++--------------------
 1 file changed, 208 insertions(+), 126 deletions(-)

diff --git a/vortrag.tex b/vortrag.tex
index 8dc9469..8bf84b0 100644
--- a/vortrag.tex
+++ b/vortrag.tex
@@ -19,11 +19,11 @@
 $\begin{array}{l}
     \begin{array}{@{}c}
         \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad
-        \Delta \vdash  \ol{v} : [\ol{T'}/\ol{X}]\ol{T}
+        \ol{v} : [\ol{T'}/\ol{X}]\ol{T}
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \Delta \vdash \generics{\ol{T'}}\texttt{m}(\ol{v}) : [\ol{T'}/\ol{X}]\type{T}
+        \generics{\ol{T'}}\texttt{m}(\ol{v}) : [\ol{T'}/\ol{X}]\type{T}
     \end{array}
 \end{array}$
 \end{center}
@@ -36,11 +36,11 @@ $\generics{\type{String}}\texttt{emptyList}() : \exptype{List}{\type{String}}$
 $\begin{array}{l}
     \begin{array}{@{}c}
         \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad
-        \Delta \vdash  \expr{v}, \ol{v} : [\ol{T'}/\ol{X}]\ol{T}
+        \ol{v} : [\ol{T'}/\ol{X}]\ol{T}
         \\
         \hline
     \vspace*{-0.3cm}\\
-        \Delta \vdash \expr{v}.\texttt{m}(\ol{v}) : [\ol{T'}/\ol{X}]\type{T}
+        \texttt{m}(\ol{v}) : [\ol{T'}/\ol{X}]\type{T}
     \end{array}
 \end{array}$
 \end{center}
@@ -50,38 +50,38 @@ $\texttt{emptyList}() : \exptype{List}{\type{String}}$
 \end{frame}
 
 
-\begin{frame}[fragile]
-\frametitle{Java Method Call}
-\rulename{M-Class} \\[1em]
-\begin{center}
-$\begin{array}{l}
-    \begin{array}{@{}c}
-    \generics{\ol{X}}\ \type{T} \ \texttt{m}(\ol{T\ x}) \set{ \ldots }
-        \\
-        \hline
-    \vspace*{-0.3cm}\\
-       \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T}
-    \end{array}
-\end{array}$
-\end{center}
+% \begin{frame}[fragile]
+% \frametitle{Java Method Call}
+% \rulename{M-Class} \\[1em]
+% \begin{center}
+% $\begin{array}{l}
+%     \begin{array}{@{}c}
+%     \generics{\ol{X}}\ \type{T} \ \texttt{m}(\ol{T\ x}) \set{ \ldots }
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%        \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T}
+%     \end{array}
+% \end{array}$
+% \end{center}
 
-\textbf{Beispiele:}\\
-\begin{verbatim}
-X head(List<X> l) { ... }
-\end{verbatim}
-\begin{itemize}
-\item 
-$\textit{mtype}(\texttt{head}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \type{X}$
-\end{itemize}
+% \textbf{Beispiele:}\\
+% \begin{verbatim}
+% X head(List<X> l) { ... }
+% \end{verbatim}
+% \begin{itemize}
+% \item 
+% $\textit{mtype}(\texttt{head}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \type{X}$
+% \end{itemize}
 
-\begin{verbatim}
-<X> List<X> emptyList() { ... }
-\end{verbatim}
-\begin{itemize}
-\item 
-$\textit{mtype}(\texttt{emptyList}) = \generics{\type{X}}\ [] \to \exptype{List}{\type{X}}$
-\end{itemize}
-\end{frame}
+% \begin{verbatim}
+% <X> List<X> emptyList() { ... }
+% \end{verbatim}
+% \begin{itemize}
+% \item 
+% $\textit{mtype}(\texttt{emptyList}) = \generics{\type{X}}\ [] \to \exptype{List}{\type{X}}$
+% \end{itemize}
+% \end{frame}
 
 \begin{frame}[fragile]
 \frametitle{Java Method Call}
@@ -99,114 +99,148 @@ $\begin{array}{l}
 \end{array}$
 \end{center}
 \textbf{Beispiel:}\\
+\begin{verbatim}
+<X> X head(List<X> l){ ... }
+
+head(new List<String>());
+\end{verbatim}
+\pause
 $\begin{array}{l}
     \begin{array}{@{}c}
-        \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad
+        \textit{mtype}(\texttt{head}) = \generics{\ol{X}}\ \exptype{List}{\type{X}} \to \type{X} \\
         \texttt{new List<String>}() : [\type{String}/\type{X}]\exptype{List}{\type{X}}
         \\
         \hline
     \vspace*{-0.3cm}\\
         \generics{\type{String}}\texttt{head}(\texttt{new List<String>}()) : [\type{String}/\type{X}]\type{X}
     \end{array}
-\end{array}$
+\end{array}$\\[1em]
 \pause
-$\begin{array}{l}
-    \begin{array}{@{}c}
-        \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad
-        \texttt{new List<String>}() : \exptype{List}{\type{String}}
-        \\
-        \hline
-    \vspace*{-0.3cm}\\
-        \generics{\type{String}}\texttt{head}(\texttt{new List<String>}()) : \type{String}
-    \end{array}
-\end{array}$
+% $\begin{array}{l}
+%     \begin{array}{@{}c}
+%         \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad
+%         \texttt{new List<String>}() : \exptype{List}{\type{String}}
+%         \\
+%         \hline
+%     \vspace*{-0.3cm}\\
+%         \generics{\type{String}}\texttt{head}(\texttt{new List<String>}()) : \type{String}
+%     \end{array}
+% \end{array}$
+
+\begin{itemize}
+    \item \texttt{head(new List<String>()) : String}
+\end{itemize}
 \end{frame}
 
-\begin{frame}[fragile]
-\frametitle{Java Method Call}
+% \begin{frame}[fragile]
+% \frametitle{Java Method Call}
 
+% \begin{verbatim}
+% head(head(emptyList()))
+% \end{verbatim}
+
+% $
+% \begin{array}[b]{c}
+% \texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}} \\
+% \quad \textit{mtype}(\texttt{get}) = \generics{X}\ \exptype{List}{\type{X}} \to \type{X}
+% \\
+% \hline
+% \texttt{head(emptyList())} : \exptype{List}{\type{String}}
+% \end{array} \rulenameAfter{T-Call}
+% $
+% \end{frame}
+
+% \begin{frame}[fragile]
+% \frametitle{Java Method Call}
+% $
+% \begin{array}[b]{c}
+% \texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}} \\
+% \quad \textit{mtype}(\texttt{get}) = \generics{X}\ \exptype{List}{\type{X}} \to \type{X}
+% \\
+% \hline
+% \generics{\exptype{List}{\exptype{List}{\type{String}}}}\texttt{head(emptyList())} : \exptype{List}{\type{String}}
+% \end{array} \rulenameAfter{T-Call}
+% $
+
+% $
+% \begin{array}[b]{c}
+% \texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}} \\
+% \quad \textit{mtype}(\texttt{get}) = \generics{X}\ \exptype{List}{\type{X}} \to \type{X}
+% \\
+% \hline
+% \generics{\exptype{List}{\type{String}}}\texttt{head(emptyList())} : \exptype{List}{\type{String}}
+% \end{array} \rulenameAfter{T-Call}
+% $
+% \end{frame}
+
+% \begin{frame}[fragile]
+% \frametitle{Java Method Call}
+
+% $
+% \begin{array}[b]{c}
+% \texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}} \\
+% \quad \textit{mtype}(\texttt{get}) = \generics{X}\ \exptype{List}{\type{X}} \to \type{X}
+% \\
+% \hline
+% \generics{\exptype{List}{\type{String}}}\texttt{head(emptyList())} : \exptype{List}{\type{String}}
+% \end{array} \rulenameAfter{T-Call}
+% $
+% \end{frame}
+
+% \begin{frame}[fragile]
+% \frametitle{Java Method Call}
+% $
+% \begin{array}[b]{c}
+% \begin{array}[b]{c}
+% \texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}}
+% \\
+% \hline
+% \texttt{emptyList().get()} : \exptype{List}{\type{String}}
+% \end{array} \rulenameAfter{T-Call}
+% \\
+% \hline
+% \texttt{emptyList().get().get()} : \type{String}
+% \end{array} \rulenameAfter{T-Call}
+% $
+% \end{frame}
+
+% \begin{frame}[fragile]
+% \frametitle{Method Call with Wildcards}
+% Eigentlich kann man mit Wildcard Typen keine Methodenaufrufe durchführen.
+% Der eigentliche Typ ist nicht bekannt.
+% ? sind auch nicht reflexiv
+% Es geht dennoch, weil sich hinter einem Wildcard Typ ein konkreter Typ verbirgt.
+% Dieser muss ausgepackt werden.
+% Die entstehende freie Typvariable kann nun als Typ benutzt werden.
+
+% \end{frame}
+
+
+\begin{frame}[fragile]
+    \frametitle{Typeinference ohne Wildcards}
+    \rulename{TI-Call} \\[1em]
+    \begin{center}
+    $\begin{array}{l}
+        \begin{array}{@{}c}
+            \textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad
+            \Delta \vdash  \expr{v}, \ol{v} : [\ol{T'}/\ol{X}]\ol{T}
+            \\
+            \hline
+        \vspace*{-0.3cm}\\
+            \Delta \vdash \expr{v}.\texttt{m}(\ol{v}) : [\ol{T'}/\ol{X}]\type{T}
+        \end{array}
+    \end{array}$
+    \end{center}
 \begin{verbatim}
-head(head(emptyList()))
+untypedMethod(l){
+    shuffle(l);
+}
 \end{verbatim}
-
-$
-\begin{array}[b]{c}
-\texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}} \\
-\quad \textit{mtype}(\texttt{get}) = \generics{X}\ \exptype{List}{\type{X}} \to \type{X}
-\\
-\hline
-\texttt{head(emptyList())} : \exptype{List}{\type{String}}
-\end{array} \rulenameAfter{T-Call}
-$
+\begin{itemize}
+    \item $\lessdot $
+\end{itemize}
 \end{frame}
 
-\begin{frame}[fragile]
-\frametitle{Java Method Call}
-$
-\begin{array}[b]{c}
-\texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}} \\
-\quad \textit{mtype}(\texttt{get}) = \generics{X}\ \exptype{List}{\type{X}} \to \type{X}
-\\
-\hline
-\generics{\exptype{List}{\exptype{List}{\type{String}}}}\texttt{head(emptyList())} : \exptype{List}{\type{String}}
-\end{array} \rulenameAfter{T-Call}
-$
-
-$
-\begin{array}[b]{c}
-\texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}} \\
-\quad \textit{mtype}(\texttt{get}) = \generics{X}\ \exptype{List}{\type{X}} \to \type{X}
-\\
-\hline
-\generics{\exptype{List}{\type{String}}}\texttt{head(emptyList())} : \exptype{List}{\type{String}}
-\end{array} \rulenameAfter{T-Call}
-$
-\end{frame}
-
-\begin{frame}[fragile]
-\frametitle{Java Method Call}
-
-$
-\begin{array}[b]{c}
-\texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}} \\
-\quad \textit{mtype}(\texttt{get}) = \generics{X}\ \exptype{List}{\type{X}} \to \type{X}
-\\
-\hline
-\generics{\exptype{List}{\type{String}}}\texttt{head(emptyList())} : \exptype{List}{\type{String}}
-\end{array} \rulenameAfter{T-Call}
-$
-\end{frame}
-
-\begin{frame}[fragile]
-\frametitle{Java Method Call}
-$
-\begin{array}[b]{c}
-\begin{array}[b]{c}
-\texttt{emptyList()} : \exptype{List}{\exptype{List}{\type{String}}}
-\\
-\hline
-\texttt{emptyList().get()} : \exptype{List}{\type{String}}
-\end{array} \rulenameAfter{T-Call}
-\\
-\hline
-\texttt{emptyList().get().get()} : \type{String}
-\end{array} \rulenameAfter{T-Call}
-$
-\end{frame}
-
-\begin{frame}[fragile]
-\frametitle{Method Call with Wildcards}
-Eigentlich kann man mit Wildcard Typen keine Methodenaufrufe durchführen.
-Der eigentliche Typ ist nicht bekannt.
-? sind auch nicht reflexiv
-Es geht dennoch, weil sich hinter einem Wildcard Typ ein konkreter Typ verbirgt.
-Dieser muss ausgepackt werden.
-Die entstehende freie Typvariable kann nun als Typ benutzt werden.
-
-\end{frame}
-
-
-
 \begin{frame}[fragile]{Capture Conversion}
 \rulename{T-Call-Wildcards} \\[1em]
 \begin{center}
@@ -343,4 +377,52 @@ shuffle2D(l); // Fehler!
 %why do we need capture constraints?
 % List<List<?>> not a subtype of List<List<X>> for any X
 
+
+
+%TODO Unify erklären
+% - es gibt die Capture Regel, welche Capture Conversion durchführt
+% - die subst-Regel, welche keine Typen mit freien Variablen in normale Typvariablen einsetzt
+\begin{frame}[fragile]{Unify}
+$\begin{array}{c}
+\tv{a} \lessdot \tv{b},
+\tv{c} \lessdot \exptype{List}{\type{X}},
+
+\end{array}$
+\end{frame}
+
+% wieso dürfen normale Typvariablen keine freien Variablen enthalten?
+% sonst könnte man der shuffle2D Method ein 
+\begin{frame}[fragile]
+\begin{verbatim}
+    <A> List<A> shuffle(List<A> l){...}
+    <A,B> List<B> map(List<A> l, Function<A,B> f) { ... }
+    List<List<?>> l;
+    l.map((List<?> x) -> shuffle(x));
+\end{verbatim}
+$
+\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\tv{x}},
+\exptype{List}{\tv{x}} \lessdot \tv{r}
+$
+\end{frame}
+
+\begin{frame}[fragile]
+\begin{verbatim}
+    List<List<?>> l;
+    l2 = l.map(x -> shuffle(x));
+    shuffle2D(l2);
+\end{verbatim}
+
+$
+\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\tv{x}},
+\exptype{List}{\exptype{List}{\tv{x}}} \lessdot \tv{r},
+\tv{r} \lessdot \tv{l2},
+\tv{l2} \lessdotCC \exptype{List}{\exptype{List}{\tv{y}}}
+$
+\end{frame}
+
+% könnte es nicht well-formed typen geben, wenn man beliebige substitutionen zulässt?
+% (brauchen wir die wildcard-TVs überhaupt? es wird eigentlich nur für den Soundness-Beweis gebraucht)
+
+
+
 \end{document}