\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]{Global Type Inference}
\begin{lstlisting}
(*@\only<1>{\color{gray}\texttt{List<? extends Object>} }@*)someList(){
    if(Math.random > 0.5){
        return new List(*@\only<1>{\color{gray}\texttt{<String>}}@*)("String");
    } else {
        return new List(*@\only<1>{\color{gray}\texttt{<Integer>}}@*)(42);
    }
}
\end{lstlisting}
\pause
\end{frame}

\begin{frame}[fragile]{Wildcards as Existential Types}
\begin{lstlisting}
(*@\only<2>{\color{red}$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$ }@*)someList(){
    if(Math.random > 0.5){
        return new List("String");
    } else {
        return new List(42);
    }
}
\end{lstlisting}
\pause
\begin{itemize}
\item \texttt{List<? extends Object>} $\implies$ $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$
\item \texttt{List<? super String>} $\implies$ $\wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\rwildcard{A}}$
\end{itemize}
\end{frame}

\begin{frame}[fragile]{Capture Conversion}
\rulename{T-Call-Wildcards} \\[1em]
\alt<-2>{
\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}}} \\
        \Delta, \overline{\Delta} \vdash \overline{\exptype{C}{\ol{T}}} <: [\ol{T'}/\ol{X}]\ol{T} \quad \quad \Delta, \overline{\Delta} \vdash [\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}
}{
\begin{center}
    $\begin{array}{l}
        \begin{array}{@{}c}
            \textit{mtype}(\texttt{shuffle}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \quad \quad 
            \texttt{l} : \wctype{\rwildcard{A}}{List}{\rwildcard{A}} \\
            \wildcard{A}{\type{Object}}{\bot} \vdash \exptype{List}{\type{A}} <: [\type{A}/\type{X}]\exptype{List}{\type{X}} \quad \quad
            \ [\type{A}/\type{X}]\exptype{List}{\type{X}} <: \wctype{\rwildcard{B}}{List}{\rwildcard{B}}
            \\
            \hline
        \vspace*{-0.3cm}\\
            \texttt{shuffle}(\expr{l}) : \wctype{\rwildcard{B}}{List}{\rwildcard{N}}
        \end{array}
    \end{array}$
    \end{center}
}
\pause
%Wildcard Capture
\begin{lstlisting}
<X> List<X> shuffle(List<X> l){ ... }

List<? extends Object> l;

shuffle(l) (*@\only<3>{\color{red}\texttt{: List<? extends Object>}}@*)
\end{lstlisting}
%why do we need capture constraints?
% List<List<?>> not a subtype of List<List<X>> for any X
\pause

\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,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}
\pause
\vfill
\begin{center}
    $\begin{array}{l}
        \begin{array}{@{}c}
            \textit{mtype}(\texttt{concat}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \\
            \texttt{l1} : \wctype{\rwildcard{A}}{List}{\rwildcard{A}}, \texttt{l2} : \wctype{\rwildcard{A}}{List}{\rwildcard{A}} \\
            \exptype{List}{\rwildcard{A}} \nless: [{\color{red}?}/\type{X}]\exptype{List}{\type{X}} \quad \quad
\exptype{List}{\rwildcard{B}} \nless: [{\color{red}?}/\type{X}]\exptype{List}{\type{X}}
            \\
            \hline
        \vspace*{-0.3cm}\\
            \texttt{shuffle}(\expr{l}) : {\color{red}\textbf{Errror}}
        \end{array}
    \end{array}$
\end{center}
\end{frame}

% - 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{\wildcard{A}{\type{U}}{\type{L}}}}{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}},
% \overline{\wtv{a} \lessdot \type{U}}, \overline{\type{L} \lessdot \wtv{a}}}
%         \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}
%         $\\[1em]
% \begin{itemize}
%     \item \textbf{Example:}
%     $\begin{array}[t]{c}
%     \exptype{List}{\type{String}} \lessdot \wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\type{A}}\\
%     \hline
%     \type{String} \doteq \wtv{a}, \wtv{a} \lessdot \type{Object}, \bot \lessdot \wtv{a}
%     \end{array}$
% \end{itemize}\\ \vfill
% \pause 
% \rulename{Capture} $
%    \begin{array}[c]{@{}ll}
%    \begin{array}[c]{l}
%        \wildcardEnv \vdash 
%        C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}} \lessdotCC \type{T} } \\ 
%      \hline
%      \vspace*{-0.4cm}\\
%      \wildcardEnv \cup \overline{\wildcard{C}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{U}}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{L}}}
%       \vdash C \cup \, \set{  
%        [\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} \lessdot \type{T} }
%    \end{array}
%     %\quad \ol{Y} = \textit{fresh}(\ol{X})
%     \quad \begin{array}[c]{l}
%      \ol{\rwildcard{C}} \ \text{fresh}\\
%      %\text{fv}(\type{T}) \neq \emptyset
%      \end{array}
%    \end{array}
%    $\\[1em]
% \begin{itemize}
% \item \textbf{Example:}
%     $\begin{array}[t]{c}
%     \wctype{\wildcard{A}{\type{U}}{\type{L}}}{List}{\type{A}} \lessdot \exptype{List}{\wtv{x}}\\
%     \hline
%  \wildcard{A}{\type{U}}{\type{L}} \vdash \exptype{List}{\type{A}} \lessdot \exptype{List}{\wtv{x}}
% \\
%     \hline
%     \wildcard{A}{\type{U}}{\type{L}} \vdash \type{A} \doteq \wtv{x}
%     \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}{\tv{x}} \lessdot {\only<2>{\color{red}}\tv{r}}, \type{String} \lessdot \tv{x},
\exptype{List}{\tv{y}} \lessdot {\only<2>{\color{red}}\tv{r}}, \type{Integer} \lessdot \tv{y}
$\\[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}{\tv{x}} \lessdot {\tv{r}}, \highlight{\tv{x} \doteq \type{String}},
\exptype{List}{\tv{y}} \lessdot {\tv{r}}, \highlight{\tv{y} \doteq \type{Integer}}
$
\pause
\\[0.5em]
\textbf{Substitution:}

$
\exptype{List}{\highlight{\type{String}}} \lessdot \tv{r},
\exptype{List}{\highlight{\type{Integer}}} \lessdot \tv{r}
$
\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]{Reduce}
$
\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}}}
\end{array}
\rulenameAfter{Reduce}
$\\[1em]
    \rulename{Reduce} $
        \begin{array}[c]{@{}ll}
        \begin{array}[c]{l}
            \wildcardEnv \vdash 
            C \cup \, \set{ \exptype{C}{\ol{S}} \lessdot
            \wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{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}},
\overline{\wtv{a} \lessdot \type{U}}, \overline{\type{L} \lessdot \wtv{a}}}
        \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}
        $\\[1em]
$
\begin{array}{l}
\exptype{List}{String} \lessdot {\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}},
\exptype{List}{Integer} \lessdot {\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}}
\\
\hline
\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}
\pause \\
\hline
\type{String} \lessdot \tv{u}, \tv{l} \lessdot \type{String},\\
\type{Integer} \lessdot \tv{u}, \tv{l} \lessdot \type{Integer}
\end{array}$
\end{frame}

\begin{frame}[fragile]
    %Es gibt stellen wo capture conversion möglich ist und Stellen wo es nicht ist.
    \frametitle{Wildcards are bound to Type}
\begin{lstlisting}
<X> List<List<X>> shuffle2D(List<List<X>> l) {...}

List<List<?>> l = ...;
shuffle2D(l); // Fehler!
\end{lstlisting}

\end{frame}

\begin{frame}[fragile]
    %Es gibt stellen wo capture conversion möglich ist und Stellen wo es nicht ist.
    \frametitle{Wildcards are bound to Type}
\begin{lstlisting}
<X> List<List<X>> shuffle2D(List<List<X>> l) {...}

(*@$\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$@*) l = ...;
shuffle2D(l); // Fehler!
\end{lstlisting}
\pause
\vfill
\begin{lstlisting}
<X> List<List<X>> shuffle2D(List<List<X>> l) {...}

(*@$\color{red}\wctype{\rwildcard{A}}{List}{\exptype{List}{\rwildcard{A}}}$@*) l = ...;
shuffle2D(l); // (*@\color{red}\textbf{Correct!}@*)
\end{lstlisting}
\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}}}$
$\only<4>{\highlight{\rulename{Subtitute}}}$

$
\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
\only<3>{\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<4>{\highlight{\type{String} \lessdot \tv{u}, \tv{l} \lessdot \type{String},
\type{Integer} \lessdot \tv{u}, \tv{l} \lessdot \type{Integer}}, \\}
\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

\end{array}$

\end{frame}

\begin{frame}[fragile]{Wildcard Elminiation}

\textit{Continue ...}\\
$
\begin{array}{l}
\type{String} \lessdot \tv{u}, \tv{l} \lessdot \type{String},
\type{Integer} \lessdot \tv{u}, \tv{l} \lessdot \type{Integer}, \\
\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}},
\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}
\end{array}$\\[1em]
\pause
\rulename{Super} \\
$
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \tv{a}\\
\hline
\wildcardEnv \vdash C \cup \set{ \wctype{\Delta'}{D}{[\ol{T}/\ol{X}]\ol{N}} \lessdot \tv{a}   }
%\set{\wctype{\ol{\wtype{W}}}{D}{[\ol{X}/\ol{Y}]\ol{Z}} \lessdot \tv{a}}
\end{array} \quad
\begin{array}{l}
\texttt{class} \ \exptype{C}{\ol{X}} \ \texttt{extends} \ \exptype{D}{\ol{N}} \\
\end{array}
$\\[1em]

\textit{Subtyping:}
\begin{lstlisting}
class String extends Object {...}
class Integer extends Object {...}
\end{lstlisting}
\pause
$
\begin{array}{l}
\type{String} \lessdot \tv{u}, \tv{l} \lessdot \type{String},
\type{Integer} \lessdot \tv{u}, \tv{l} \lessdot \type{Integer}, \\
\hline
\highlight{
\type{Object}} \lessdot \tv{u}, \tv{l} \lessdot \type{String},
\highlight{\type{Object}} \lessdot \tv{u}, \tv{l} \lessdot \type{Integer}
\\
\hline
\tv{u} \doteq \type{Object}, \ldots \\
\pause
{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}},
{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}}
\end{array}
$
\end{frame}

\begin{frame}[fragile]{Capture Conversion during Unify}
\rulename{Capture} $
   \begin{array}[c]{@{}ll}
   \begin{array}[c]{l}
       \wildcardEnv \vdash 
       C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}} \lessdotCC \type{T} } \\ 
     \hline
     \vspace*{-0.4cm}\\
     \wildcardEnv \cup \overline{\wildcard{C}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{U}}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{L}}}
      \vdash C \cup \, \set{  
       [\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} \lessdot \type{T} }
   \end{array}
    %\quad \ol{Y} = \textit{fresh}(\ol{X})
    \quad \begin{array}[c]{l}
     \ol{\rwildcard{C}} \ \text{fresh}\\
     %\text{fv}(\type{T}) \neq \emptyset
     \end{array}
   \end{array}
   $\\[1em]
\begin{itemize}
\item Constraints: ${\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}},
{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}}$
\end{itemize}
\pause
\vfill
$\begin{array}{l}
{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}},
{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}}
\pause 
\\
\hline
\highlight{\wildcard{X}{\tv{u}}{\tv{l}}} \vdash \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{x}},
{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\wtv{x}}
\pause
\\
\hline
\wildcard{X}{\tv{u}}{\tv{l}}, \highlight{\wildcard{Y}{\tv{u}}{\tv{l}}} \vdash \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{x}},
{\exptype{List}{\highlight{\rwildcard{Y}}}} \lessdotCC \exptype{List}{\wtv{x}}
\end{array}$
\end{frame}

\begin{frame}[fragile]{Wildcard Elimination}
\textit{Continue ...}\\
$
\begin{array}{l}
\tv{u} \doteq \type{Object}, \tv{l} \lessdot \type{String}, \tv{l} \lessdot \type{Integer}, \\
\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}},
\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}
\pause
\\
\hline
\tv{l} \lessdot \type{String}, \tv{l} \lessdot \type{Integer}, \\
\wctype{\wildcard{X}{\type{Object}}{\tv{l}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}},
\wctype{\wildcard{X}{\type{Object}}{\tv{l}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}
\pause
\\
\hline
\wildcard{X}{\tv{u}}{\tv{l}} \vdash \tv{l} \lessdot \type{String}, \tv{l} \lessdot \type{Integer}, \\
\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{x}},
\wctype{\wildcard{X}{\type{Object}}{\tv{l}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}
\pause
\\
\hline
\wildcard{X}{\type{Object}}{\tv{l}}, \wildcard{Y}{\type{Object}}{\tv{l}}, \vdash \tv{l} \lessdot \type{String}, \tv{l} \lessdot \type{Integer}, \\
\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{x}},
\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{x}}
\pause
\\
\hline
\wildcard{X}{\type{Object}}{\tv{l}}, \wildcard{Y}{\type{Object}}{\tv{l}}, \vdash \tv{l} \lessdot \type{String}, \tv{l} \lessdot \type{Integer}, \\
\rwildcard{X} \doteq \wtv{x},
\rwildcard{Y} \doteq \wtv{x}
\pause
\\
\hline
\wildcard{X}{\type{Object}}{\tv{l}}, \wildcard{Y}{\type{Object}}{\tv{l}}, \vdash \tv{l} \lessdot \type{String}, \tv{l} \lessdot \type{Integer}, \\
\rwildcard{X} \doteq \rwildcard{Y}
\end{array}$\\[0.5em]
\pause
\only<7>{
\rulename{Normalize}
$\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}} \vdash C \cup \set{\rwildcard{A} \doteq \type{T}}\\
                     \hline
[\type{U}/\type{A}]\wildcardEnv \vdash [\type{U}/\type{A}]
C \cup [\type{U}/\type{A}]\set{\ntv{a} \doteq \type{T}, \type{L} \doteq \type{U}}
\end{array}
$
}
\pause
$\begin{array}{l}
\hline
\tv{l} \lessdot \type{String}, \tv{l} \lessdot \type{Integer}, \highlight{\tv{l} \doteq \type{Object}}
\implies \textbf{Error!}
\end{array}$
\end{frame}

\begin{frame}[fragile]{Backtracking}
\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}
\begin{itemize}
\item \texttt{List<? extends Object> someList()} is not the correct type annotation in this case
\pause
\item Backtracking to:
$\exptype{List}{\tv{x}} \lessdot {\tv{r}}, \type{String} \lessdot \tv{x},
\exptype{List}{\tv{y}} \lessdot {\tv{r}}, \type{Integer} \lessdot \tv{y},
\tv{r} \lessdotCC \exptype{List}{\wtv{x}},
\tv{r} \lessdotCC \exptype{List}{\wtv{x}}$
\pause
\item Using the \rulename{Super} rule:\\
$\exptype{List}{\tv{x}} \lessdot {\tv{r}}, \highlight{\type{Object}} \lessdot \tv{x},
\exptype{List}{\tv{y}} \lessdot {\tv{r}}, \highlight{\type{Object}} \lessdot \tv{y},
\ldots $
\end{itemize}
\end{frame}

\begin{frame}[fragile]{Correct Solution}
\begin{lstlisting}
<X> List<X> concat(List<X> l1, List<X> l2){ ... }
(*@\color{red}\texttt{List<Object>}@*) someList(){
    if(Math.random > 0.5){
        return new List(*@\color{red}\texttt{<Object>}@*)("String");
    } else {
        return new List(*@\color{red}\texttt{<Object>}@*)(42);
    }
}

concat(someList(), someList())
\end{lstlisting}
\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]{Wildcard Placeholders}
\begin{lstlisting}
    List<List<?>> l;
    (*@\only<2>{\color{red}$\exptype{List}{\exptype{List}{\rwildcard{A}}}$}@*)l2 = l.map(x -> shuffle(x)(*@\only<2>{\color{red} : $\exptype{List}{\rwildcard{A}}$}@*));
    shuffle2D(l2); (*@\only<2>{\color{red} // ERROR!}@*)
\end{lstlisting}
\vfill
\textbf{Constraints:}\\
$
\begin{array}{l}
\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}}, \\
\exptype{List}{\exptype{List}{\wtv{x}}} \lessdot \tv{l2}, \\
\tv{l2} \lessdotCC \exptype{List}{\exptype{List}{\wtv{y}}}
\end{array}
$
\\ \pause
\vfill
\begin{itemize}
    \item Falsche Lösung:
$\color{red}\tv{l2} \doteq \exptype{List}{\exptype{List}{\rwildcard{A}}}$\\
% $
% \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}
% $
$
\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}{\rwildcard{A}}}, \\
\exptype{List}{\exptype{List}{\rwildcard{A}}} \lessdotCC \exptype{List}{\exptype{List}{\tv{y}}}
\end{array}
$
\pause
\item Korrekte Lösung = $\emptyset$. Programm ist inkorrekt
\end{itemize}
\end{frame}

\begin{frame}[fragile]{Conclusion}
\begin{itemize}
\item Wildcard creation at $\type{T} \lessdot \tv{a}$ constraints
\begin{itemize}
\item Wildcards are bound to a type
\end{itemize}
\pause
\item Eliminate Wildcards by setting upper = lower bound
\begin{itemize}
\item Removes Wildcards without backtracking
\end{itemize}
\pause
\item Capture Constraints for Capture Conversion during \unify{}
\pause
\item Wildcard Type Placeholders to keep free variables in scope
\pause
\vfill
\item \unify{} is Sound
\begin{itemize}
\pause
\item (but no completeness proof yet)
\end{itemize}
\end{itemize}

\end{frame}

\end{document}