VortragBadHonnef24/vortrag.tex

\documentclass[%
	pdftex,
	t,					% Folieninhalt am oberen Rand beginnen.
	10pt,				% Schriftgroesse
]{beamer}

% Einstellungen laden
\usetheme{DHBW}
\usepackage{xstring}
\usepackage[utf8]{inputenc}
%\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
%\usepackage{amsmath}
%\usepackage{amsfonts}
%\usepackage{amssymb}
\usepackage{alltt}
\usepackage{nameref}

\newcommand{\einstellung}[1]{%
  \expandafter\newcommand\csname #1\endcsname{}
  \expandafter\newcommand\csname setze#1\endcsname[1]{\expandafter\renewcommand\csname#1\endcsname{##1}}
}
\input{einstellungen_liste} % verfügbare Einstellungen
%\input{einstellungen} % lese Einstellungen
\setzetitel{Typeinferenz für Java mit Wildcards}
\setzeuntertitel{Bad Honnef 2024}
\setzedatum{30. April 2024}
\setzestudiengang{Stuidengang Informatik}
\setzedhbw{DHBW Stuttgart Campus Horb}
\setzeinternetadresse{www.dhbw-stuttgart.de/horb}
\setzeautor{Andreas Stadelmeier}%\\Andreas Stadelmeier}
\setzeschriftart{palatino} % oder goudysans, lmodern, libertine
%% Farben (Angabe in HTML-Notation mit großen Buchstaben)
\newcommand{\ladefarben}{%
	\definecolor{LinkColor}{HTML}{00007A}
	\definecolor{ListingBackground}{HTML}{FCF7DE}
}
%% Mathematikpakete benutzen (Pakete aktivieren)
%\usepackage{amsmath}
%\usepackage{amssymb}

%% Programmiersprachen Highlighting (Listings)
\newcommand{\listingsettings}{%
	\lstset{%
		language=Java,			% Standardsprache des Quellcodes
		%numbers=left,			% Zeilennummern links
		stepnumber=1,			% Jede Zeile nummerieren.
		numbersep=5pt,			% 5pt Abstand zum Quellcode
		numberstyle=\tiny,		% Zeichengrösse 'tiny' für die Nummern.
		breaklines=false,		% Zeilen umbrechen wenn notwendig.
		breakautoindent=true,	% Nach dem Zeilenumbruch Zeile einrücken.
		postbreak=\space,		% Bei Leerzeichen umbrechen.
		tabsize=2,				% Tabulatorgrösse 2
		basicstyle=\ttfamily\small, % Nichtproportionale Schrift, klein für den Quellcode
		showspaces=false,		% Leerzeichen nicht anzeigen.
		showstringspaces=false,	% Leerzeichen auch in Strings ('') nicht anzeigen.
		extendedchars=true,		% Alle Zeichen vom Latin1 Zeichensatz anzeigen.
		%captionpos=b,			% sets the caption-position to bottom
		%backgroundcolor=\color{ListingBackground}, % Hintergrundfarbe des Quellcodes setzen.
		xleftmargin=0pt,		% Rand links
		xrightmargin=0pt,		% Rand rechts
		%frame=single,			% Rahmen an
		%frameround=ffff,
		rulecolor=\color{darkgray},	% Rahmenfarbe
		fillcolor=\color{ListingBackground}
        showtabs=false,
        %breaklines=true,
        %breakatwhitespace=true,
        %basicstyle=\ttfamily\fontsize{8}{9.6}\selectfont, %\footnotesize
        escapeinside={(*@}{@*)},
        captionpos=t,float,abovecaptionskip=-\medskipamount
	}
}

\usepackage{prolog_slide}
%\input{prolog}

\usepackage[english, ngerman]{babel}
{\selectlanguage{ngerman}} % Paket babel benutzt neue deutsche Rechtschreibung
%{\selectlanguage{english}} % Paket babel benutzt Englisch


%%%%%%% Package Includes %%%%%%%

\usepackage[overlay, absolute]{textpos}
\usepackage{longtable}
\usepackage{pgffor} % für automatische Kapiteldateieinbindung
\usepackage{listings}
\usepackage{calc}


%%%%%% Configuration %%%%%

%% Anwenden der Einstellungen

\usepackage{\schriftart}
\ladefarben{}

% Titel, Autor und Datum
\title{\titel}
\subtitle{\untertitel}
\author{\autor}
\date{\datum}

% Literaturverweise (sowohl deutsch als auch englisch)
% \usepackage[
% 	%backend=biber,		% empfohlen. Falls biber Probleme macht: bibtex
% 	%backend=bibtex,		% empfohlen. Falls biber Probleme macht: bibtex
% 	bibwarn=true,
% 	bibencoding=utf8,	% wenn .bib in utf8, sonst ascii
% 	sortlocale=de_DE,	% oder en_US
% 	style=alphabetic	%Zitierstil. Siehe http://ctan.mirrorcatalogs.com/macros/latex/contrib/biblatex/doc/biblatex.pdf
% ]{biblatex}

%%%%%% Additional settings %%%%%%

% Hurenkinder und Schusterjungen verhindern
% http://projekte.dante.de/DanteFAQ/Silbentrennung
\clubpenalty=10000
\widowpenalty=10000
\displaywidowpenalty=10000

% Bildpfad
\graphicspath{{images/}}

% Einige häufig verwendete Sprachen
\lstloadlanguages{PHP,Python,Java,C,C++,bash}
\listingsettings{}
%\includeonly{content/01kapitel}
%\includeonly{content/01kapitel,content/02kapitel}
%\includeonly{content/02kapitel}
%\includeonly{content/03kapitel}
%\includeonly{content/04kapitel}
%\includeonly{content/02kapitel,content/03kapitel}
%\includeonly{content/04kapitel,content/05kapitel}
%\includeonly{content/05kapitel}
%\includeonly{content/04kapitel,content/05kapitel,content/06kapitel}
%\includeonly{content/06kapitel}
%\includeonly{content/07kapitel}
%\includeonly{content/08kapitel}
%\includeonly{content/07kapitel, content/08kapitel}
\usepackage{amsmath}
\usepackage{amssymb}
\newcommand\ddfrac[2]{\frac{\displaystyle #1}{\displaystyle #2}}

\newcommand{\tv}[1]{\mathit{ #1 }}
\newcommand{\tto}{\texttt{ -> }}
\newcommand{\funcType}{\ensuremath{\exptype{Function}{\type{T}, \type{R}}}}
%\newcommand{\fjtypeInsert}{\textbf{FJTypeInsert}}
\newcommand{\unifyGenerics}{\ensuremath{\gamma}}% {\ensuremath{\overline{\type{G}\triangleleft \type{H}}}}
\newcommand{\fjtype}{\textbf{FJType}}
\newcommand{\unify}{\textbf{Unify}}
\newcommand{\typeMethod}{\textbf{TYPEMethod}}
\newcommand{\typeExpr}{\textbf{TYPEExpr}}
\newcommand{\constraint}{\ensuremath{\mathit{c}}}%{\ensuremath{\mathtt{C}}}
\newcommand{\consSet}{C}%{\ensuremath{\overline{\mathtt{C}}}}
\newcommand{\orCons}{\textit{oc}}%{\ensuremath{\textbf{C}_{||}}}
\newcommand{\simpleCons}{\textit{sc}}
\newcommand{\overridesFunc}{\textit{overrides}}
\newcommand{\typeAssumptionsSymbol}{\ensuremath{\Theta}}
\newcommand{\typeAssumptions}{\ensuremath{(\mv{\Pi} ; \overline{\localVarAssumption})}}%{\ensuremath{(\overline{\methodAssumption} ; \overline{\fieldAssumption}; \overline{\localVarAssumption})}}
\newcommand{\constraints}{\ensuremath{\mathit{\overline{c}}}}
\newcommand{\itype}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\il}[1]{\ensuremath{\overline{\itype{#1}}}}
\newcommand{\gType}[1]{\texttt{#1}}
\newcommand{\mtypeEnvironment}{\ensuremath{\Pi}}
\newcommand{\methodAssumption}{\ensuremath{\mathtt{\lambda}}}
\newcommand{\localVarAssumption}{\ensuremath{\mathtt{\eta}}}
\newcommand{\expandLB}{\textit{expandLB}}
\newcommand{\type}[1]{\texttt{#1}}
\newcommand{\environmentvdash}{\Pi;\Delta;\Gamma \vdash}
\newcommand\subeq{\mathbin{\texttt{<:}}}
\newcommand\mv[1]{{\tt #1}}

\def\exptypett#1#2{\texttt{#1}\textrm{{\tt <#2}}\textrm{{\tt >}}\xspace}
\def\exp#1#2{#1(\,#2\,)\xspace}

\begin{document}
\bibliographystyle{unsrt}
% Titelfolie
\IfFileExists{content/00titelfolie}{%
	\input{content/00titelfolie}
}
{%
	%file does not exist
}

% Inhalt
\IfFileExists{content/01inhalt}{%
	\input{content/01inhalt}
}
{%
	%file does not exist
}

% Kapitel
\foreach \i in {01,02,03,04,05,06,07,08,09,10,...,99} {% 
	\edef\FileName{content/\i kapitel}%
		\IfFileExists{\FileName}{%
			\include{\FileName}
		}
		{%
			%file does not exist
		}
}
%\small
%\renewcommand{\pause}{}
\bibliographystyle{alpha}
%\centerslidesfalse
\begin{frame}
\maketitle
\end{frame}

\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
        \ol{v} : [\ol{T'}/\ol{X}]\ol{T}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \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
        \ol{v} : [\ol{T'}/\ol{X}]\ol{T}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \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{verbatim}
<X> X head(List<X> l){ ... }

head(new List<String>());
\end{verbatim}
\pause
$\begin{array}{l}
    \begin{array}{@{}c}
        \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}$\\[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{itemize}
    \item \texttt{head(new List<String>()) : String}
\end{itemize}
\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]
    \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}
untypedMethod(l){
    shuffle(l);
}
\end{verbatim}
\begin{itemize}
    \item $\lessdot $
\end{itemize}
\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



%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]{Reduce}
    \rulename{Reduce} $
        \begin{array}[c]{@{}ll}
        \begin{array}[c]{l}
            \wildcardEnv \vdash 
            C \cup \, \set{ \exptype{C}{\ol{S}} \lessdot
            \wctype{\overline{\rwildcard{A}}}{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}} }
        \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}
        $
\begin{itemize}
    \item \textbf{Example:}
    $\begin{array}[t]{c}
    \exptype{List}{\type{String}} \lessdot \wctype{\rwildcard{A}}{List}{\type{A}}\\
    \hline
    \type{String} \doteq \wtv{a}
    \end{array}$
    \item \textbf{Example:}
    $\begin{array}[t]{c}
    \wctype{\rwildcard{A}}{List}{\type{A}} \lessdot \exptype{List}{\type{String}}\\
    \hline
    \type{A} \doteq \type{String}
    \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");
    } else {
        return new List(42);
    }
}
    \end{lstlisting}
    \pause
$
\exptype{List}{String} \lessdot {\only<2>{\color{red}}\tv{r}},
\exptype{List}{Integer} \lessdot {\only<2>{\color{red}}\tv{r}}
$\\[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}{String} \lessdot {\tv{r}},
\exptype{List}{Integer} \lessdot {\tv{r}},
\highlight{\tv{r} \doteq \wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}}
$
\pause
\\[0.5em]
\textbf{Substitution:}

$
\exptype{List}{String} \lessdot \highlight{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}},
\exptype{List}{Integer} \lessdot \highlight{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}}
$
\end{frame}

\begin{frame}[fragile]
$
\begin{array}{l}
\exptype{List}{String} \lessdot \highlight{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}},
\exptype{List}{Integer} \lessdot \highlight{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}}
\\
\hline
\type{String} \doteq \wtv{x1}, \type{Integer} \doteq \wtv{x2}
\end{array}
\rulenameAfter{Reduce}
$
\end{frame}

\begin{frame}[fragile]{Wildcard Elminiation}
\begin{lstlisting}
<X> List<X> concat(List<X> l1, List<X> l2){ ... }
someList(){
    if(Math.random > 0.5){
        return new List("String");
    } else {
        return new List(42);
    }
}

concat(someList(), someList())
\end{lstlisting}

\only<1>{\textbf{Input}:}
$\only<2>{\highlight{\rulename{General}}}$
$\only<3>{\highlight{\rulename{Reduce}}}$

$
\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}}
\pause
\\
\hline
\exptype{List}{String} \lessdot \only<2>{\highlight}{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}},
\exptype{List}{Integer} \lessdot \only<2>{\highlight}{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}},\\
\only<2>{\highlight}{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}},
\only<2>{\highlight}{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}}
\pause
\\
\hline
\highlight{\type{String} \doteq \wtv{x1}, \wtv{x1} \lessdot \tv{u}, \tv{l} \lessdot \wtv{x1},
\type{Integer} \doteq \wtv{x2}, \wtv{x2} \lessdot \tv{u}, \tv{l} \lessdot \wtv{x2}}, \\
\only<2>{\highlight}{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}},
\only<2>{\highlight}{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{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}

$
\begin{array}{l}
\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\tv{x}}, \\
\exptype{List}{\exptype{List}{\tv{x}}} \lessdot \tv{l2}, \\
\tv{l2} \lessdotCC \exptype{List}{\exptype{List}{\tv{y}}}
\end{array}
$

\begin{itemize}
    \item Falsche Lösung:
    $
\begin{array}{l}
\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\highlight{\rwildcard{A}}}, \\
\exptype{List}{\exptype{List}{\tv{x}}} \lessdot \exptype{List}{\exptype{List}{\tv{x}}},
\tv{r} \lessdot \tv{l2},
\tv{l2} \lessdotCC \exptype{List}{\exptype{List}{\tv{y}}}
\end{array}
$
\end{itemize}
\end{frame}

\begin{frame}[fragile]{Lösung durch Unify}
$
\begin{array}{l}
\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\tv{x}}, \\
\exptype{List}{\exptype{List}{\tv{x}}} \lessdot \tv{l2}, \\
\tv{l2} \lessdotCC \exptype{List}{\exptype{List}{\tv{y}}}
\end{array}
$

\begin{itemize}
    \item Falsche Lösung:
    $
\begin{array}{l}
\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\highlight{\rwildcard{A}}}, \\
\exptype{List}{\exptype{List}{\tv{x}}} \lessdot \exptype{List}{\exptype{List}{\tv{x}}},
\tv{r} \lessdot \tv{l2},
\tv{l2} \lessdotCC \exptype{List}{\exptype{List}{\tv{y}}}
\end{array}
$
\end{itemize}
\end{frame}

\begin{frame}[fragile]
\begin{verbatim}
    List<List<?>> l;
    l2 = l.map(x -> shuffle(x));
    shuffle2D(l2);
\end{verbatim}

$
\begin{array}{l}
\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{array}
$
\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}