Cleanup. Add Unify example why free variables are not allowed to leave scope
This commit is contained in:
Andreas Stadelmeier
parent
2df4b69982
commit
2e0909dcea
334
vortrag.tex
334
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}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user