\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  \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}

\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}$

$\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}
\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}
\end{document}
