VortragBadHonnef24/vortrag.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]
%Wildcard Capture
\begin{verbatim}
List<List<?>> l;

head(l) : List<?>
\end{verbatim}
%why do we need capture constraints?
% List<List<?>> not a subtype of List<List<X>> for any X

$\wctype{\rwildcard{A}}{List}{\rwildcard{A}}$
\end{frame}

\begin{frame}[fragile]
%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}

\begin{verbatim}
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 shuffle(List<List<X>> l){ 
    //randomly exchange every element
    // in the two dimensional list l
}

List<List<?>> l;

shuffle(l); // Error
\end{verbatim}

$\wctype{\rwildcard{A}}{List}{\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}