347 lines
9.8 KiB
TeX
347 lines
9.8 KiB
TeX
\documentclass{beamer}
|
|
\input{prolog}
|
|
%Information to be included in the title page:
|
|
\title{Typinferenz für Java mit Wildcards}
|
|
\author{Andreas Stadelmeier}
|
|
\institute{DHBW Stuttgart Campus Horb}
|
|
\date{2024}
|
|
|
|
\begin{document}
|
|
|
|
\frame{\titlepage}
|
|
|
|
\newcommand{\rulenameAfter}[1]{\begin{array}[b]{l}\rulename{#1}\\[-0.5em] \ \end{array}}
|
|
|
|
\begin{frame}[fragile]
|
|
\frametitle{Java Method Call}
|
|
\rulename{T-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 \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}
|
|
\end{array}
|
|
\end{array}$
|
|
\end{center}
|
|
|
|
\textbf{Example:}
|
|
$\generics{\type{String}}\texttt{emptyList}() : \exptype{List}{\type{String}}$
|
|
\\[2em]
|
|
\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}
|
|
|
|
\textbf{Example:}
|
|
$\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}
|
|
|
|
\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{frame}[fragile]
|
|
\frametitle{Java Method Call}
|
|
\rulename{T-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}.\generics{\ol{T'}}\texttt{m}(\ol{v}) : [\ol{T'}/\ol{X}]\type{T}
|
|
\end{array}
|
|
\end{array}$
|
|
\end{center}
|
|
\textbf{Beispiel:}\\
|
|
$\begin{array}{l}
|
|
\begin{array}{@{}c}
|
|
\textit{mtype}(\texttt{m}) = \generics{\ol{X}}\ \ol{T} \to \type{T} \quad \quad
|
|
\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}$
|
|
\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}$
|
|
\end{frame}
|
|
|
|
\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]{Capture Conversion}
|
|
\rulename{T-Call-Wildcards} \\[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 \ol{v} : \ol{\wctype{\Delta}{C}{\ol{T}}} \\
|
|
\overline{\exptype{C}{\ol{T}}} <: [\ol{T'}/\ol{X}]\ol{T} \quad \quad [\ol{T'}/\ol{X}]\type{T} <: \type{R}
|
|
\\
|
|
\hline
|
|
\vspace*{-0.3cm}\\
|
|
\Delta \vdash \texttt{m}(\ol{v}) : \type{R}
|
|
\end{array}
|
|
\end{array}$
|
|
\end{center}
|
|
%Wildcard Capture
|
|
\begin{verbatim}
|
|
<X> List<X> shuffle(List<X> l){ ... }
|
|
|
|
List<?> l;
|
|
|
|
shuffle(l) : List<?>
|
|
\end{verbatim}
|
|
%why do we need capture constraints?
|
|
% List<List<?>> not a subtype of List<List<X>> for any X
|
|
|
|
\begin{center}
|
|
$\begin{array}{l}
|
|
\begin{array}{@{}c}
|
|
\textit{mtype}(\texttt{shuffle}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \\
|
|
\texttt{l} : \wctype{\rwildcard{A}}{List}{\rwildcard{A}} \quad \quad
|
|
\exptype{List}{\type{A}} <: [\type{A}/\type{X}]\exptype{List}{\type{X}} \\
|
|
\ [\type{A}/\type{X}]\exptype{List}{\type{X}} <: \wctype{\rwildcard{A}}{List}{\rwildcard{A}}
|
|
\\
|
|
\hline
|
|
\vspace*{-0.3cm}\\
|
|
\texttt{shuffle}(\expr{l}) : \wctype{\rwildcard{A}}{List}{\rwildcard{A}}
|
|
\end{array}
|
|
\end{array}$
|
|
\end{center}
|
|
\end{frame}
|
|
|
|
\begin{frame}[fragile,t]
|
|
%Explain why ? cannot be used as a regular type
|
|
\begin{verbatim}
|
|
<X> List<X> concat(List<X> l1, List<X> l2){
|
|
return l1.addAll(l2);
|
|
}
|
|
|
|
List<?> l1;
|
|
List<?> l2;
|
|
|
|
concat(l1, l2); //Error
|
|
\end{verbatim}
|
|
\end{frame}
|
|
|
|
\begin{frame}[fragile,t]
|
|
\begin{verbatim}
|
|
<X> List<X> concat(List<X> l1, List<X> l2){
|
|
return l1.addAll(l2);
|
|
}
|
|
|
|
List<String> ls = new List<String>();
|
|
|
|
List<?> l1 = ls; //korrekt!
|
|
List<?> l2 = new List<Integer>(1);
|
|
|
|
concat(l1, l2); //Error (würde l2 an ls anfügen!)
|
|
// ls.getLast() -> 1 (ein Int obwohl ls : List<String>)
|
|
\end{verbatim}
|
|
\end{frame}
|
|
|
|
\begin{frame}[fragile]
|
|
%Wildcard Capture
|
|
\begin{verbatim}
|
|
<X> void shuffle2D(List<List<X>> l){
|
|
//randomly exchange every element
|
|
// in the two dimensional list l
|
|
}
|
|
|
|
List<List<?>> l;
|
|
|
|
shuffle2D(l); // Error
|
|
\end{verbatim}
|
|
|
|
$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \nless: \exptype{List}{\rwildcard{A}}$
|
|
\end{frame}
|
|
|
|
\begin{frame}[fragile]
|
|
%Es gibt stellen wo capture conversion möglich ist und Stellen wo es nicht ist.
|
|
\frametitle{Capture Constraint}
|
|
\begin{verbatim}
|
|
<X> List<List<X>> shuffle2D(List<? extends List<X>> l) {...}
|
|
|
|
List<List<?>> l = ...;
|
|
shuffle2D(l); // Fehler!
|
|
\end{verbatim}
|
|
\begin{itemize}
|
|
\item hier ergibt sich ein Subtype-Constraint der keine Capture Conversion zulässt:
|
|
\item $\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\tv{x}}$
|
|
\pause
|
|
\item $\unify{}(\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\tv{a}}) = \emptyset$
|
|
\end{itemize}
|
|
|
|
\end{frame}
|
|
|
|
\begin{frame}[fragile]
|
|
%Es gibt stellen wo capture conversion möglich ist und Stellen wo es nicht ist.
|
|
\frametitle{Capture Constraint}
|
|
\begin{verbatim}
|
|
<X> List<List<X>> shuffle2D(List<? extends List<X>> l) {...}
|
|
|
|
List<List<?>> l = ...;
|
|
shuffle2D(l); // Fehler!
|
|
\end{verbatim}
|
|
\begin{itemize}
|
|
\item hier ergibt sich ein Subtype-Constraint der keine Capture Conversion zulässt:
|
|
\item $\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\tv{x}}$
|
|
\pause
|
|
\item $\unify{}(\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\tv{a}}) = \emptyset$
|
|
\end{itemize}
|
|
|
|
\end{frame}
|
|
|
|
\begin{frame}[fragile]
|
|
\frametitle{Capture Constraint}
|
|
$\unify{}(\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\tv{a}}) = \emptyset$
|
|
$\unify{}(\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\tv{a}}) = \set{\tv{a} \to \rwildcard{A}}$
|
|
\end{frame}
|
|
|
|
% TODO:
|
|
% Folie zu aktueller Stand Unify: Es gibt <. Constraints. Unify löst diese
|
|
% Folie zu <? constraints: sie werden benötigt, weil unify während der Lösungsfindung Capture Conversion durchführen muss
|
|
%why do we need capture constraints?
|
|
% List<List<?>> not a subtype of List<List<X>> for any X
|
|
|
|
\end{document}
|