Wildcard Elimination and Concat example with backtracking
This commit is contained in:
JanUlrich
parent
e92d008a6c
commit
f371d8ee61
250
vortrag.tex
250
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}
|
||||
<X> List<X> concat(List<X> l1, List<X> 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<? extends Object> 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}
|
||||
<X> List<X> concat(List<X> l1, List<X> l2){ ... }
|
||||
(*@\color{red}\texttt{List<Object>}@*) 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}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user