From f371d8ee6112cd33aa22b4aa69c77f9836898f3e Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Sun, 28 Apr 2024 15:33:01 +0200 Subject: [PATCH] Wildcard Elimination and Concat example with backtracking --- vortrag.tex | 250 +++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 239 insertions(+), 11 deletions(-) diff --git a/vortrag.tex b/vortrag.tex index 35a9a70..2ecb981 100644 --- a/vortrag.tex +++ b/vortrag.tex @@ -589,12 +589,13 @@ shuffle2D(l); // Fehler! \begin{array}[c]{l} \wildcardEnv \vdash C \cup \, \set{ \exptype{C}{\ol{S}} \lessdot - \wctype{\overline{\rwildcard{A}}}{C}{\ol{T}} } \\ + \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} } \\ \hline \vspace*{-0.4cm}\\ \wildcardEnv \vdash C \cup \, \set{ - \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}} } + \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}}, +\overline{\wtv{a} \lessdot \type{U}}, \overline{\type{L} \lessdot \wtv{a}}} \end{array} %\quad \ol{Y} = \textit{fresh}(\ol{X}) \quad \begin{array}[c]{l} @@ -604,23 +605,91 @@ shuffle2D(l); // Fehler! %\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset \end{array} \end{array} - $ + $\\[1em] \begin{itemize} \item \textbf{Example:} $\begin{array}[t]{c} - \exptype{List}{\type{String}} \lessdot \wctype{\rwildcard{A}}{List}{\type{A}}\\ + \exptype{List}{\type{String}} \lessdot \wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\type{A}}\\ \hline - \type{String} \doteq \wtv{a} + \type{String} \doteq \wtv{a}, \wtv{a} \lessdot \type{Object}, \bot \lessdot \wtv{a} \end{array}$ - \item \textbf{Example:} +\end{itemize}\\ \vfill +\pause +\rulename{Capture} $ + \begin{array}[c]{@{}ll} + \begin{array}[c]{l} + \wildcardEnv \vdash + C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}} \lessdotCC \type{T} } \\ + \hline + \vspace*{-0.4cm}\\ + \wildcardEnv \cup \overline{\wildcard{C}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{U}}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{L}}} + \vdash C \cup \, \set{ + [\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} \lessdot \type{T} } + \end{array} + %\quad \ol{Y} = \textit{fresh}(\ol{X}) + \quad \begin{array}[c]{l} + \ol{\rwildcard{C}} \ \text{fresh}\\ + %\text{fv}(\type{T}) \neq \emptyset + \end{array} + \end{array} + $\\[1em] +\begin{itemize} +\item \textbf{Example:} $\begin{array}[t]{c} - \wctype{\rwildcard{A}}{List}{\type{A}} \lessdot \exptype{List}{\type{String}}\\ + \wctype{\wildcard{A}{\type{U}}{\type{L}}}{List}{\type{A}} \lessdot \exptype{List}{\wtv{x}}\\ \hline - \type{A} \doteq \type{String} + \wildcard{A}{\type{U}}{\type{L}} \vdash \exptype{List}{\type{A}} \lessdot \exptype{List}{\wtv{x}} +\\ + \hline + \wildcard{A}{\type{U}}{\type{L}} \vdash \type{A} \doteq \wtv{x} \end{array}$ \end{itemize} \end{frame} +\begin{frame}[fragile]{Wildcard Creation} + \begin{lstlisting} +(*@\only<2>{$\color{red}\tv{r}$ }@*)someList(){ + if(Math.random > 0.5){ + return new List("String"); + } else { + return new List(42); + } +} + \end{lstlisting} + \pause +$ +\exptype{List}{\tv{x}} \lessdot {\only<2>{\color{red}}\tv{r}}, \type{String} \lessdot \tv{x}, +\exptype{List}{\tv{y}} \lessdot {\only<2>{\color{red}}\tv{r}}, \type{Integer} \lessdot \tv{y} +$\\[1em] +\pause +\rulename{General} $ + \begin{array}[c]{l} + \wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \ntv{a}\\ + \hline + \wildcardEnv \vdash C \cup \set{\wctype{\Delta}{C}{\ol{T}} \lessdot \ntv{a}, + \ntv{a} \doteq \wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}} + } + \end{array} \quad \begin{array}[c]{l} + \texttt{class} \ \exptype{C}{\ol{X}} \set{\ldots }\\%\triangleleft \exptype{D}{\ol{N}} \\ + \tv{u}, \tv{l}\ \text{fresh} + \end{array} + $ +\\[1em] +\pause +$ +\exptype{List}{\tv{x}} \lessdot {\tv{r}}, \highlight{\tv{x} \doteq \type{String}}, +\exptype{List}{\tv{y}} \lessdot {\tv{r}}, \highlight{\tv{y} \doteq \type{Integer}} +$ +\pause +\\[0.5em] +\textbf{Substitution:} + +$ +\exptype{List}{\highlight{\type{String}}} \lessdot \tv{r}, +\exptype{List}{\highlight{\type{Integer}}} \lessdot \tv{r} +$ +\end{frame} + \begin{frame}[fragile]{Wildcard Creation} \begin{lstlisting} (*@\only<2>{$\color{red}\tv{r}$ }@*)someList(){ @@ -696,6 +765,7 @@ concat(someList(), someList()) \only<1>{\textbf{Input}:} $\only<2>{\highlight{\rulename{General}}}$ $\only<3>{\highlight{\rulename{Reduce}}}$ +$\only<4>{\highlight{\rulename{Subtitute}}}$ $ \begin{array}{l} @@ -713,14 +783,167 @@ $ \pause \\ \hline -\highlight{\type{String} \doteq \wtv{x1}, \wtv{x1} \lessdot \tv{u}, \tv{l} \lessdot \wtv{x1}, -\type{Integer} \doteq \wtv{x2}, \wtv{x2} \lessdot \tv{u}, \tv{l} \lessdot \wtv{x2}}, \\ +\only<3>{\highlight{\type{String} \doteq \wtv{x1}, \wtv{x1} \lessdot \tv{u}, \tv{l} \lessdot \wtv{x1}, +\type{Integer} \doteq \wtv{x2}, \wtv{x2} \lessdot \tv{u}, \tv{l} \lessdot \wtv{x2}}, \\} +\only<4>{\highlight{\type{String} \lessdot \tv{u}, \tv{l} \lessdot \type{String}, +\type{Integer} \lessdot \tv{u}, \tv{l} \lessdot \type{Integer}}, \\} \only<2>{\highlight}{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}}, \only<2>{\highlight}{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}} +\pause + \end{array}$ \end{frame} + +\begin{frame}[fragile]{Wildcard Elminiation} + +\textit{Continue ...}\\ +$ +\begin{array}{l} +\type{String} \lessdot \tv{u}, \tv{l} \lessdot \type{String}, +\type{Integer} \lessdot \tv{u}, \tv{l} \lessdot \type{Integer}, \\ +\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}, +\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}} +\end{array}$\\[1em] +\pause +\rulename{Super} \\ +$ +\begin{array}[c]{l} +\wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \tv{a}\\ +\hline +\wildcardEnv \vdash C \cup \set{ \wctype{\Delta'}{D}{[\ol{T}/\ol{X}]\ol{N}} \lessdot \tv{a} } +%\set{\wctype{\ol{\wtype{W}}}{D}{[\ol{X}/\ol{Y}]\ol{Z}} \lessdot \tv{a}} +\end{array} \quad +\begin{array}{l} +\texttt{class} \ \exptype{C}{\ol{X}} \ \texttt{extends} \ \exptype{D}{\ol{N}} \\ +\end{array} +$\\[1em] + +\textit{Subtyping:} +\begin{lstlisting} +class String extends Object {...} +class Integer extends Object {...} +\end{lstlisting} +\pause +$ +\begin{array}{l} +\type{String} \lessdot \tv{u}, \tv{l} \lessdot \type{String}, +\type{Integer} \lessdot \tv{u}, \tv{l} \lessdot \type{Integer}, \\ +\hline +\highlight{ +\type{Object}} \lessdot \tv{u}, \tv{l} \lessdot \type{String}, +\highlight{\type{Object}} \lessdot \tv{u}, \tv{l} \lessdot \type{Integer} +\\ +\hline +\tv{u} \doteq \type{Object}, \ldots \\ +\pause +{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}}, +{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}} +\end{array} +$ +\end{frame} + +\begin{frame}[fragile]{Wildcard Elimination} +\textit{Continue ...}\\ +$ +\begin{array}{l} +\tv{u} \doteq \type{Object}, \tv{l} \lessdot \type{String}, \tv{l} \lessdot \type{Integer}, \\ +\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}, +\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}} +\pause +\\ +\hline +\tv{l} \lessdot \type{String}, \tv{l} \lessdot \type{Integer}, \\ +\wctype{\wildcard{X}{\type{Object}}{\tv{l}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}, +\wctype{\wildcard{X}{\type{Object}}{\tv{l}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}} +\pause +\\ +\hline +\wildcard{X}{\tv{u}}{\tv{l}} \vdash \tv{l} \lessdot \type{String}, \tv{l} \lessdot \type{Integer}, \\ +\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{x}}, +\wctype{\wildcard{X}{\type{Object}}{\tv{l}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}} +\pause +\\ +\hline +\wildcard{X}{\type{Object}}{\tv{l}}, \wildcard{Y}{\type{Object}}{\tv{l}}, \vdash \tv{l} \lessdot \type{String}, \tv{l} \lessdot \type{Integer}, \\ +\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{x}}, +\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{x}} +\pause +\\ +\hline +\wildcard{X}{\type{Object}}{\tv{l}}, \wildcard{Y}{\type{Object}}{\tv{l}}, \vdash \tv{l} \lessdot \type{String}, \tv{l} \lessdot \type{Integer}, \\ +\rwildcard{X} \doteq \wtv{x}, +\rwildcard{Y} \doteq \wtv{x} +\pause +\\ +\hline +\wildcard{X}{\type{Object}}{\tv{l}}, \wildcard{Y}{\type{Object}}{\tv{l}}, \vdash \tv{l} \lessdot \type{String}, \tv{l} \lessdot \type{Integer}, \\ +\rwildcard{X} \doteq \rwildcard{Y} +\end{array}$\\[0.5em] +\pause +\only<7>{ +\rulename{Normalize} +$\begin{array}[c]{l} +\wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}} \vdash C \cup \set{\rwildcard{A} \doteq \type{T}}\\ + \hline +[\type{U}/\type{A}]\wildcardEnv \vdash [\type{U}/\type{A}] +C \cup [\type{U}/\type{A}]\set{\ntv{a} \doteq \type{T}, \type{L} \doteq \type{U}} +\end{array} +$ +} +\pause +$\begin{array}{l} +\hline +\tv{l} \lessdot \type{String}, \tv{l} \lessdot \type{Integer}, \highlight{\tv{l} \doteq \type{Object}} +\implies \textbf{Error!} +\end{array}$ +\end{frame} + +\begin{frame}[fragile]{Backtracking} +\begin{lstlisting} + List concat(List l1, List l2){ ... } +someList(){ + if(Math.random > 0.5){ + return new List("String"); + } else { + return new List(42); + } +} + +concat(someList(), someList()) +\end{lstlisting} +\begin{itemize} +\item \texttt{List someList()} is not the correct type annotation in this case +\pause +\item Backtracking to: +$\exptype{List}{\tv{x}} \lessdot {\tv{r}}, \type{String} \lessdot \tv{x}, +\exptype{List}{\tv{y}} \lessdot {\tv{r}}, \type{Integer} \lessdot \tv{y}, +\tv{r} \lessdotCC \exptype{List}{\wtv{x}}, +\tv{r} \lessdotCC \exptype{List}{\wtv{x}}$ +\pause +\item Using the \rulename{Super} rule:\\ +$\exptype{List}{\tv{x}} \lessdot {\tv{r}}, \highlight{\type{Object}} \lessdot \tv{x}, +\exptype{List}{\tv{y}} \lessdot {\tv{r}}, \highlight{\type{Object}} \lessdot \tv{y}, +\ldots $ +\end{itemize} +\end{frame} + +\begin{frame}[fragile]{Correct Solution} +\begin{lstlisting} + List concat(List l1, List l2){ ... } +(*@\color{red}\texttt{List}@*) someList(){ + if(Math.random > 0.5){ + return new List("String"); + } else { + return new List(42); + } +} + +concat(someList(), someList()) +\end{lstlisting} +\end{frame} + % wieso dürfen normale Typvariablen keine freien Variablen enthalten? % sonst könnte man der shuffle2D Method ein \begin{frame}[fragile] @@ -805,6 +1028,11 @@ $ % 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) - +\begin{frame}[fragile]{Conclusion} +\begin{itemize} +\item Eliminate Wildcards by setting upper = lower bound +\item Removes Wildcards without backtracking +\end{itemize} +\end{frame} \end{document}