712 lines
23 KiB
TeX
712 lines
23 KiB
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{black}, % Rahmenfarbe
|
|
fillcolor=\color{black},
|
|
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{B}}{List}{\rwildcard{B}} \\
|
|
\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{concat}(\expr{l1}, \expr{l2}) : {\color{red}\textbf{Errror}}
|
|
\end{array}
|
|
\end{array}$
|
|
\end{center}
|
|
\end{frame}
|
|
|
|
\begin{frame}[fragile]{Wildcard Creation}
|
|
\begin{lstlisting}
|
|
(*@\only<2>{$\color{red}\tv{r}$ }@*)someList(){
|
|
if(Math.random > 0.5){
|
|
return new List<(*@\only<2>{$\color{red}\tv{x}$}@*)>("String");
|
|
} else {
|
|
return new List<(*@\only<2>{$\color{red}\tv{y}$}@*)>(42);
|
|
}
|
|
}
|
|
\end{lstlisting}
|
|
\pause
|
|
$
|
|
\exptype{List}{\tv{x}} \lessdot {\only<2>{\color{red}}\tv{r}}, \type{String} \lessdot {\only<2>{\color{red}}\tv{x}},
|
|
\exptype{List}{\tv{y}} \lessdot {\only<2>{\color{red}}\tv{r}}, \type{Integer} \lessdot {\only<2>{\color{red}}\tv{y}}
|
|
$\\[1em]
|
|
\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}, \hfill
|
|
\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},\hfill
|
|
\type{Integer} \lessdot \tv{u}, \tv{l} \lessdot \type{Integer}
|
|
\end{array}$
|
|
\end{frame}
|
|
|
|
\begin{frame}[fragile]{Wildcard Eliminiation}
|
|
\begin{lstlisting}
|
|
<X> List<X> concat(List<X> l1, List<X> l2){ ... }
|
|
|
|
List<? extends Object> someList(){
|
|
if(Math.random > 0.5){
|
|
return new List<>("String");
|
|
} else {
|
|
return new List<>(42);
|
|
}
|
|
}
|
|
\end{lstlisting}
|
|
|
|
\end{frame}
|
|
\begin{frame}[fragile]{Wildcard Eliminiation}
|
|
\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);
|
|
}
|
|
}
|
|
|
|
(*@\color{red}\texttt{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}},
|
|
\highlight{\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]{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}}}} \lessdot \exptype{List}{\wtv{x}}
|
|
\end{array}$
|
|
\end{frame}
|
|
|
|
\begin{frame}[fragile]{Wildcard Elimination}
|
|
\textit{Continue ...}\\
|
|
$
|
|
\begin{array}{l}
|
|
\ldots \\
|
|
\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
|
|
\begin{itemize}
|
|
\item Remove Wildcard by setting lower bound = upper bound
|
|
\end{itemize}
|
|
|
|
$\begin{array}{l}
|
|
\ldots \\
|
|
\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}{\wtv{x}} \lessdot \tv{z}, \\
|
|
\exptype{List}{\tv{z}} \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}
|