Final Version
This commit is contained in:
JanUlrich
parent
b31d31a063
commit
e71d69f13e
271
vortrag.tex
271
vortrag.tex
@ -61,8 +61,8 @@
|
||||
xrightmargin=0pt, % Rand rechts
|
||||
%frame=single, % Rahmen an
|
||||
%frameround=ffff,
|
||||
rulecolor=\color{darkgray}, % Rahmenfarbe
|
||||
fillcolor=\color{ListingBackground},
|
||||
rulecolor=\color{black}, % Rahmenfarbe
|
||||
fillcolor=\color{black},
|
||||
showtabs=false,
|
||||
%breaklines=true,
|
||||
%breakatwhitespace=true,
|
||||
@ -230,9 +230,9 @@
|
||||
\begin{lstlisting}
|
||||
(*@\only<2>{\color{red}$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$ }@*)someList(){
|
||||
if(Math.random > 0.5){
|
||||
return new List("String");
|
||||
return new List<>("String");
|
||||
} else {
|
||||
return new List(42);
|
||||
return new List<>(42);
|
||||
}
|
||||
}
|
||||
\end{lstlisting}
|
||||
@ -324,134 +324,42 @@ concat(l1, l2); //Error
|
||||
$\begin{array}{l}
|
||||
\begin{array}{@{}c}
|
||||
\textit{mtype}(\texttt{concat}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \\
|
||||
\texttt{l1} : \wctype{\rwildcard{A}}{List}{\rwildcard{A}}, \texttt{l2} : \wctype{\rwildcard{A}}{List}{\rwildcard{A}} \\
|
||||
\texttt{l1} : \wctype{\rwildcard{A}}{List}{\rwildcard{A}}, \texttt{l2} : \wctype{\rwildcard{B}}{List}{\rwildcard{B}} \\
|
||||
\exptype{List}{\rwildcard{A}} \nless: [{\color{red}?}/\type{X}]\exptype{List}{\type{X}} \quad \quad
|
||||
\exptype{List}{\rwildcard{B}} \nless: [{\color{red}?}/\type{X}]\exptype{List}{\type{X}}
|
||||
\\
|
||||
\hline
|
||||
\vspace*{-0.3cm}\\
|
||||
\texttt{shuffle}(\expr{l}) : {\color{red}\textbf{Errror}}
|
||||
\texttt{concat}(\expr{l1}, \expr{l2}) : {\color{red}\textbf{Errror}}
|
||||
\end{array}
|
||||
\end{array}$
|
||||
\end{center}
|
||||
\end{frame}
|
||||
|
||||
% - 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]{Reduce}
|
||||
% \rulename{Reduce} $
|
||||
% \begin{array}[c]{@{}ll}
|
||||
% \begin{array}[c]{l}
|
||||
% \wildcardEnv \vdash
|
||||
% C \cup \, \set{ \exptype{C}{\ol{S}} \lessdot
|
||||
% \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}},
|
||||
% \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}
|
||||
% \ol{\wtv{a}} \ \text{fresh}\\
|
||||
% %\text{fv}(\exptype{C}{\ol{S}}) \subseteq \text{dom}(\overline{\wildcard{B}{\type{U'}}{\type{L'}}})
|
||||
% %\text{dom}(\overline{\wildcard{A}{\type{U}}{\type{L}}}) \subseteq \text{fv}(\exptype{C}{\ol{T}}) \\
|
||||
% %\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{\wildcard{A}{\type{Object}}{\bot}}{List}{\type{A}}\\
|
||||
% \hline
|
||||
% \type{String} \doteq \wtv{a}, \wtv{a} \lessdot \type{Object}, \bot \lessdot \wtv{a}
|
||||
% \end{array}$
|
||||
% \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{\wildcard{A}{\type{U}}{\type{L}}}{List}{\type{A}} \lessdot \exptype{List}{\wtv{x}}\\
|
||||
% \hline
|
||||
% \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");
|
||||
return new List<(*@\only<2>{$\color{red}\tv{x}$}@*)>("String");
|
||||
} else {
|
||||
return new List(42);
|
||||
return new List<(*@\only<2>{$\color{red}\tv{y}$}@*)>(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}
|
||||
\exptype{List}{\tv{x}} \lessdot {\only<2>{\color{red}}\tv{r}}, \type{String} \lessdot {\only<2>{\color{red}}\tv{x}},
|
||||
\exptype{List}{\tv{y}} \lessdot {\only<2>{\color{red}}\tv{r}}, \type{Integer} \lessdot {\only<2>{\color{red}}\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(){
|
||||
if(Math.random > 0.5){
|
||||
return new List("String");
|
||||
return new List<>("String");
|
||||
} else {
|
||||
return new List(42);
|
||||
return new List<>(42);
|
||||
}
|
||||
}
|
||||
\end{lstlisting}
|
||||
@ -526,58 +434,42 @@ $
|
||||
\exptype{List}{Integer} \lessdot {\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}}
|
||||
\\
|
||||
\hline
|
||||
\type{String} \doteq \wtv{x1}, \wtv{x1} \lessdot \tv{u}, \tv{l} \lessdot \wtv{x1}, \\
|
||||
\type{String} \doteq \wtv{x1}, \wtv{x1} \lessdot \tv{u}, \tv{l} \lessdot \wtv{x1}, \hfill
|
||||
\type{Integer} \doteq \wtv{x2}, \wtv{x2} \lessdot \tv{u}, \tv{l} \lessdot \wtv{x2}
|
||||
\pause \\
|
||||
\hline
|
||||
\type{String} \lessdot \tv{u}, \tv{l} \lessdot \type{String},\\
|
||||
\type{String} \lessdot \tv{u}, \tv{l} \lessdot \type{String},\hfill
|
||||
\type{Integer} \lessdot \tv{u}, \tv{l} \lessdot \type{Integer}
|
||||
\end{array}$
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}[fragile]
|
||||
%Es gibt stellen wo capture conversion möglich ist und Stellen wo es nicht ist.
|
||||
\frametitle{Wildcards are bound to Type}
|
||||
\begin{lstlisting}
|
||||
<X> List<List<X>> shuffle2D(List<List<X>> l) {...}
|
||||
|
||||
List<List<?>> l = ...;
|
||||
shuffle2D(l); // Fehler!
|
||||
\end{lstlisting}
|
||||
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}[fragile]
|
||||
%Es gibt stellen wo capture conversion möglich ist und Stellen wo es nicht ist.
|
||||
\frametitle{Wildcards are bound to Type}
|
||||
\begin{lstlisting}
|
||||
<X> List<List<X>> shuffle2D(List<List<X>> l) {...}
|
||||
|
||||
(*@$\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$@*) l = ...;
|
||||
shuffle2D(l); // Fehler!
|
||||
\end{lstlisting}
|
||||
\pause
|
||||
\vfill
|
||||
\begin{lstlisting}
|
||||
<X> List<List<X>> shuffle2D(List<List<X>> l) {...}
|
||||
|
||||
(*@$\color{red}\wctype{\rwildcard{A}}{List}{\exptype{List}{\rwildcard{A}}}$@*) l = ...;
|
||||
shuffle2D(l); // (*@\color{red}\textbf{Correct!}@*)
|
||||
\end{lstlisting}
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}[fragile]{Wildcard Elminiation}
|
||||
\begin{frame}[fragile]{Wildcard Eliminiation}
|
||||
\begin{lstlisting}
|
||||
<X> List<X> concat(List<X> l1, List<X> l2){ ... }
|
||||
|
||||
List<? extends Object> someList(){
|
||||
if(Math.random > 0.5){
|
||||
return new List<>("String");
|
||||
} else {
|
||||
return new List<>(42);
|
||||
}
|
||||
}
|
||||
\end{lstlisting}
|
||||
|
||||
\end{frame}
|
||||
\begin{frame}[fragile]{Wildcard Eliminiation}
|
||||
\begin{lstlisting}
|
||||
<X> List<X> concat(List<X> l1, List<X> l2){ ... }
|
||||
|
||||
someList(){
|
||||
if(Math.random > 0.5){
|
||||
return new List("String");
|
||||
return new List<>("String");
|
||||
} else {
|
||||
return new List(42);
|
||||
return new List<>(42);
|
||||
}
|
||||
}
|
||||
|
||||
concat(someList(), someList())
|
||||
(*@\color{red}\texttt{concat(someList(), someList())}@*)
|
||||
\end{lstlisting}
|
||||
|
||||
\only<1>{\textbf{Input}:}
|
||||
@ -589,8 +481,8 @@ $
|
||||
\begin{array}{l}
|
||||
\exptype{List}{String} \lessdot {\tv{r}},
|
||||
\exptype{List}{Integer} \lessdot {\tv{r}},
|
||||
\tv{r} \lessdotCC \exptype{List}{\wtv{x}},
|
||||
\tv{r} \lessdotCC \exptype{List}{\wtv{x}}
|
||||
\highlight{\tv{r} \lessdotCC \exptype{List}{\wtv{x}},
|
||||
\tv{r} \lessdotCC \exptype{List}{\wtv{x}}}
|
||||
\pause
|
||||
\\
|
||||
\hline
|
||||
@ -613,54 +505,6 @@ $
|
||||
|
||||
\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]{Capture Conversion during Unify}
|
||||
\rulename{Capture} $
|
||||
\begin{array}[c]{@{}ll}
|
||||
@ -698,7 +542,7 @@ $\begin{array}{l}
|
||||
\\
|
||||
\hline
|
||||
\wildcard{X}{\tv{u}}{\tv{l}}, \highlight{\wildcard{Y}{\tv{u}}{\tv{l}}} \vdash \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{x}},
|
||||
{\exptype{List}{\highlight{\rwildcard{Y}}}} \lessdotCC \exptype{List}{\wtv{x}}
|
||||
{\exptype{List}{\highlight{\rwildcard{Y}}}} \lessdot \exptype{List}{\wtv{x}}
|
||||
\end{array}$
|
||||
\end{frame}
|
||||
|
||||
@ -706,23 +550,7 @@ $\begin{array}{l}
|
||||
\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
|
||||
\\
|
||||
\ldots \\
|
||||
\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}},
|
||||
@ -740,18 +568,12 @@ $
|
||||
\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{itemize}
|
||||
\item Remove Wildcard by setting lower bound = upper bound
|
||||
\end{itemize}
|
||||
|
||||
$\begin{array}{l}
|
||||
\ldots \\
|
||||
\hline
|
||||
\tv{l} \lessdot \type{String}, \tv{l} \lessdot \type{Integer}, \highlight{\tv{l} \doteq \type{Object}}
|
||||
\implies \textbf{Error!}
|
||||
@ -761,11 +583,12 @@ $\begin{array}{l}
|
||||
\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");
|
||||
return new List<>("String");
|
||||
} else {
|
||||
return new List(42);
|
||||
return new List<>(42);
|
||||
}
|
||||
}
|
||||
|
||||
@ -790,6 +613,7 @@ $\exptype{List}{\tv{x}} \lessdot {\tv{r}}, \highlight{\type{Object}} \lessdot \t
|
||||
\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(*@\color{red}\texttt{<Object>}@*)("String");
|
||||
@ -828,7 +652,8 @@ concat(someList(), someList())
|
||||
$
|
||||
\begin{array}{l}
|
||||
\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}}, \\
|
||||
\exptype{List}{\exptype{List}{\wtv{x}}} \lessdot \tv{l2}, \\
|
||||
\exptype{List}{\wtv{x}} \lessdot \tv{z}, \\
|
||||
\exptype{List}{\tv{z}} \lessdot \tv{l2}, \\
|
||||
\tv{l2} \lessdotCC \exptype{List}{\exptype{List}{\wtv{y}}}
|
||||
\end{array}
|
||||
$
|
||||
|
||||
Loading…
Reference in New Issue
Block a user