344 lines
15 KiB
TeX
344 lines
15 KiB
TeX
|
|
\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate]{lipics-v2021}
|
|
%This is a template for producing LIPIcs articles.
|
|
%See lipics-v2021-authors-guidelines.pdf for further information.
|
|
%for A4 paper format use option "a4paper", for US-letter use option "letterpaper"
|
|
%for british hyphenation rules use option "UKenglish", for american hyphenation rules use option "USenglish"
|
|
%for section-numbered lemmas etc., use "numberwithinsect"
|
|
%for enabling cleveref support, use "cleveref"
|
|
%for enabling autoref support, use "autoref"
|
|
%for anonymousing the authors (e.g. for double-blind review), add "anonymous"
|
|
%for enabling thm-restate support, use "thm-restate"
|
|
%for enabling a two-column layout for the author/affilation part (only applicable for > 6 authors), use "authorcolumns"
|
|
%for producing a PDF according the PDF/A standard, add "pdfa"
|
|
|
|
%\pdfoutput=1 %uncomment to ensure pdflatex processing (mandatatory e.g. to submit to arXiv)
|
|
%\hideLIPIcs %uncomment to remove references to LIPIcs series (logo, DOI, ...), e.g. when preparing a pre-final version to be uploaded to arXiv or another public repository
|
|
|
|
%\graphicspath{{./graphics/}}%helpful if your graphic files are in another directory
|
|
|
|
\usepackage[T1]{fontenc}
|
|
|
|
\usepackage{cite}
|
|
\usepackage[disable]{todonotes} % [disable]
|
|
\usepackage[utf8]{inputenc}
|
|
\usepackage{hyperref}
|
|
\usepackage{amsmath}
|
|
\usepackage{amssymb}
|
|
\usepackage{subcaption}
|
|
\usepackage{prftree}
|
|
\usepackage{tabularx}
|
|
\usepackage{multicol}
|
|
\usepackage{nicematrix}
|
|
\usepackage{tikz}
|
|
\usepackage{soul}
|
|
\newcommand{\mathcolorbox}[2]{\colorbox{#1}{$\displaystyle #2$}}
|
|
\usepackage{cancel}
|
|
\usepackage{tcolorbox}
|
|
|
|
\input{prolog}
|
|
|
|
\bibliographystyle{plainurl}% the mandatory bibstyle
|
|
|
|
\title{Global Type Inference for Featherweight Java with Wildcards} %TODO Please add
|
|
|
|
%\titlerunning{Dummy short title} %TODO optional, please use if title is longer than one line
|
|
|
|
\author{Andreas Stadelmeier}{DHBW Stuttgart, Campus Horb, Germany}{a.stadelmeier@hb.dhbw-stuttgart.de}{}{}%TODO mandatory, please use full name; only 1 author per \author macro; first two parameters are mandatory, other parameters can be empty. Please provide at least the name of the affiliation and the country. The full address is optional. Use additional curly braces to indicate the correct name splitting when the last name consists of multiple name parts.
|
|
|
|
\author{Martin Plümicke}{DHBW Stuttgart, Campus Horb, Germany}{pl@dhbw.de}{}{}
|
|
|
|
\author{Peter Thiemann}{Universität Freiburg, Institut für Informatik, Germany}{thiemann@informatik.uni-freiburg.de}{}{}
|
|
|
|
\authorrunning{A. Stadelmeier and M. Plümicke and P. Thiemann} %TODO mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et al.'
|
|
|
|
\Copyright{Andreas Stadelmeier and Martin Plümicke and Peter Thiemann} %TODO mandatory, please use full first names. LIPIcs license is "CC-BY"; http://creativecommons.org/licenses/by/3.0/
|
|
|
|
\ccsdesc[500]{Software and its engineering~Language features}
|
|
%\ccsdesc[300]{Software and its engineering~Syntax}
|
|
|
|
\keywords{type inference, Java, subtyping, generics} %TODO mandatory; please add comma-separated list of keywords
|
|
|
|
\category{} %optional, e.g. invited paper
|
|
|
|
\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
|
|
%\relatedversiondetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93]{Classification (e.g. Full Version, Extended Version, Previous Version}{URL to related version} %linktext and cite are optional
|
|
|
|
%\supplement{}%optional, e.g. related research data, source code, ... hosted on a repository like zenodo, figshare, GitHub, ...
|
|
%\supplementdetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93, subcategory={Description, Subcategory}, swhid={Software Heritage Identifier}]{General Classification (e.g. Software, Dataset, Model, ...)}{URL to related version} %linktext, cite, and subcategory are optional
|
|
|
|
%\funding{(Optional) general funding statement \dots}%optional, to capture a funding statement, which applies to all authors. Please enter author specific funding statements as fifth argument of the \author macro.
|
|
|
|
%\acknowledgements{I want to thank \dots}%optional
|
|
|
|
%\nolinenumbers %uncomment to disable line numbering
|
|
|
|
|
|
|
|
%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
\EventEditors{John Q. Open and Joan R. Access}
|
|
\EventNoEds{2}
|
|
\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
|
|
\EventShortTitle{CVIT 2016}
|
|
\EventAcronym{CVIT}
|
|
\EventYear{2016}
|
|
\EventDate{December 24--27, 2016}
|
|
\EventLocation{Little Whinging, United Kingdom}
|
|
\EventLogo{}
|
|
\SeriesVolume{42}
|
|
\ArticleNo{23}
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
\begin{document}
|
|
|
|
\maketitle
|
|
|
|
%TODO mandatory: add short abstract of the document
|
|
\begin{abstract}
|
|
TODO: Abstract
|
|
\end{abstract}
|
|
|
|
\input{introduction}
|
|
|
|
%We could do a translation from Java to \wildFJ explaining implicit capture conversion
|
|
|
|
\section{Soundness of Typing}
|
|
|
|
|
|
We show soundness with the type rules statet in \cite{WildcardsNeedWitnessProtection}.
|
|
A correct \FGJGT{} program can be converted to a correct \wildFJ{} program.
|
|
|
|
\begin{figure}
|
|
$\begin{array}{rcl}
|
|
| \texttt{x} |
|
|
& = & \texttt{x} \\
|
|
| \texttt{let} \ \texttt{x} : \type{T} = \texttt{e},\, \ol{x} : \ol{T} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x}) |
|
|
& = & |\texttt{e}|.\texttt{m}(\ol{|e|}) \\
|
|
| \texttt{let} \ \texttt{x} : \type{T} = \texttt{e}\ \texttt{in}\ \texttt{x}.\texttt{f} |
|
|
& = & |\texttt{e}|.\texttt{f} \\
|
|
| \texttt{e} \elvis{} \texttt{e} |
|
|
& = & |\texttt{e}| \elvis{} |\texttt{e}| \\
|
|
\end{array}$
|
|
\caption{Erasure} \label{fig:erasure}
|
|
\end{figure}
|
|
|
|
|
|
|
|
\input{tRules}
|
|
|
|
\input{tiRules}
|
|
|
|
\input{constraints}
|
|
|
|
\section{Capture Conversion}
|
|
The input to our type inference algorithm does not contain let statements.
|
|
Those are added after computing a type solution.
|
|
Let statements act as capture conversion and only have to be applied in method calls involving wildcard types.
|
|
|
|
\begin{figure}
|
|
\begin{minipage}{0.45\textwidth}
|
|
\begin{lstlisting}[style=fgj]
|
|
<X> List<X> clone(List<X> l);
|
|
example(p){
|
|
return clone(p);
|
|
}
|
|
\end{lstlisting}
|
|
\end{minipage}%
|
|
\hfill
|
|
\begin{minipage}{0.5\textwidth}
|
|
\begin{lstlisting}[style=tfgj]
|
|
(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){
|
|
return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in
|
|
clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
|
|
}
|
|
\end{lstlisting}
|
|
\end{minipage}
|
|
\caption{Type inference adding capture conversion}\label{fig:addingLetExample}
|
|
\end{figure}
|
|
|
|
Figure \ref{fig:addingLetExample} shows a let statement getting added to the typed output.
|
|
The method \texttt{clone} cannot be called with the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
|
|
After a capture conversion \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$ with $\rwildcard{X}$ being a free variable.
|
|
Afterwards we have to find a supertype of $\exptype{List}{\rwildcard{X}}$, which does not contain free variables
|
|
($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in this case).
|
|
|
|
During the constraint generation step most types are not known yet and are represented by a type placeholder.
|
|
During a methodcall like the one in the \texttt{example} method in figure \ref{fig:ccExample} the type of the parameter \texttt{p}
|
|
is not known yet.
|
|
The type \texttt{List<?>} would be one possibility as a parameter type for \texttt{p}.
|
|
To make wildcards work for our type inference algorithm \unify{} has to apply capture conversions if necessary.
|
|
|
|
The type placeholder $\tv{r}$ is the return type of the \texttt{example} method.
|
|
One possible type solution is $\tv{p} \doteq \tv{r} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$,
|
|
which leads to:
|
|
\begin{verbatim}
|
|
List<?> example(List<?> p){
|
|
return clone(p);
|
|
}
|
|
\end{verbatim}
|
|
|
|
But by substituting $\tv{p} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in the constraint
|
|
$\tv{p} \lessdot \exptype{List}{\wtv{x}}$ leads to
|
|
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{x}}$.
|
|
|
|
To make this typing possible we have to introduce a capture conversion via a let statement:
|
|
$\texttt{return}\ (\texttt{let}\ \texttt{x} : \wctype{\rwildcard{X}}{List}{\rwildcard{X}} = \texttt{p}\ \texttt{in} \
|
|
\texttt{clone}\generics{\rwildcard{X}}(x) : \wctype{\rwildcard{X}}{List}{\rwildcard{X}})$
|
|
|
|
Inside the let statement the variable \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$
|
|
|
|
$
|
|
\begin{array}[c]{l}
|
|
\wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \rwildcard{G}}\\
|
|
\hline
|
|
[\type{G}/\wtv{a}]\wildcardEnv \vdash [\type{G}/\wtv{a}]C \cup \set{\tv{a} \doteq \type{G}}
|
|
\end{array}
|
|
$
|
|
|
|
This spawns additional problems.
|
|
%TODO
|
|
%we need the constraint set to be a list
|
|
%not on every constraint CC is allowed. The unify algorithm does not know the context in which a constraint was generated
|
|
%free type variables cannot leave the scope of the method call
|
|
|
|
\begin{figure}
|
|
\begin{minipage}{0.45\textwidth}
|
|
\begin{verbatim}
|
|
<X> List<X> clone(List<X> l){...}
|
|
|
|
example(p){
|
|
return clone(p);
|
|
}
|
|
\end{verbatim}
|
|
\end{minipage}%
|
|
\hfill
|
|
\begin{minipage}{0.35\textwidth}
|
|
\begin{constraintset}
|
|
\textbf{Constraints:}\\
|
|
$
|
|
\tv{p} \lessdot \exptype{List}{\wtv{x}}, \\
|
|
\tv{p} \lessdot \tv{r}, \\
|
|
\tv{p} \lessdot \type{Object},
|
|
\tv{r} \lessdot \type{Object}
|
|
$
|
|
\end{constraintset}
|
|
\end{minipage}
|
|
|
|
\caption{Type inference example}\label{fig:ccExample}
|
|
\end{figure}
|
|
|
|
In addition with free variables this leads to unwanted behaviour.
|
|
Take the constraint
|
|
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ for example.
|
|
After a capture conversion from $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ to $\exptype{List}{\rwildcard{Y}}$ and a substitution $\wtv{a} \doteq \rwildcard{Y}$
|
|
we get
|
|
$\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$.
|
|
Which is correct if we apply capture conversion to the left side:
|
|
$\exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$
|
|
If the input constraints did not intend for this constraint to undergo a capture conversion then \unify{} would produce an invalid
|
|
type solution due to:
|
|
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \nless: \exptype{List}{\rwildcard{X}}$
|
|
The reason for this is the \texttt{S-Exists} rule's premise
|
|
$\text{dom}(\Delta') \cap \text{fv}(\exptype{List}{\rwildcard{X}}) = \emptyset$.
|
|
|
|
Additionally free variables are not allowed to leave the scope of a capture conversion
|
|
introduced by a let statement.
|
|
%TODO we combat both of this with wildcard type placeholders (? flag)
|
|
|
|
Type placeholders which are not flagged as possible free variables ($\wtv{a}$) can never hold a free variable or a type containing free variables.
|
|
Constraint generation places these standard place holders at method return types and parameter types.
|
|
\begin{lstlisting}[style=fgj]
|
|
<X> List<X> clone(List<X> l);
|
|
(*@$\red{\tv{r}}$@*) example((*@$\red{\tv{p}}$@*) p){
|
|
return clone(p);
|
|
}
|
|
\end{lstlisting}
|
|
This prevents type solutions that contain free variables in parameter and return types.
|
|
When calling a method which already has a type annotation we have to consider adding a capture conversion in form of a let statement.
|
|
The constraint $\tv{p} \lessdot \exptype{List}{\wtv{x}}$ signals the \unify{} algorithm that here a capture conversion is possible.
|
|
$\sigma(\tv{p}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, \sigma(\tv{r}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, $ is a possible solution.
|
|
But only when adding a capture conversion:
|
|
\begin{lstlisting}[style=fgj]
|
|
<X> List<X> clone(List<X> l);
|
|
(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){
|
|
return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
|
|
}
|
|
\end{lstlisting}
|
|
\unify{}'s type solution for constraints involving free variables only holds under special circumstances.
|
|
Constraint $\tv{p} \lessdot \exptype{List}{\wtv{x}}$ only holds when a capture conversion is applied to the left side:
|
|
$\Delta, \Delta' \vdash CC(\sigma(\tv{p})) <: \sigma(\exptype{List}{\wtv{x}})$
|
|
and there is a an environment $\Delta'$ holding all type variables used inside the subtype relation.
|
|
This is done by packing the method call inside a let statement, which performs a capture conversion on all expressions used as parameters.
|
|
%TODO: Explain (do soundness and TYPE algorithm first)
|
|
|
|
A type solution of the \unify{} algorithm only guarantees correct subtyping for constraints not containing free variables.
|
|
Constraints like $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ only guarantee
|
|
$\Delta, \Delta' \vdash \sigma(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) <: \sigma(\exptype{List}{\wtv{a}})$ when
|
|
adding a $\Delta'$ environment and applying a capture conversion on the left side.
|
|
In this case the type solution would be $\tv{a} \to \rwildcard{X}$ leading to:
|
|
$\Delta, \set{\rwildcard{X}} \vdash \exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$
|
|
|
|
This is the reason input constraints containing free variables cannot be stored in a set.
|
|
$\wtv{a} \lessdot \wtv{b}$ is not the same as $\wtv{a} \lessdot \wtv{b}$.
|
|
Both constraints will end up the same after a substitution for both placeholders $\tv{a}$ and $\tv{b}$.
|
|
But afterwards a capture conversion is applied, which can generate different types on the left sides.
|
|
\begin{itemize}
|
|
\item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Y}}$
|
|
\item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Z}}$
|
|
\end{itemize}
|
|
|
|
|
|
Also the subtype relation is not symmetric for types involving free type variables.
|
|
$\type{T} \lessdot \type{S}$ and $\type{S} \lessdot \type{T}$ doesnt mean $\type{T} = \type{S}$, because we apply a capture conversion on every constraint.
|
|
Only for constraints without free variables symmetry is given.
|
|
|
|
% Can untyped methods also get a capture conversion? NO!
|
|
|
|
%TODO: Explain why capture conversion is needed (also in respect to martins algorithm)
|
|
|
|
\input{Unify}
|
|
|
|
\section{Limitations}
|
|
|
|
This example does not work:
|
|
|
|
\begin{minipage}{0.35\textwidth}
|
|
\begin{verbatim}
|
|
class Example{
|
|
<A> Pair<A,A> make(List<A> l){...}
|
|
<A> bool compare(Pair<A,A> p){...}
|
|
|
|
bool test(List<?> l){
|
|
return compare(make(l));
|
|
}
|
|
}
|
|
\end{verbatim}
|
|
\end{minipage}%
|
|
\hfill
|
|
\begin{minipage}{0.55\textwidth}
|
|
\begin{constraintset}
|
|
\textbf{Constraints:}\\
|
|
$
|
|
\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{x}}, \\
|
|
\exptype{Pair}{\wtv{x},\wtv{x}} \lessdot \tv{r}, \\
|
|
\tv{r} \lessdot \exptype{Pair}{\tv{z}, \tv{z}}%,\\
|
|
%\tv{y} \lessdot \tv{m}
|
|
$\\
|
|
\end{constraintset}
|
|
\end{minipage}
|
|
|
|
|
|
\input{conclusion}
|
|
|
|
\include{soundness}
|
|
%\include{termination}
|
|
|
|
\bibliography{martin}
|
|
|
|
\appendix
|
|
%\include{examples}
|
|
%\input{exampleWildcardParameter}
|
|
%\input{commonPatternsProof}
|
|
%\input{appendix}
|
|
\end{document}
|