commit 8f3d49d70f3a2e7fe15da78f53e37eea17291f68 Author: Andreas Stadelmeier Date: Wed Dec 27 14:29:33 2023 +0100 Initial commit. Applying LipICS style to wildcard paper diff --git a/TIforWildFJ.tex b/TIforWildFJ.tex new file mode 100644 index 0000000..9f0bbad --- /dev/null +++ b/TIforWildFJ.tex @@ -0,0 +1,319 @@ + +\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} + +%\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] + List clone(List 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} + List clone(List 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] + List clone(List 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] + List clone(List 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{ + Pair make(List l){...} + bool compare(Pair 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} diff --git a/cc-by.pdf b/cc-by.pdf new file mode 100644 index 0000000..3b7aba1 Binary files /dev/null and b/cc-by.pdf differ diff --git a/conclusion.tex b/conclusion.tex new file mode 100644 index 0000000..988cd4d --- /dev/null +++ b/conclusion.tex @@ -0,0 +1,35 @@ +\section{Conclusion and Further Work} +% we solved the problems given in the introduction (see examples TODO give names to examples) +The problems introduced in the openening \ref{challenges} can be solved via our \unify{} algorithm (see examples \ref{example1} and \ref{example2}). +As you can see by the given examples our type inference algorithm can calculate +type solutions for programs involving wildcards. + +Going further we try to proof soundness and completeness for \unify{}. + + +% The tricks are: +% \begin{itemize} +% \item Erasing wildcards by setting $\type{U} \doteq \type{L}$ +% \end{itemize} + +% Improvements: +% \begin{itemize} +% \item Straightforward algorithm. Less data types used. Only two sort of constraints. +% \end{itemize} + +% \subsection{Problems} +% The algorithm is lacking completeness. + +% \begin{verbatim} +% void m(List a){} + +% m2(l){ +% l.add("String"); +% } +% \end{verbatim} + +%COnstraints: +%l <. List +%String <. a + + diff --git a/constraints.tex b/constraints.tex new file mode 100644 index 0000000..9ef6c51 --- /dev/null +++ b/constraints.tex @@ -0,0 +1,337 @@ + +\section{Constraint generation} +Our type inference algorithm is split into two parts. +A constraint generation step \textbf{TYPE} and a \unify{} step. + +Method names are not unique. +It is possible to define the same method in multiple classes. +The \TYPE{} algorithm accounts for that by generating Or-Constraints. +This can lead to multiple possible solutions. + +%\subsection{Well-Formedness} + + +%Why do we need a constraint generation step? +%% The problem is NP-Hard +%% a method call, does not know which type it will produce +%% depending on its type the + +%NO equals constraints during the constraint generation step! +\begin{figure}[tp] + \begin{align*} + % Type + \type{T}, \type{U} &::= \tv{a} \mid \wtv{a} \mid \mv{X} \mid {\wcNtype{\Delta}{N}} && \text{types and type placeholders}\\ + \type{N} &::= \exptype{C}{\il{T}} && \text{class type (with type variables)} \\ + % Constraints + \simpleCons &::= \type{T} \lessdot \type{U} && \text{subtype constraint}\\ + \orCons{} &::= \set{\set{\overline{\simpleCons_1}}, \ldots, \set{\overline{\simpleCons_n}}} && \text{or-constraint}\\ + \constraint &::= \simpleCons \mid \orCons && \text{constraint}\\ + \consSet &::= \set{\constraints} && \text{constraint set}\\ + % Method assumptions: + \methodAssumption &::= \exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \exptype{}{\ol{Y} + \triangleleft \ol{P}}\ \ol{\type{T}} \to \type{T} && + \text{method + type assumption}\\ + \localVarAssumption &::= \texttt{x} : \itype{T} && \text{parameter + assumption}\\ + \mtypeEnvironment & ::= \overline{\methodAssumption} & + & \text{method type environment} \\ + \typeAssumptionsSymbol &::= ({\mtypeEnvironment} ; \overline{\localVarAssumption}) + \end{align*} + \caption{Syntax of constraints and type assumptions.} + \label{fig:syntax-constraints} +\end{figure} + +\begin{figure}[tp] + \begin{gather*} + \begin{array}{@{}l@{}l} + \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\ol{X} \triangleleft \ol{N}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, K \, \overline{M} \}}) =\\ + & \begin{array}{ll@{}l} +\textbf{let} & \forall \texttt{m} \in \ol{M}: \tv{a}_\texttt{m}, \ol{\tv{a}_m} \ \text{fresh} \\ + & \ol{\methodAssumption} = \begin{array}[t]{l} + \set{ \mv{m'} : (\exptype{C}{\ol{X} \triangleleft \ol{N}} \to \ol{\tv{a}} \to \tv{a}) \mid + \mv{m'} \in \ol{M} \setminus \set{\mv{m}}, \, \tv{a}\, \ol{\tv{a}}\ \text{fresh} } \\ +\ \cup \, \set{\mv{m} : (\exptype{C}{\ol{X} \triangleleft \ol{N}} \to \ol{\tv{a}_m} \to \tv{a}_\mv{m})} +\end{array} + \\ + & C_m = \typeExpr(\mtypeEnvironment \cup \set{\mv{this} : + \exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}_m} }, \texttt{e}, \tv{a}_\texttt{m}) \\ +\textbf{in} + & { ( \mtypeEnvironment \cup \ol{\methodAssumption}, \, + \bigcup_{\texttt{m} \in \ol{M}} C_m ) + } + \end{array} + \end{array} + \end{gather*} + \caption{Constraint generation for classes} + \label{fig:constraints-for-classes} +\end{figure} + +% \textbf{Method Assumptions} + +% %$\Pi$ is a set of method assumptions used by the $\fjtype{}$ algorithm. + +% % \begin{verbatim} +% % class Example { +% % Y m(Example p){ ... } +% % } +% % \end{verbatim} + +% In Featherweight Java a method type is bound to a specific class. +% The class \texttt{Example} shown above contains one method \texttt{m}: + +% \begin{displaymath} +% \textit{mtype}({\texttt{m}, \exptype{Example}{\type{X}}}) = \generics{\type{Y}} \ \exptype{Example}{\type{Y}} \to \type{Y} +% \end{displaymath} + +% $\Pi$ is a set of method assumptions used by the $\fjtype{}$ algorithm. +% It's a map of method types to method names. +% Every method name has a set of possible types, +% because there could be more than one method with the same name in a program consisting out of multiple classes. +% To simplify the syntax of method assumptions, we add the inheriting class type to the parameter list: + +% \begin{displaymath} +% \Pi = \set{ \texttt{m} : \generics{\type{X}, \type{Y}} \ (\exptype{Example}{\type{X}}, \exptype{Example}{\type{Y}}) \to \type{Y}} +% \end{displaymath} + +% \begin{verbatim} +% class Example { } + +% Y m(Example this, Example p){ ... } +% \end{verbatim} + +The constraint generation step is the same as the one for regular Generic Featherweight Java. +Wildcard types are not used during the constraint generation step and have no influence on it. + +\begin{displaymath} + \begin{array}{@{}l@{}l} + \typeExpr{} &({\mtypeEnvironment} , \texttt{e}.\texttt{f}, \tv{a}) = \\ + & \begin{array}{ll} + \textbf{let} + & \tv{r} \ \text{fresh} \\ + & \consSet_R = \typeExpr({\mtypeEnvironment}, \texttt{e}, \tv{r})\\ + & \constraint = \begin{array}[t]{@{}l@{}l} + \orCons\set{ + \set{ & + \tv{r} \lessdot \exptype{C}{\ol{\wtv{a}}} , + [\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} , \ol{\tv{a}} \lessdot [\overline{\tv{a}}/\ol{X}]\ol{N} + } \\ + & \quad \mid \mv{T}\ \mv{f} \in \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots} + , \, \overline{\wtv{a}} \text{ fresh} + }\end{array}\\ + {\mathbf{in}} & { + \consSet_R \cup \set{\constraint}} + \end{array} + \end{array} +\end{displaymath} + +The set of method assumptions returned by the \textit{mtypes} function is used to generate the constraints for a method call expression: + +There are two kinds of method calls. +The ones to already typed methods and calls to untyped methods. + +%Soundness: TODO + + +\begin{displaymath} +\begin{array}{@{}l@{}l} + \typeExpr{} & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a} ) = \\ + & \begin{array}{ll} + \textbf{let} + & \tv{r}, \ol{\tv{r}} \text{ fresh} \\ + & \consSet_R = \typeExpr(({\mtypeEnvironment} ; + \overline{\localVarAssumption}), \texttt{e}, \tv{r})\\ + & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \ol{e}, \ol{\tv{r}}) \\ + & \begin{array}{@{}l@{}l} + \constraint = \orCons\set{ & + \begin{array}[t]{l} + \{ \tv{r} \lessdot \exptype{C}{\ol{\wtv{a}}}, + \overline{\tv{r}} \lessdot \ol{T}, + \type{T} \lessdot \tv{a}, + \overline{\wtv{a}} \lessdot \ol{N} \} + \end{array}\\ + & \ |\ + (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \overline{\type{T}} \to \type{T}) \in + {\mtypeEnvironment} + , \, \overline{\wtv{a}} \text{ fresh} } + \end{array}\\ + \mathbf{in} & \consSet_R \cup \overline{\consSet} \cup \constraint + \end{array} + \end{array} +\end{displaymath} + +\begin{displaymath} +\begin{array}{@{}l@{}l} + \typeExpr{} & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a} ) = \\ + & \begin{array}{ll} + \textbf{let} + & \tv{r}, \ol{\tv{r}} \text{ fresh} \\ + & \consSet_R = \typeExpr(({\mtypeEnvironment} ; + \overline{\localVarAssumption}), \texttt{e}, \tv{r})\\ + & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \ol{e}, \ol{\tv{r}}) \\ + & \begin{array}{@{}l@{}l} + \constraint = \orCons\set{ & + \begin{array}[t]{l} + [\overline{\wtv{a}}/\ol{Y}] [\overline{\wtv{b}}/\ol{X}] \{ \tv{r} \lessdot \exptype{C}{\ol{X}}, + \overline{\tv{r}} \lessdot \ol{T}, + \type{T} \lessdot \tv{a}, + \overline{\wtv{a}} \lessdot \ol{N}, + \overline{\wtv{b}} \lessdot \ol{N'} \} + \end{array}\\ + & \ |\ + (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T}) \in + {\mtypeEnvironment} + , \, \overline{\wtv{a}} \text{ fresh}, \, \overline{\wtv{b}} \text{ fresh} } + \end{array}\\ + \mathbf{in} & \consSet_R \cup \overline{\consSet} \cup \constraint + \end{array} + \end{array} +\end{displaymath} +\\[1em] +\noindent +\textbf{Example:} +\begin{verbatim} +class Class1{ + X m(List lx, List lt){ ... } + List wGet(){ ... } + List get() { ... } +} + +class Class2{ + example(c1){ + return c1.m(c1.get(), c1.wGet()); + } +} +\end{verbatim} +%This example comes with predefined type annotations. +We assume the class \texttt{Class1} has already been processed by our type inference algorithm, +which has lead to the given type annotations for \texttt{Class1}. +Now we call the $\fjtype{}$ function with the class \texttt{Class2} and the method assumptions for the preceeding class: +\begin{displaymath} +\mtypeEnvironment = \left\{\begin{array}{l} + \type{Class1}.\texttt{m}: \generics{\type{X} \triangleleft \type{Object}} \ + (\exptype{List}{\type{X}}, \, \wctype{\wildcard{A}{\type{X}}{\bot}}{List}{\wildcard{A}{\type{X}}{\bot}}) \to \type{X}, \\ + \type{Class1}.\texttt{wGet}: () \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\wildcard{A}{\type{Object}}{\type{String}}}, \\ + \type{Class1}.\texttt{get}: () \to \exptype{List}{\type{String}} +\end{array} \right\} +\end{displaymath} + +The result of the $\typeExpr{}$ function is the constraint set +\begin{displaymath} +C = \left\{ \begin{array}{l} +\tv{c1} \lessdot \type{Class1}, \\ +\tv{p1} \lessdot \exptype{List}{\wtv{x}}, \\ +\exptype{List}{\type{String}} \lessdot \tv{p1}, \\ +\tv{p2} \lessdot \wctype{\wildcard{A}{\wtv{x}}{\bot}}{List}{\rwildcard{A}}, \\ +\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{p2} +\end{array} \right\} +\end{displaymath} + + +The first parameter of a method assumption is the receiver type $\type{T}_r$. +\texttt{Class1} for this example. +Therefore the $(\tv{c1} \lessdot \type{Class1})$ constraint. +The type variable $\tv{c1}$ is assigned to the parameter \texttt{c1} of the \texttt{example} method. + +or a simplified version: + +\begin{displaymath} +C = \left\{ \begin{array}{l} +\tv{c1} \lessdot \type{Class1}, \\ +\exptype{List}{\type{String}} + \lessdot \exptype{List}{\wtv{x}}, \\ +\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} + \lessdot \wctype{\wildcard{A}{\wtv{x}}{\bot}}{List}{\rwildcard{A}} +\end{array} \right\} +\end{displaymath} + + +$\wtv{x}$ is a type variable we use for the generic $\type{X}$. It is flagged as a free type variable. +%TODO: Do an example where wildcards are inserted and we need capture conversion +%\unify{} returns the solution $(\sigma = \set{ \tv{x} \to \type{String} })$ + +% \\[1em] +% \noindent +% \textbf{Example:} +% \begin{verbatim} +% class Class1 { +% Pair make(List l){ ... } +% boolean compare(Pair p) { ... } + +% example(l){ +% return compare(make(l)); +% } +% } +% \end{verbatim} + +% The method call \texttt{make(l)} generates the constraints +% \begin{displaymath} +% \tv{l} \lessdot \exptype{List}{\tv{x}}, \exptype{Pair}{\tv{x}, \tv{x}} \lessdot \tv{m} +% \end{displaymath} +% with $\tv{l}$ being the type placeholder for the variable \texttt{l} +% and $\tv{m}$ is the type variable for the return type of the method call. +% $\tv{m}$ is then used as the parameter for the \texttt{compare} method: +% \begin{displaymath} +% \tv{m} \lessdot \exptype{Pair}{\tv{y}, \tv{y}} +% \end{displaymath} +% Note the conversion of the generic parameters \texttt{X} and \texttt{Y} to type variables $\tv{x}$ and $\tv{y}$. + + + +% Step 3 of the \unify{} algorithm has to look for every possible supertype of $\exptype{Pair}{\tv{x}, \tv{x}}$, +% when processing the $\exptype{Pair}{\tv{x}, \tv{x}} \lessdot \tv{m}$ constraint. + +\begin{displaymath} + \begin{array}{@{}l@{}l} + \typeExpr{} &({\mtypeEnvironment} , e_1 \elvis{} e_2, \tv{a}) = \\ + & \begin{array}{ll} + \textbf{let} + & \tv{r}_1, \tv{r}_2 \ \text{fresh} \\ + & \consSet_1 = \typeExpr({\mtypeEnvironment}, e_1, \tv{r}_2)\\ + & \consSet_2 = \typeExpr({\mtypeEnvironment}, e_2, \tv{r}_2)\\ + {\mathbf{in}} & { + \consSet_1 \cup \consSet_2 \cup + \set{\tv{r}_1 \lessdot \tv{a}, \tv{r}_2 \lessdot \tv{a}}} + \end{array} + \end{array} +\end{displaymath} + +%We could skip wfresh here: +\begin{displaymath} + \begin{array}{@{}l@{}l} + \typeExpr{} &({\mtypeEnvironment} , x, \tv{a}) = + \mtypeEnvironment(x) + \end{array} +\end{displaymath} + +\begin{displaymath} + \begin{array}{@{}l@{}l} + \typeExpr{} &({\mtypeEnvironment} , \texttt{new}\ \type{C}(\overline{e}), \tv{a}) = \\ + & \begin{array}{ll} + \textbf{let} + & \ol{\tv{r}} \ \text{fresh} \\ + & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \overline{e}, \ol{\tv{r}}) \\ + & C = \set{\ol{\tv{r}} \lessdot [\ol{\tv{a}}/\ol{X}]\ol{T}, \ol{\tv{a}} \lessdot \ol{N} \mid \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}} \\ + {\mathbf{in}} & { + \overline{\consSet} \cup + \set{\tv{a} \doteq \exptype{C}{\ol{a}}}} + \end{array} + \end{array} +\end{displaymath} + +% Problem: +% > void t2(List l){} + +% void test(List> l){ +% t2(l); +% } +% Problem: +% List> <. List, a <. List +% Y.List =. a +% Z.List <. List + +% These constraints should fail! + +\section{Result Generation} +If \unify{} returns atleast one type solution $(\Delta, \sigma)$ +the last step of the type inference algorithm is to generate a typed class. diff --git a/introduction.tex b/introduction.tex new file mode 100644 index 0000000..ca5c1a5 --- /dev/null +++ b/introduction.tex @@ -0,0 +1,222 @@ + +\section{Type Inference for Java} +%The goal is to find a correct typing for a given Java program. +Type inference for Java has many use cases and could be used to help programmers by inserting correct types for them, +Finding better type solutions for already typed Java programs (for example more generical ones), +or allowing to write typeless Java code which is then type infered and thereby type checked by our algorithm. +The algorithm proposed in this paper can determine a correct typing for the untyped Java source code example shown in figure \ref{fig:intro-example-typeless}. +Our algorithm is also capable of finding solutions involving wildcards as shown in figure \ref{fig:intro-example-typed}. + +This paper extends a type inference algorithm for Featherweight Java (\cite{TIforFGJ}) by adding wildcards. +The last step to create a type inference algorithm compatible to the Java type system. +The algorithm is a modified version of the \unify{} algorithm presented in \cite{plue09_1}. + +%TODO +% The goal is to proof soundness in respect to the type rules introduced by \cite{aModelForJavaWithWildcards} +% and \cite{WildcardsNeedWitnessProtection}. + +\begin{figure}[tp] + \begin{subfigure}[t]{0.49\linewidth} + \begin{lstlisting}[style=fgj] +genList() { + if( ... ) { + return new List(); + } else { + return new List(); + } +} + \end{lstlisting} + \caption{Java method with missing return type} + \label{fig:intro-example-typeless} + \end{subfigure} + ~ + \begin{subfigure}[t]{0.49\linewidth} + \begin{lstlisting}[style=tfgj] +List genList() { + if( ... ) { + return new List(); + } else { + return new List(); + } +} + \end{lstlisting} + \caption{Correct type} + \label{fig:intro-example-typed} + \end{subfigure} + %\caption{Example code} + %\label{fig:intro-example-code} + \end{figure} + +% \subsection{Wildcards} +% Java subtyping involving generics is invariant. +% For example \texttt{List} is not a subtype of \texttt{List}. +% %Wildcards introduce variance by allowing \texttt{List} to be a subtype of \texttt{List}. + +% \texttt{List} is not a valid return type for the method \texttt{genList}. +% The type inference algorithm has to find the correct type involving wildcards (\texttt{List}). + +\subsection{Java Wildcards} +Wildcards add variance to Java type parameters. +In Java a \texttt{List} is not a subtype of \texttt{List} +even though it seems intuitive with \texttt{String} being a subtype of \texttt{Object}. +Here wildcards come into play. + +$\exptype{List}{String} <: \wctype{\wildcard{X}{\bot}{\type{Object}}}{List}{\rwildcard{X}}$ +means \texttt{List} is a subtype of \texttt{List}. +The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound at the same time, +and a type they are bound to. +In this case the name is $\rwildcard{X}$ and it's bound to the the type \texttt{List}. +% Additionally they can hold a upper or lower bound restriction like \texttt{List}. +% Our representation of this type is: $\wctype{\wildcard{X}{\type{String}}{\type{Object}}}{List}{\rwildcard{X}}$ +% Every wildcard has a name ($\rwildcard{X}$ in this case) and an upper and lower bound (respectively \texttt{Object} and \texttt{String}). + + +\subsection{Constraints} + +Constraints consist of normal types and type variables: + +$\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}$ + +\noindent +Those two constraints imply that we have to find a type replacement for type variable $\tv{a}$, +which is a supertype of $\exptype{List}{String}$ aswell as $\exptype{List}{Integer}$. +This paper describes a \unify{} algorithm to solve these constraints and calculate a type solution $\sigma$. +For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$. + +\subsection{Challenges}\label{challenges} +The introduction of wildcards adds additional challenges. +% we cannot replace every type variable with a wildcard +Type variables can also be used as type parameters, for example +$\exptype{List}{String} \lessdot \exptype{List}{\tv{a}}$. +A problem arises when replacing type variables with wildcards. + +% Wildcards are not reflexive. +% ( on the equals property ), every wildcard has to be capture converted when leaving its scope + +% do not substitute free type variables + +Lets have a look at two examples: +\begin{itemize} +\item \begin{example} \label{intro-example1} +The first one is a valid Java program. +The type \texttt{List} is \textit{capture converted} to a fresh type variable $\rwildcard{X}$ +which is used as the generic method parameter \texttt{A}. + +Java uses capture conversion to replace the generic \texttt{A} by a capture converted version of the +\texttt{? super String} wildcard. +Knowing that the type \texttt{String} is a subtype of any type the wildcard \texttt{? super String} can inherit +it is safe to pass \texttt{"String"} for the first parameter of the function. + +\begin{verbatim} + List add(A a, List la) {} + + List list = ...; + add("String", list); +\end{verbatim} +The constraints representing this code snippet are: + +\begin{displaymath} + \type{String} \lessdot \wtv{a},\, +\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}} +\end{displaymath} + +Here $\sigma(\tv{a}) = \rwildcard{X}$ is a valid solution. +\end{example} + +\item \begin{example}\label{intro-example2} +This example displays an incorrect Java program. +The method call to \texttt{concat} with two wildcard lists is unsound. +Each list could be of a different kind and therefore the \texttt{concat} cannot succeed. +\begin{verbatim} + List concat(List l1, List l2) {} + + List list = ... ; + concat(list, list); +\end{verbatim} +The constraints for this example are: + +$\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}, \\ +\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ +%$\exptype{List}{?} \lessdot \exptype{List}{\tv{a}}, +%\exptype{List}{?} \lessdot \exptype{List}{\tv{a}}$ + +Remember that the given constraints cannot have a valid solution. +%This is due to the fact that the wildcard variables cannot leave their scope. +In this example the \unify{} algorithm should not replace $\tv{a}$ with the captured wildcard $\rwildcard{X}$. +\end{example} + +\end{itemize} + +The \unify{} algorithm only sees the constraints with no information about the program they originated from. +The main challenge was to find an algorithm which computes $\sigma(\tv{a}) = \rwildcard{X}$ for example \ref{intro-example1} but not for example \ref{intro-example2}. +% Solution: A type variable can only take one type and not a wildcard type. + % A wildcard type is only treated like a wildcard while his definition is in scope (during the reduce rule) + + + + +% \subsection{Capture Conversion} +% \begin{verbatim} +% List add(A a, List la) {} + +% List list = ...; + +% add("String", list); +% \end{verbatim} +% The constraints representig this code snippet are: +% $\type{String} \lessdot \tv{a}, +% \wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\tv{a}}$ +% Under the hood the typechecker has to find a replacement for the generic method parameter \texttt{A}. + +% Java allows a method \texttt{ List add(A a, List la)} to be called with +% \texttt{String} and \texttt{List}. +% A naive approach would be to treat wildcards like any other type and replace \texttt{A} +% with \texttt{? super String}. +% Generating the method type \texttt{List add(? super String a, List la)}. + +% This does not work for a method like +% \texttt{ void merge(List l1, List l2)}. +% It is crucial for this method to be called with two lists of the same type. +% Substituting a wildcard for the generic \texttt{A} leads to +% \texttt{void merge(List l1, List l2)}, +% which is unsound. + +% Capture conversion utilizes the fact that instantiated classes always have an actual type. +% \texttt{new List()} and \texttt{new List()} are +% valid instances. +% \texttt{new List()} is not. +% Every type $\wcNtype{\Delta}{N}$ contains an underlying instance of a type $\type{N}$. +% Knowing this fact allows to make additional assumptions. + +% \wildFJ{} type rules allow for generic parameters to be replaced by wildcard types. +% This is possible because wildcards are split into two parts. +% Their declaration at the environment part $\Delta$ of a type $\wcNtype{\Delta}{N}$ +% and their actual use in the body of the type $\type{N}$. +% Replacing the generic \texttt{A} in the type \texttt{List} +% by a wildcard $\type{X}$ will not generate the type \texttt{List}. +% \texttt{List} is the equivalent of $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\type{X}}$. +% The generated type here is $\exptype{List}{\type{X}}$, which has different subtype properties. +% There is no information about what the type $\exptype{List}{\type{X}}$ actually is. +% It has itself as a subtype and for example a type like $\exptype{ArrayList}{\type{X}}$. + +% A method call for example only works with values, which are correct instances of classes. +% Capture conversion automatically converts wildcard type to a concrete class type, +% which then can be used as a parameter for a method call. + +% In \wildFJ{} this is done via let statements. + +% Written in FJ syntax: $\type{N}$ is a initialized type and +% $\wcNtype{\Delta}{N}$ is a type containing wildcards $\Delta$. + +% It is crucial for the wildcard names to never be used twice. +% Otherwise the members of a list with type $\wctype{\type{X}}{List}{\type{X}}$ and +% a list with type $\wctype{\type{X}}{List}{\type{X}}$ would be the same. $\type{X}$ in fact. + +% The let statement adds wildcards to the environment. +% Those wildcards are not allowed to escape the scope of the let statement. +% Which is a problem for our type inference algorithm. + +% The capture converted version of the type $\wctype{\rwildcard{X}}{Box}{\rwildcard{X}}$ is +% $\exptype{Box}{\rwildcard{X}}$. +% The captured type is only used as an intermediate type during a method call. + diff --git a/lipics-logo-bw.pdf b/lipics-logo-bw.pdf new file mode 100644 index 0000000..26b83d6 Binary files /dev/null and b/lipics-logo-bw.pdf differ diff --git a/lipics-v2021.cls b/lipics-v2021.cls new file mode 100644 index 0000000..9107039 --- /dev/null +++ b/lipics-v2021.cls @@ -0,0 +1,1260 @@ +%% +%% This is file `lipics-v2021.cls'. +%% +%% ----------------------------------------------------------------- +%% Author: Dagstuhl Publishing & le-tex publishing services +%% +%% This file is part of the lipics package for preparing +%% LIPICS articles. +%% +%% Copyright (C) 2021 Schloss Dagstuhl +%% +%% This work may be distributed and/or modified under the +%% conditions of the LaTeX Project Public License, either version 1.3 +%% of this license or (at your option) any later version. +%% The latest version of this license is in +%% http://www.latex-project.org/lppl.txt +%% and version 1.3 or later is part of all distributions of LaTeX +%% version 2005/12/01 or later. +%% +%% This work has the LPPL maintenance status `maintained'. +%% +%% The Current Maintainer of this work is +%% Schloss Dagstuhl (publishing@dagstuhl.de). +%% ----------------------------------------------------------------- +%% +\ProvidesClass{lipics-v2021} + [2023/05/12 v3.1.3 LIPIcs articles] +\NeedsTeXFormat{LaTeX2e}[2015/01/01] +\emergencystretch1em +\advance\hoffset-1in +\advance\voffset-1in +\advance\hoffset2.95mm +\newif\if@nobotseplist \@nobotseplistfalse +\def\@endparenv{% + \addpenalty\@endparpenalty\if@nobotseplist\else\addvspace\@topsepadd\fi\@endpetrue} +\def\@doendpe{% + \@endpetrue + \def\par{\@restorepar + \everypar{}% + \par + \if@nobotseplist + \addvspace\topsep + \addvspace\partopsep + \global\@nobotseplistfalse + \fi + \@endpefalse}% + \everypar{{\setbox\z@\lastbox}% + \everypar{}% + \if@nobotseplist\global\@nobotseplistfalse\fi + \@endpefalse}} +\def\enumerate{% + \ifnum \@enumdepth >\thr@@\@toodeep\else + \advance\@enumdepth\@ne + \edef\@enumctr{enum\romannumeral\the\@enumdepth}% + \expandafter + \list + \csname label\@enumctr\endcsname + {\advance\partopsep\topsep + \topsep\z@\@plus\p@ + \ifnum\@listdepth=\@ne + \labelsep0.72em + \else + \ifnum\@listdepth=\tw@ + \labelsep0.3em + \else + \labelsep0.5em + \fi + \fi + \usecounter\@enumctr\def\makelabel##1{\hss\llap{##1}}}% + \fi} +\def\endenumerate{\ifnum\@listdepth=\@ne\global\@nobotseplisttrue\fi\endlist} +\def\itemize{% + \ifnum \@itemdepth >\thr@@\@toodeep\else + \advance\@itemdepth\@ne + \edef\@itemitem{labelitem\romannumeral\the\@itemdepth}% + \expandafter + \list + \csname\@itemitem\endcsname + {\advance\partopsep\topsep + \topsep\z@\@plus\p@ + \ifnum\@listdepth=\@ne + \labelsep0.83em + \else + \ifnum\@listdepth=\tw@ + \labelsep0.75em + \else + \labelsep0.5em + \fi + \fi + \def\makelabel##1{\hss\llap{##1}}}% + \fi} +\def\enditemize{\ifnum\@listdepth=\@ne\global\@nobotseplisttrue\fi\endlist} +\def\@title{\textcolor{red}{Author: Please provide a title}} +\let\@subtitle\@empty +\def\subtitle#1{\gdef\@subtitle{#1}} +\def\subtitleseperator{: } +\def\@sect#1#2#3#4#5#6[#7]#8{% + \ifnum #2>\c@secnumdepth + \let\@svsec\@empty + \else + \refstepcounter{#1}% + \protected@edef\@svsec{\@seccntformat{#1}\relax}% + \fi + \@tempskipa #5\relax + \ifdim \@tempskipa>\z@ + \begingroup + #6{% + \@hangfrom{\hskip #3\relax + \ifnum #2=1 + \colorbox{lipicsYellow}{\kern0.15em\@svsec\kern0.15em}\quad + \else + \@svsec\quad + \fi}% + \interlinepenalty \@M #8\@@par}% + \endgroup + \csname #1mark\endcsname{#7}% + \addcontentsline{toc}{#1}{% + \ifnum #2>\c@secnumdepth \else + \protect\numberline{\csname the#1\endcsname}% + \fi + #7}% + \else + \def\@svsechd{% + #6{\hskip #3\relax + \@svsec #8}% + \csname #1mark\endcsname{#7}% + \addcontentsline{toc}{#1}{% + \ifnum #2>\c@secnumdepth \else + \protect\numberline{\csname the#1\endcsname}% + \fi + #7}}% + \fi + \@xsect{#5}} +\def\@seccntformat#1{\csname the#1\endcsname} +\def\@biblabel#1{\textcolor{lipicsGray}{\sffamily\bfseries#1}} +\def\EventLogoHeight{25} +\def\copyrightline{% + \ifx\@hideLIPIcs\@undefined + \ifx\@EventLogo\@empty + \else + \setbox\@tempboxa\hbox{\includegraphics[height=\EventLogoHeight\p@]{\@EventLogo}}% + \rlap{\hspace\textwidth\hspace{-\wd\@tempboxa}\hspace{\z@}% + \vtop to\z@{\vskip-0mm\unhbox\@tempboxa\vss}}% + \fi + \scriptsize + \vtop{\hsize\textwidth + \nobreakspace\par + \@Copyright + \ifx\@EventLongTitle\@empty\else\@EventLongTitle.\\\fi + \ifx\@EventEditors\@empty\else + \@Eds: \@EventEditors + ; Article~No.\,\@ArticleNo; pp.\,\@ArticleNo:\thepage--\@ArticleNo:\number\numexpr\getpagerefnumber{TotPages}% + \\ + \fi + \setbox\@tempboxa\hbox{\IfFileExists{lipics-logo-bw.pdf}{\includegraphics[height=14\p@,trim=0 15 0 0]{lipics-logo-bw}}{\includegraphics[height=14\p@, width=62pt]{example-image-plain}}}% + \hspace*{\wd\@tempboxa}\enskip + \href{https://www.dagstuhl.de/lipics/}% + {Leibniz International Proceedings in Informatics}\\ + \smash{\unhbox\@tempboxa}\enskip + \href{https://www.dagstuhl.de}% + {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik, Dagstuhl Publishing, Germany}}% + \fi} +\def\ps@plain{\let\@mkboth\@gobbletwo + \let\@oddhead\@empty + \let\@evenhead\@empty + \let\@evenfoot\copyrightline + \let\@oddfoot\copyrightline} +\def\lipics@opterrshort{Option "\CurrentOption" not supported} +\def\lipics@opterrlong{The option "\CurrentOption" from article.cls is not supported by lipics.cls.} +\DeclareOption{a5paper}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} +\DeclareOption{b5paper}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} +\DeclareOption{legalpaper}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} +\DeclareOption{executivepaper}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} +\DeclareOption{landscape}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} +\DeclareOption{10pt}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} +\DeclareOption{11pt}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} +\DeclareOption{12pt}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} +\DeclareOption{oneside}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} +\DeclareOption{twoside}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} +\DeclareOption{titlepage}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} +\DeclareOption{notitlepage}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} +\DeclareOption{onecolumn}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} +\DeclareOption{twocolumn}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} +\DeclareOption{fleqn}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} +\DeclareOption{openbib}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} +\DeclareOption{a4paper}{\PassOptionsToClass{\CurrentOption}{article} + \advance\hoffset-2.95mm + \advance\voffset8.8mm} +\DeclareOption{numberwithinsect}{\let\numberwithinsect\relax} +\DeclareOption{cleveref}{\let\usecleveref\relax} +\DeclareOption{autoref}{\let\useautoref\relax} +\DeclareOption{anonymous}{\let\authoranonymous\relax} +\DeclareOption{thm-restate}{\let\usethmrestate\relax} +\DeclareOption{authorcolumns}{\let\authorcolumns\relax} +\let\compactauthor\relax +\DeclareOption{oldauthorstyle}{\let\compactauthor\@empty} +\DeclareOption{compactauthor}{\let\compactauthor\relax} +\DeclareOption{pdfa}{\let\pdfa\relax} +\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}} +\ProcessOptions +\LoadClass[twoside,notitlepage,fleqn]{article} +\renewcommand\normalsize{% + \@setfontsize\normalsize\@xpt{13}% + \abovedisplayskip 10\p@ \@plus2\p@ \@minus5\p@ + \abovedisplayshortskip \z@ \@plus3\p@ + \belowdisplayshortskip 6\p@ \@plus3\p@ \@minus3\p@ + \belowdisplayskip \abovedisplayskip + \let\@listi\@listI} +\normalsize +\renewcommand\small{% + \@setfontsize\small\@ixpt{11.5}% + \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@ + \abovedisplayshortskip \z@ \@plus2\p@ + \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@ + \def\@listi{\leftmargin\leftmargini + \topsep 4\p@ \@plus2\p@ \@minus2\p@ + \parsep 2\p@ \@plus\p@ \@minus\p@ + \itemsep \parsep}% + \belowdisplayskip \abovedisplayskip +} +\renewcommand\footnotesize{% + \@setfontsize\footnotesize{8.5}{9.5}% + \abovedisplayskip 6\p@ \@plus2\p@ \@minus4\p@ + \abovedisplayshortskip \z@ \@plus\p@ + \belowdisplayshortskip 3\p@ \@plus\p@ \@minus2\p@ + \def\@listi{\leftmargin\leftmargini + \topsep 3\p@ \@plus\p@ \@minus\p@ + \parsep 2\p@ \@plus\p@ \@minus\p@ + \itemsep \parsep}% + \belowdisplayskip \abovedisplayskip +} +\renewcommand\large{\@setfontsize\large{10.5}{13}} +\renewcommand\Large{\@setfontsize\Large{12}{14}} +\setlength\parindent{1.5em} +\setlength\headheight{3mm} +\setlength\headsep {10mm} +\setlength\footskip{3mm} +\setlength\textwidth{140mm} +\setlength\textheight{222mm} +\setlength\oddsidemargin{32mm} +\setlength\evensidemargin{38mm} +\setlength\marginparwidth{25mm} +\setlength\topmargin{13mm} +\setlength{\skip\footins}{2\baselineskip \@plus 4\p@ \@minus 2\p@} +\def\@listi{\leftmargin\leftmargini + \parsep\z@ \@plus\p@ + \topsep 8\p@ \@plus2\p@ \@minus4\p@ + \itemsep \parsep} +\let\@listI\@listi +\@listi +\def\@listii {\leftmargin\leftmarginii + \labelwidth\leftmarginii + \advance\labelwidth-\labelsep + \topsep 4\p@ \@plus2\p@ \@minus\p@ + \parsep\z@ \@plus\p@ + \itemsep \parsep} +\def\@listiii{\leftmargin\leftmarginiii + \labelwidth\leftmarginiii + \advance\labelwidth-\labelsep + \topsep 2\p@ \@plus\p@\@minus\p@ + \parsep \z@ + \partopsep \p@ \@plus\z@ \@minus\p@ + \itemsep \z@ \@plus\p@} +\def\ps@headings{% + \def\@evenhead{\large\sffamily\bfseries + \llap{\hbox to0.5\oddsidemargin{ \ifx\@hideLIPIcs\@undefined\ifx\@ArticleNo\@empty\textcolor{red}{XX}\else\@ArticleNo\fi:\fi\thepage\hss}}\leftmark\hfil}% + \def\@oddhead{\large\sffamily\bfseries\rightmark\hfil + \rlap{\hbox to0.5\oddsidemargin{\hss \ifx\@hideLIPIcs\@undefined\ifx\@ArticleNo\@empty\textcolor{red}{XX}\else\@ArticleNo\fi:\fi\thepage}}}% + \def\@oddfoot{\hfil + \rlap{% + \vtop{% + \vskip10mm + \colorbox{lipicsYellow} + {\@tempdima\evensidemargin + \advance\@tempdima1in + \advance\@tempdima\hoffset + \hb@xt@\@tempdima{% + \ifx\@hideLIPIcs\@undefined + \textcolor{lipicsGray}{\normalsize\sffamily + \bfseries\quad + \expandafter\textsolittle + \expandafter{\@EventShortTitle}}% + \fi + \strut\hss}}}}} + \let\@evenfoot\@empty + \let\@mkboth\markboth + \let\sectionmark\@gobble + \let\subsectionmark\@gobble} +\pagestyle{headings} +\renewcommand\maketitle{\par + \begingroup + \thispagestyle{plain} + \renewcommand\thefootnote{\@fnsymbol\c@footnote}% + \if@twocolumn + \ifnum \col@number=\@ne + \@maketitle + \else + \twocolumn[\@maketitle]% + \fi + \else + \newpage + \global\@topnum\z@ % Prevents figures from going at top of page. + \@maketitle + \fi + \thispagestyle{plain}\@thanks + \endgroup + \global\let\thanks\relax + \global\let\maketitle\relax + \global\let\@maketitle\relax + \global\let\@thanks\@empty + \global\let\@author\@empty + \global\let\@date\@empty + \global\let\@title\@empty + \global\let\@subtitle\@empty + \global\let\title\relax + \global\let\author\relax + \global\let\date\relax + \global\let\and\relax +} +\newwrite\tocfile +\def\@maketitle{% + \newpage + \null\vskip-\baselineskip + \vskip-\headsep + \@titlerunning + \@authorrunning + %%\let \footnote \thanks + \parindent\z@ \raggedright + \if!\@title!\def\@title{\textcolor{red}{Author: Please fill in a title}}\fi + {\LARGE\sffamily\bfseries\mathversion{bold}\@title \if!\@subtitle!\else{\\\Large\sffamily\bfseries\mathversion{bold}\@subtitle}\fi \par}% + \vskip 1em + \ifx\@author\orig@author + \textcolor{red}{Author: Please provide author information}% + \else + {\def\thefootnote{\@arabic\c@footnote}% + \setcounter{footnote}{0}% + \fontsize{9.5}{12}\selectfont\@author}% + \fi + \bgroup + \immediate\openout\tocfile=\jobname.vtc + \protected@write\tocfile{ + \let\footnote\@gobble + \let\thanks\@gobble + \def\footnotemark{} + \def\and{and }% + \def\,{ } + \def\\{ } + }{% + \string\contitem + \string\title{\@title \if!\@subtitle!\else\subtitleseperator \@subtitle\fi}% + \string\author{\@authorsfortoc}% + \string\page{\@ArticleNo:\thepage--\@ArticleNo:\number\numexpr\getpagerefnumber{TotPages}}}% + \closeout\tocfile + \egroup + \par} +\renewcommand\tableofcontents{% + \section*{\contentsname}% + \@starttoc{toc}} +\setcounter{secnumdepth}{4} +\renewcommand\section{\@startsection {section}{1}{\z@}% + {-3.5ex \@plus -1ex \@minus -.2ex}% + {2.3ex \@plus.2ex}% + {\sffamily\Large\bfseries\raggedright}} +\renewcommand\subsection{\@startsection{subsection}{2}{\z@}% + {-3.25ex\@plus -1ex \@minus -.2ex}% + {1.5ex \@plus .2ex}% + {\sffamily\Large\bfseries\raggedright}} +\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}% + {-3.25ex\@plus -1ex \@minus -.2ex}% + {1.5ex \@plus .2ex}% + {\sffamily\Large\bfseries\raggedright}} +\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}% + {-3.25ex \@plus-1ex \@minus-.2ex}% + {1.5ex \@plus .2ex}% + {\sffamily\large\bfseries\raggedright}} +\renewcommand\subparagraph{\@startsection{subparagraph}{5}{\z@}% + {3.25ex \@plus1ex \@minus .2ex}% + {-1em}% + {\sffamily\normalsize\bfseries}} +\newcommand{\proofsubparagraph}{\@startsection{subparagraph}{5}{\z@}% + {3.25ex \@plus1ex \@minus .2ex}% + {-1em}% + {\color{lipicsGray}\sffamily\normalsize\bfseries}} +\setlength\leftmargini \parindent +\setlength\leftmarginii {1.2em} +\setlength\leftmarginiii{1.2em} +\setlength\leftmarginiv {1.2em} +\setlength\leftmarginv {1.2em} +\setlength\leftmarginvi {1.2em} +\renewcommand\labelenumi{% + \textcolor{lipicsGray}{\sffamily\bfseries\upshape\mathversion{bold}\theenumi.}} +\renewcommand\labelenumii{% + \textcolor{lipicsGray}{\sffamily\bfseries\upshape\mathversion{bold}\theenumii.}} +\renewcommand\labelenumiii{% + \textcolor{lipicsGray}{\sffamily\bfseries\upshape\mathversion{bold}\theenumiii.}} +\renewcommand\labelenumiv{% + \textcolor{lipicsGray}{\sffamily\bfseries\upshape\mathversion{bold}\theenumiv.}} +\renewcommand\labelitemi{% + \textcolor{lipicsBulletGray}{\ifnum\@listdepth=\@ne + \rule{0.67em}{0.33em}% + \else + \rule{0.45em}{0.225em}% + \fi}} +\renewcommand\labelitemii{% + \textcolor{lipicsBulletGray}{\rule{0.45em}{0.225em}}} +\renewcommand\labelitemiii{% + \textcolor{lipicsBulletGray}{\sffamily\bfseries\textasteriskcentered}} +\renewcommand\labelitemiv{% + \textcolor{lipicsBulletGray}{\sffamily\bfseries\textperiodcentered}} +\renewenvironment{description} + {\list{}{\advance\partopsep\topsep\topsep\z@\@plus\p@ + \labelwidth\z@ \itemindent-\leftmargin + \let\makelabel\descriptionlabel}} + {\ifnum\@listdepth=\@ne\global\@nobotseplisttrue\fi\endlist} +\renewcommand*\descriptionlabel[1]{% + \hspace\labelsep\textcolor{lipicsGray}{\sffamily\bfseries\mathversion{bold}#1}} +\def\topmattervskip{0.7} +\renewenvironment{abstract}{% + \vskip\topmattervskip\bigskipamount + \noindent + \rlap{\color{lipicsLineGray}\vrule\@width\textwidth\@height1\p@}% + \hspace*{7mm}\fboxsep1.5mm\colorbox[rgb]{1,1,1}{\raisebox{-0.4ex}{% + \large\selectfont\sffamily\bfseries\abstractname}}% + \vskip3\p@ + \fontsize{9}{12}\selectfont + \noindent\ignorespaces} + {\vskip\topmattervskip\baselineskip\noindent + \subjclassHeading + \ifx\@ccsdescString\@empty + \textcolor{red}{Author: Please fill in 1 or more \string\ccsdesc\space macro}% + \else + \@ccsdescString + \fi + \vskip\topmattervskip\baselineskip + \noindent\keywordsHeading + \ifx\@keywords\@empty + \textcolor{red}{Author: Please fill in \string\keywords\space macro}% + \else + \@keywords + \fi + \ifx\@hideLIPIcs\@undefined + \ifx\@DOIPrefix\@empty\else + \vskip\topmattervskip\baselineskip\noindent + \doiHeading\href{https://doi.org/\@lipicsdoi}{\@lipicsdoi}% + \fi + \fi + \ifx\@category\@empty\else + \vskip\topmattervskip\baselineskip\noindent + \categoryHeading\@category + \fi + \ifx\@relatedversion\@empty\else + \vskip\topmattervskip\baselineskip\noindent + \relatedversionHeading\ifx\authoranonymous\relax\textcolor{red}{Anonymous related version(s)}\else\@relatedversion\fi + \fi + \ifx\@supplement\@empty\else + \vskip\topmattervskip\baselineskip\noindent + \supplementHeading\ifx\authoranonymous\relax\textcolor{red}{Anonymous supplementary material}\else\@supplement\fi + \fi + \ifx\@funding\@empty\else + \vskip\topmattervskip\baselineskip\noindent + \fundingHeading\ifx\authoranonymous\relax\textcolor{red}{Anonymous funding}\else\@funding\fi + \fi + \ifx\@acknowledgements\@empty\else + \vskip\topmattervskip\baselineskip\noindent + \acknowledgementsHeading\ifx\authoranonymous\relax\textcolor{red}{Anonymous acknowledgements} \else\@acknowledgements\fi + \fi + \protected@write\@auxout{}{\string\gdef\string\@pageNumberEndAbstract{\thepage}}% + }% end abstract +\renewenvironment{thebibliography}[1] + {\if@noskipsec \leavevmode \fi + \par + \@tempskipa-3.5ex \@plus -1ex \@minus -.2ex\relax + \@afterindenttrue + \@tempskipa -\@tempskipa \@afterindentfalse + \if@nobreak + \everypar{}% + \else + \addpenalty\@secpenalty\addvspace\@tempskipa + \fi + \noindent + \rlap{\color{lipicsLineGray}\vrule\@width\textwidth\@height1\p@}% + \hspace*{7mm}\fboxsep1.5mm\colorbox[rgb]{1,1,1}{\raisebox{-0.4ex}{% + \normalsize\sffamily\bfseries\refname}}% + \@xsect{1ex \@plus.2ex}% + \list{\@biblabel{\@arabic\c@enumiv}}% + {\leftmargin8.5mm + \labelsep\leftmargin + \settowidth\labelwidth{\@biblabel{#1}}% + \advance\labelsep-\labelwidth + \usecounter{enumiv}% + \let\p@enumiv\@empty + \renewcommand\theenumiv{\@arabic\c@enumiv}}% + \fontsize{9}{12}\selectfont + \sloppy + \clubpenalty4000 + \@clubpenalty \clubpenalty + \widowpenalty4000% + \sfcode`\.\@m\protected@write\@auxout{}{\string\gdef\string\@pageNumberStartBibliography{\thepage}}} + {\def\@noitemerr + {\@latex@warning{Empty `thebibliography' environment}}% + \protected@write\@auxout{}{\string\gdef\string\@pageNumberEndBibliography{\thepage}}% + \endlist} +\g@addto@macro\appendix{\immediate\write\@auxout{\string\gdef\string\@pageNumberStartAppendix{\thepage}}}% +\renewcommand\footnoterule{% + \kern-8\p@ + {\color{lipicsBulletGray}\hrule\@width40mm\@height1\p@}% + \kern6.6\p@} +\renewcommand\@makefntext[1]{% + \parindent\z@\hangindent1em + \leavevmode + \hb@xt@1em{\@makefnmark\hss}#1} +\usepackage{microtype} +\usepackage[utf8]{inputenc} +\ifx\pdfa\relax% + \IfFileExists{glyphtounicode.tex}{ + \input glyphtounicode + \pdfgentounicode=1 + }{}% +\fi +\IfFileExists{lmodern.sty}{\RequirePackage{lmodern}}{} +\IfFileExists{fontawesome5.sty}{% +\RequirePackage{fontawesome5}% +\IfFileExists{orcid.pdf}{% +\def\orcidsymbol{\includegraphics[height=9\p@]{orcid}} +}{ +\def\orcidsymbol{\textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries \faOrcid}}% +} +\def\mailsymbol{\textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries \faIcon[regular]{envelope}}}% +\def\homesymbol{\textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries \faHome}}% +}{% +\ClassWarning{Package fontawesome5 not installed}{Please install package fontawesome5} +\def\orcidsymbol{\textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries ORCID}} +\def\mailsymbol{\textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries @}}% +\def\homesymbol{\textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries H}}% +}% +\RequirePackage[T1]{fontenc} +\RequirePackage{textcomp} +\RequirePackage[mathscr]{eucal} +\RequirePackage{amssymb} +\PassOptionsToPackage{retainmissing}{MnSymbol} +\AtBeginDocument{\@ifpackageloaded{MnSymbol}% + {\expandafter\let\csname ver@amssymb.sty\endcsname\relax + \let\complement\@undefined + \RequirePackage{amssymb}}{}} +\RequirePackage{soul} +\sodef\textsolittle{}{.12em}{.5em\@plus.08em\@minus.06em}% + {.4em\@plus.275em\@minus.183em} +\RequirePackage{color} %kept for backward compatibility +\AtBeginDocument{ + \@ifpackageloaded{xcolor}{ + }{ + \RequirePackage{xcolor} + } + \definecolor{darkgray}{rgb}{0.31,0.31,0.33} + \definecolor[named]{lipicsGray}{rgb}{0.31,0.31,0.33} + \definecolor[named]{lipicsBulletGray}{rgb}{0.60,0.60,0.61} + \definecolor[named]{lipicsLineGray}{rgb}{0.51,0.50,0.52} + \definecolor[named]{lipicsLightGray}{rgb}{0.85,0.85,0.86} + \definecolor[named]{lipicsYellow}{rgb}{0.99,0.78,0.07} +} +\RequirePackage{babel} +\RequirePackage[tbtags,fleqn]{amsmath} +\AtBeginDocument{ + \@ifpackageloaded{enumitem}{\ClassWarning{Package 'enumitem' incompatible}{Don't use package 'enumitem'; Package enumerate preloaded!}}{} + \@ifpackageloaded{paralist}{\ClassWarning{Package 'paralist' incompatible}{Don't use package 'paralist'; Package enumerate preloaded!}}{} +} +\RequirePackage{enumerate} +\def\@enum@{\list{\textcolor{lipicsGray}{\sffamily\bfseries\upshape\mathversion{bold}\csname label\@enumctr\endcsname}}% + {\advance\partopsep\topsep + \topsep\z@\@plus\p@ + \usecounter{\@enumctr}\def\makelabel##1{\hss\llap{##1}}}} +\def\romanenumerate{\enumerate[(i)]} +\let\endromanenumerate\endenumerate +\def\alphaenumerate{\enumerate[(a)]} +\let\endalphaenumerate\endenumerate +\def\bracketenumerate{\enumerate[(1)]} +\let\endbracketenumerate\endenumerate +\RequirePackage{graphicx} +\RequirePackage{array} +\let\@classzold\@classz +\def\@classz{% + \expandafter\ifx\d@llarbegin\begingroup + \toks \count@ = + \expandafter{\expandafter\small\the\toks\count@}% + \fi + \@classzold} +\RequirePackage{multirow} +\RequirePackage{tabularx} +\RequirePackage[online]{threeparttable} +\def\TPTtagStyle#1{#1)} +\def\tablenotes{\small\TPT@defaults + \@ifnextchar[\TPT@setuptnotes\TPTdoTablenotes} % ] +\RequirePackage{listings} +\lstset{basicstyle=\small\ttfamily,% + backgroundcolor=\color{lipicsLightGray},% + frame=single,framerule=0pt,xleftmargin=\fboxsep,xrightmargin=\fboxsep} +\RequirePackage[left,mathlines]{lineno} +\linenumbers +\renewcommand\linenumberfont{\normalfont\tiny\sffamily} +%%%% patch to cope with amsmath +%%%% http://phaseportrait.blogspot.de/2007/08/lineno-and-amsmath-compatibility.html +\newcommand*\patchAmsMathEnvironmentForLineno[1]{% + \expandafter\let\csname old#1\expandafter\endcsname\csname #1\endcsname + \expandafter\let\csname oldend#1\expandafter\endcsname\csname end#1\endcsname + \renewenvironment{#1}% + {\linenomath\csname old#1\endcsname}% + {\csname oldend#1\endcsname\endlinenomath}}% +\newcommand*\patchBothAmsMathEnvironmentsForLineno[1]{% + \patchAmsMathEnvironmentForLineno{#1}% + \patchAmsMathEnvironmentForLineno{#1*}}% +\AtBeginDocument{% + \patchBothAmsMathEnvironmentsForLineno{equation}% + \patchBothAmsMathEnvironmentsForLineno{align}% + \patchBothAmsMathEnvironmentsForLineno{flalign}% + \patchBothAmsMathEnvironmentsForLineno{alignat}% + \patchBothAmsMathEnvironmentsForLineno{gather}% + \patchBothAmsMathEnvironmentsForLineno{multline}} +\ifx\pdfa\relax% + \RequirePackage[pdfa,unicode]{hyperref}% +\else% + \RequirePackage[unicode]{hyperref}% +\fi% +\let\usehyperxmp\@empty% +\ifx\pdfa\relax% + \IfFileExists{hyperxmp.sty}{% + \RequirePackage{hyperxmp}% + \@ifpackagelater{hyperxmp}{2019/04/05}{% + \let\usehyperxmp\relax% + }{% + \ClassWarning{Package hyperxmp outdated}{You are using an outdated version of the package hyperxmp. Please update!}% + }}{}% +\fi% +\IfFileExists{totpages.sty}{ + \RequirePackage{totpages} +}{ + \ClassWarning{Package totpages not installed}{Please install package totpages} + \newcounter{TotPages} + \setcounter{TotPages}{99} +} +\let\C\relax% +\let\G\relax% +\let\F\relax% +\let\U\relax% +\pdfstringdefDisableCommands{% + \let\thanks\@gobble% + \let\footnote\@gobble% + \def\footnotemark{}% + \def\cs#1{\textbackslash #1}% + \let\normalfont\@empty% + \let\scshape\@empty% + \def\and{and }% + \def\,{ }% + \def\textrightarrow{ -> }% + \let\mathsf\@empty% +}% +\hypersetup{ + breaklinks=true, + pdfencoding=unicode, + bookmarksnumbered, + pdfborder={0 0 0}, + pdfauthor={ } +}% +\AtBeginDocument{ +\ifx\usehyperxmp\relax +\hypersetup{ +pdftitle={\@title \if!\@subtitle!\else\subtitleseperator \@subtitle\fi}, +pdfauthor={\ifx\authoranonymous\relax Anonymous author(s) \else \@authorsforpdf \fi}, +pdfkeywords={\@keywords}, +pdfproducer={LaTeX with lipics-v2021.cls}, +pdfsubject={LIPIcs, Vol.\@SeriesVolume, \@EventShortTitle}, +pdfcopyright = { Copyright (C) \ifx\authoranonymous\relax Anonymous author(s) \else \@copyrightholder; \fi licensed under Creative Commons License CC-BY 4.0}, +pdflang={en}, +pdfmetalang={en}, +pdfpublisher={Schloss Dagstuhl -- Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany}, +pdflicenseurl={https://creativecommons.org/licenses/by/4.0/}, +pdfpubtype={LIPIcs}, +pdfvolumenum={\@SeriesVolume}, +pdfpagerange={\@ArticleNo:\thepage-\@ArticleNo:\theTotPages}, +pdfdoi={\@lipicsdoi}, +pdfapart=3, +pdfaconformance=B +} +\else% +\hypersetup{ +pdftitle={\@title \if!\@subtitle!\else\subtitleseperator \@subtitle\fi}, +pdfauthor={\ifx\authoranonymous\relax Anonymous author(s) \else \@authorsforpdf \fi}, +pdfkeywords={\@keywords}, +pdfcreator={LaTeX with lipics-v2021.cls}, +pdfsubject={LIPIcs, Vol.\@SeriesVolume, \@EventShortTitle; Copyright (C) \ifx\authoranonymous\relax Anonymous author(s) \else \@copyrightholder; \fi licensed under Creative Commons License CC-BY 4.0} +}% +\fi % +} +\ifx\usehyperxmp\relax +\pdfobjcompresslevel=0 +\pdfinclusioncopyfonts=1 +\IfFileExists{colorprofiles.tex}{ +\RequirePackage{colorprofiles}% +\IfFileExists{sRGB.icc}{ +\immediate\pdfobj stream attr{/N 3} file{sRGB.icc} +\pdfcatalog{% +/OutputIntents [ +<< +/Type /OutputIntent +/S /GTS_PDFA1 +/DestOutputProfile \the\pdflastobj\space 0 R +/OutputConditionIdentifier (sRGB) +/Info (sRGB) +>> +] +}}{} +}{\ClassWarning{Package colorprofiles not installed}{Please install package colorprofiles}} +\fi +\RequirePackage[labelsep=space,singlelinecheck=false,% + font={up,small},labelfont={sf,bf},% + listof=false]{caption}%"listof" instead of "list" for backward compatibility +\@ifpackagelater{hyperref}{2009/12/09} + {\captionsetup{compatibility=false}}%cf. http://groups.google.de/group/comp.text.tex/browse_thread/thread/db9310eb540fbbd8/42e30f3b7b3aa17a?lnk=raot + {} +\DeclareCaptionLabelFormat{boxed}{% + \kern0.05em{\color[rgb]{0.99,0.78,0.07}\rule{0.73em}{0.73em}}% + \hspace*{0.67em}\bothIfFirst{#1}{~}#2} +\captionsetup{labelformat=boxed} +\captionsetup[table]{position=top} +\RequirePackage[figuresright]{rotating} +\caption@AtBeginDocument{\@ifpackageloaded{subfig}{\ClassError{lipics}{% + Do not load the subfig package}{The more recent subcaption package is already loaded}}{}} +\RequirePackage{subcaption} +\def\titlerunning#1{\gdef\@titlerunning{{\let\footnote\@gobble\markboth{#1}{#1}}}} +\def\authorrunning#1{% + \gdef\@authorrunning{\markright{\ifx\authoranonymous\relax\textcolor{red}{Anonymous author(s)} \else\if!#1!\textcolor{red}{Author: Please fill in the \string\authorrunning\space macro}\else#1\fi\fi}}} +\titlerunning{\@title \if!\@subtitle!\else\subtitleseperator \@subtitle\fi} +\authorrunning{\textcolor{red}{Author: Please use the \string\authorrunning\space macro}} +\def\EventLongTitle#1{\gdef\@EventLongTitle{#1}} +\EventLongTitle{} +\def\EventShortTitle#1{\gdef\@EventShortTitle{#1}} +\EventShortTitle{} +\def\EventEditors#1{\gdef\@EventEditors{#1}} +\EventEditors{} +\def\EventNoEds#1{\gdef\@EventNoEds{#1}\xdef\@Eds{Editor\ifnum#1>1s\fi}} +\EventNoEds{1} +\def\EventLogo#1{\gdef\@EventLogo{#1}} +\EventLogo{} +\def\EventAcronym#1{\gdef\@EventAcronym{#1}} +\EventAcronym{} +\def\EventYear#1{\gdef\@EventYear{#1}} +\EventYear{} +\def\EventDate#1{\gdef\@EventDate{#1}} +\EventDate{} +\def\EventLocation#1{\gdef\@EventLocation{#1}} +\EventLocation{} +\def\SeriesVolume#1{\gdef\@SeriesVolume{#1}} +\SeriesVolume{} +\def\ArticleNo#1{\gdef\@ArticleNo{#1}} +\ArticleNo{} +\def\DOIPrefix#1{\gdef\@DOIPrefix{#1}} +\DOIPrefix{10.4230/LIPIcs} +\def\@lipicsdoi{\@DOIPrefix.\@EventAcronym.\@EventYear.\@ArticleNo} +\def\and{\newline} +\let\orig@author\@author +\let\@authorsfortoc\@empty +\let\@authorsforpdf\@empty +\newcount\c@author +\newcounter{currentauthor} +\def\authorcolumnsMin{6} +\def\@authornum{0} +\def\author#1#2#3#4#5{% + \ifx\@author\orig@author\let\@author\@empty\fi + \g@addto@macro\@author{% + \noexpandarg\StrBehind{#2}{\and \url}[\homepageTemp]\IfSubStr{#2}{\and \url}{\StrBefore{#2}{\and \url}[\affiliation]}{\def\affiliation{#2}}% + \expandarg\exploregroups\StrRemoveBraces{\homepageTemp}[\homepage]% + \ifx\authorcolumns\relax + \ifnum\c@author>\authorcolumnsMin + \stepcounter{currentauthor} + \ifodd\value{currentauthor} + \begin{minipage}[t]{\textwidth} + \begin{minipage}[t]{0.49\textwidth} + \else + \hfill \begin{minipage}[t]{0.49\textwidth} + \fi + \else + \ClassWarning{Option 'authorcolumns' only applicable for > 6 authors}{Option 'authorcolumns' only applicable for >6 authors!} + \addvspace{0.5\baselineskip} + \fi + \else + \addvspace{0.5\baselineskip} + \fi + {\Large\bfseries + \if!#1! + \textcolor{red}{Author: Please enter author name}% + \else + \ifx\authoranonymous\relax + \textcolor{red}{Anonymous author} + \else + #1\,% + \ifx\compactauthor\relax\if!#3!\else{\,\href{mailto:#3}{\mailsymbol}}\fi% + \ifx\homepage\@empty\else{\,\href{\homepage}{\homesymbol}}\fi\fi% + \if!#4!\else{\,\href{#4}{\orcidsymbol}}\fi% + \if!#5!\else + \ifx\@funding\@empty + \expandafter\g@addto@macro\expandafter\@funding{\textit{\expandafter{\let\footnote\@gobble #1}}:\space{#5}} + \else + \expandafter\g@addto@macro\expandafter\@funding{\\\textit{\expandafter{\let\footnote\@gobble #1}}:\space{#5}} + \fi + \fi + \fi + \fi + } + {\small + \if!#2!\textcolor{red}{Author: Please enter affiliation as second parameter of the author macro}\else{\\* \ifx\authoranonymous\relax\textcolor{red}{Anonymous affiliation}\else\ifx\compactauthor\relax \affiliation \else#2\fi\fi}\fi + \ifx\compactauthor\relax\else\if!#3!\else{\ifx\authoranonymous\relax\else\\*\href{mailto:#3}{#3}\fi}\fi\fi + }\par + \ifx\authorcolumns\relax + \ifnum\c@author>\authorcolumnsMin + \end{minipage} + \ifnum\c@author=\value{currentauthor} + \end{minipage} + \else + \ifodd\value{currentauthor} + \else + \end{minipage}% + \medskip + \fi + \fi + \fi + \fi}% + \global\advance\c@author\@ne + \protected@write\@auxout{}{\string\gdef\string\@authornum{\the\c@author}} + \ifnum\c@author=\@ne + \gdef\@authorsfortoc{#1}% + \gdef\@authorsforpdf{#1} + \else + \expandafter\g@addto@macro\expandafter\@authorsforpdf\expandafter{, #1} + \expandafter\g@addto@macro\expandafter\@authorsfortoc\expandafter{\expandafter\csname\the\c@author authand\endcsname#1}% + \@namedef{\the\c@author authand}{,\space}% + \AtBeginDocument{% + \expandafter\ifnum\@authornum=2 + \@namedef{2authand}{\space and\space}% + \else + \@namedef{\@authornum authand}{,\space and\space}% + \fi} + \fi} +\newcommand*\affil[2][]{% + \ClassError{lipics} + {\string\affil\space deprecated: Please enter affiliation as second parameter of the author macro} + {Since 2017, \string\affil\space is obsolete in lipics.}} +\newcommand*\Copyright[1]{% + \def\@copyrightholder{#1} + \def\@Copyright{% + \setbox\@tempboxa\hbox{\IfFileExists{cc-by.pdf}{\includegraphics[height=14\p@,clip]{cc-by}}{\includegraphics[height=14\p@, width=40pt]{example-image-plain}}}% + \@rightskip\@flushglue \rightskip\@rightskip + \hangindent\dimexpr\wd\@tempboxa+0.5em\relax + \href{https://creativecommons.org/licenses/by/4.0/}% + {\smash{\lower\baselineskip\hbox{\unhcopy\@tempboxa}}}\enskip + \textcopyright\ % + \ifx!#1!\textcolor{red}{Author: Please fill in the \string\Copyright\space macro}\else\ifx\authoranonymous\relax\textcolor{red}{Anonymous author(s)}\else#1\fi\fi + ;\\% + licensed under Creative Commons License CC-BY 4.0\ifx!#1!\\\null\fi\par}} +\Copyright{\textcolor{red}{Author: Please provide a copyright holder}} +\let\@copyrightholder\@empty +\def\hideLIPIcs{\let\@hideLIPIcs\relax} +\usepackage{xstring} +\def\keywords#1{\def\@keywords{#1}} +\let\@keywords\@empty +\def\keywordsHeading{% + \textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries + Keywords and phrases\enskip}} +\RequirePackage{comment} +\excludecomment{CCSXML} +% inspired by https://tex.stackexchange.com/questions/12810/how-do-i-split-a-string +\global\newcommand\ccsdesc[2][100]{\@ccsdesc#1~#2~~\relax} +\let\orig@ccsdesc\@ccsdesc +\let\@ccsdesc\@empty +\let\@ccsdescString\@empty +\gdef\@ccsdesc#1~#2~#3~{ + \ifx\@ccsdesc\orig@ccsdesc\let\@ccsdesc\@empty\fi + \ifx!#3! + \ifx\@ccsdescString\@empty + \g@addto@macro\@ccsdescString{{#2}} + \else + \g@addto@macro\@ccsdescString{; {#2}} + \fi + \else + \ifx\@ccsdescString\@empty + \g@addto@macro\@ccsdescString{{#2} $\rightarrow$ {#3}} + \else + \g@addto@macro\@ccsdescString{; {#2} $\rightarrow$ {#3}} + \fi + \fi +\ccsdescEnd +} +\def\ccsdescEnd#1\relax{} +\def\subjclass#1{ + \ClassError{lipics} + {\string\subjclass\space deprecated: Please enter subject classification in 1 or more ccsdesc macros} + {Since 2019, \string\subjclass\space is obsolete in lipics.}} +\let\@subjclass\@empty +\def\subjclassHeading{% + \textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries + 2012 ACM Subject Classification\enskip}} +\def\doiHeading{% + \textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries + Digital Object Identifier\enskip}} +\def\category#1{\def\@category{#1}} +\let\@category\@empty +\def\categoryHeading{% + \textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries + Category\enskip}} +\def\relatedversion#1{\def\@relatedversion{#1}} +\let\@relatedversion\@empty +\define@key{relatedversiondetails}{linktext}{\def\relatedversiondetails@linktext{#1}} +\define@key{relatedversiondetails}{cite}{\def\relatedversiondetails@cite{#1}} +\newcommand*\addtorelatedversionmacro[2]{% + \ifx\@relatedversion\@empty% + \g@addto@macro\@relatedversion{#1}% + \else% + \g@addto@macro\@relatedversion{\\#1}% + \fi% +}% +\newcommand{\relatedversiondetails}[3][]{% + \begingroup% + \let\relatedversiondetails@linktext\@empty + \let\relatedversiondetails@cite\@empty + \setkeys{relatedversiondetails}{#1}% + \ifx\relatedversiondetails@linktext\@empty% + \protected@edef\tmp{\textit{#2}:\space{\url{#3}}}% + \else% + \protected@edef\tmp{\textit{#2}:\space{\href{#3}{\texttt{\relatedversiondetails@linktext}}}}% + \fi% + \ifx\relatedversiondetails@cite\@empty% + \else% + \protected@edef\tmp{\tmp\nobreakspace\cite{\relatedversiondetails@cite}}% + \fi% + \expandafter\addtorelatedversionmacro\expandafter{\tmp}{#1}% + \endgroup% +}% +\def\relatedversionHeading{% + \textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries + Related Version\enskip}} +\def\supplement#1{\def\@supplement{#1}} +\let\@supplement\@empty +\define@key{supplementdetails}{linktext}{\def\supplementdetails@linktext{#1}} +\define@key{supplementdetails}{cite}{\def\supplementdetails@cite{#1}} +\define@key{supplementdetails}{subcategory}{\def\supplementdetails@subcategory{#1}} +\define@key{supplementdetails}{swhlinktext}{\def\supplementdetails@swhlinktext{#1}} +\let\supplementdetails@swhlinktext\@empty +\define@key{supplementdetails}{swhid}{ + \ifx\supplementdetails@swhlinktext\@empty% + \StrBefore{#1}{;}[\supplementdetails@swhlinktext]% + \fi% + \def\supplementdetails@swhid{#1}% +} + +\define@key{supplementdetails}{swhdelimiter}{\def\supplementdetails@swhdelimiter{#1}} +\def\supplementdetails@swhdelimiter{\\ \hspace*{1.2em}} +\newcommand*\addtosupplementmacro[2]{% + \ifx\@supplement\@empty% + \g@addto@macro\@supplement{#1}% + \else% + \g@addto@macro\@supplement{\\#1}% + \fi% +}% +\newcommand{\supplementdetails}[3][]{% + \begingroup% + \let\supplementdetails@linktext\@empty + \let\supplementdetails@cite\@empty + \let\supplementdetails@subcategory\@empty + \let\supplementdetails@swhid\@empty + \setkeys{supplementdetails}{#1}% + \ifx\supplementdetails@subcategory\@empty% + \protected@edef\tmp{\textit{#2}} + \else + \protected@edef\tmp{\textit{#2\,\,(\supplementdetails@subcategory)}}% + \fi + \ifx\supplementdetails@linktext\@empty% + \protected@edef\tmp{\tmp:\space{\url{#3}}}% + \else% + \protected@edef\tmp{\tmp:\space{\href{#3}{\texttt{\supplementdetails@linktext}}}}% + \fi% + \ifx\supplementdetails@cite\@empty% + \else% + \protected@edef\tmp{\tmp\nobreakspace\cite{\supplementdetails@cite}}% + \fi + \ifx\supplementdetails@swhid\@empty% + \else% + \ifx\supplementdetails@swhlinktext\@empty% + \protected@edef\tmp{\tmp \supplementdetails@swhdelimiter{} archived at % + \href{https://archive.softwareheritage.org/\supplementdetails@swhid}{\nolinkurl{\supplementdetails@swhid}}}% + \else% + \protected@edef\tmp{\tmp \supplementdetails@swhdelimiter{} archived at % + \href{https://archive.softwareheritage.org/\supplementdetails@swhid}{\nolinkurl{\supplementdetails@swhlinktext}}}% + \fi% + \fi% + \expandafter\addtosupplementmacro\expandafter{\tmp}{#1}% + \endgroup% +}% +\def\supplementHeading{% + \textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries + Supplementary Material\enskip}} +\newcommand\flag[2][0.9cm]{% + \leavevmode\marginpar{% + \raisebox{\dimexpr-\totalheight+\ht\strutbox\relax}% + [\dimexpr\ht\strutbox+3mm][\dp\strutbox]{\expandafter\includegraphics[width=#1]{#2}}% +}} +\def\funding#1{\def\@funding{#1}} +\let\@funding\@empty +\def\fundingHeading{% + \textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries + Funding\enskip}} +\def\acknowledgements#1{\def\@acknowledgements{#1}} +\let\@acknowledgements\@empty +\def\acknowledgementsHeading{% + \textcolor{lipicsGray}{\fontsize{9}{12}\sffamily\bfseries + Acknowledgements\enskip}} +\RequirePackage{amsthm} +\ifx\usethmrestate\relax + \RequirePackage{thm-restate} +\fi +\thm@headfont{% + \textcolor{lipicsGray}{$\blacktriangleright$}\nobreakspace\sffamily\bfseries} +\def\th@remark{% + \thm@headfont{% + \textcolor{lipicsGray}{$\blacktriangleright$}\nobreakspace\sffamily}% + \normalfont % body font + \thm@preskip\topsep \divide\thm@preskip\tw@ + \thm@postskip\thm@preskip +} +\def\@endtheorem{\endtrivlist}%\@endpefalse +\renewcommand\qedsymbol{\textcolor{lipicsGray}{\ensuremath{\blacktriangleleft}}} +\renewenvironment{proof}[1][\proofname]{\par + \pushQED{\qed}% + \normalfont \topsep6\p@\@plus6\p@\relax + \trivlist + \item[\hskip\labelsep + \color{lipicsGray}\sffamily\bfseries + #1\@addpunct{.}]\ignorespaces +}{% + \popQED\endtrivlist%\@endpefalse +} +\newcommand{\claimqedhere}{\renewcommand\qedsymbol{\textcolor{lipicsGray}{\ensuremath{\vartriangleleft}}}% +\qedhere% +\renewcommand\qedsymbol{\textcolor{lipicsGray}{\ensuremath{\blacktriangleleft}}}} +\newenvironment{claimproof}[1][\proofname]{ + \pushQED{\qed}% + \normalfont \topsep6\p@\@plus6\p@\relax + \trivlist + \item[\hskip\labelsep + \color{lipicsGray}\sffamily + #1\@addpunct{.}]\ignorespaces +}{% + \renewcommand\qedsymbol{\textcolor{lipicsGray}{\ensuremath{\vartriangleleft}}} + \popQED\endtrivlist%\@endpefalse + \renewcommand\qedsymbol{\textcolor{lipicsGray}{\ensuremath{\blacktriangleleft}}} +} +% inspired by qed of amsthm class +\DeclareRobustCommand{\lipicsEnd}{% + \leavevmode\unskip\penalty9999 \hbox{}\nobreak\hfill + \quad\hbox{$\lrcorner$}% +} +\AtBeginDocument{ + \@ifpackageloaded{algorithm2e}{ + \@ifpackagelater{algorithm2e}{2009/11/17}{ + \renewcommand{\algorithmcfname}{\sffamily\bfseries{}Algorithm}% + \renewcommand{\@algocf@procname}{\sffamily\bfseries{}Procedure}% + \SetAlgoCaptionSeparator{~} + \SetAlCapHSkip{0pt} + \renewcommand{\algocf@captiontext}[2]{% + \kern0.05em{\color{lipicsYellow}\rule{0.73em}{0.73em}}% + \hspace*{0.67em}\small #1\algocf@capseparator\nobreakspace#2} + \renewcommand{\algocf@makecaption}[2]{% + \parbox[t]{\textwidth}{\algocf@captiontext{#1}{#2}}% + }% + \renewcommand{\algocf@captionproctext}[2]{% + {% + \kern0.05em{\color{lipicsYellow}\rule{0.73em}{0.73em}}% + \hspace*{0.67em}\small% +\ProcSty{\ProcFnt\algocf@procname\ifthenelse{\boolean{algocf@procnumbered}}{\nobreakspace\thealgocf\algocf@typo\algocf@capseparator}{\relax}}% + \nobreakspace\ProcNameSty{\ProcNameFnt\algocf@captname #2@}% Name of the procedure in ProcName Style. + \ifthenelse{\equal{\algocf@captparam #2@}{\arg@e}}{}{% if no argument, write nothing + \ProcNameSty{\ProcNameFnt(}\ProcArgSty{\ProcArgFnt\algocf@captparam #2@}\ProcNameSty{\ProcNameFnt)}%else put arguments in ProcArgSty: + }% endif + \algocf@captother #2@% + }% +}% + \renewcommand{\@algocf@capt@boxed}{above} + \renewcommand{\@algocf@capt@ruled}{above} + \setlength\algotitleheightrule{0pt} + }{\ClassWarning{% + Package algorithm2e outdated}{You are using an outdated version of the package algorithm2e. Please update!}} + }{} + \@ifpackageloaded{algorithm}{ + \captionsetup[algorithm]{name=Algorithm, labelformat=boxed, position=top} + \newcommand\fs@ruled@notop{\def\@fs@cfont{\bfseries}\let\@fs@capt\floatc@ruled + \def\@fs@pre{}% + \def\@fs@post{\kern2pt\hrule\relax}% + \def\@fs@mid{\kern2pt\hrule\kern2pt}% + \let\@fs@iftopcapt\iftrue} + \@ifundefined{fst@algorithm}{}{ + \renewcommand\fst@algorithm{\fs@ruled@notop} + } + }{} + \ifx\usecleveref\relax\else + \@ifpackageloaded{cleveref}{\ClassWarning{Use document option 'cleveref' instead}{Use document option 'cleveref' instead directly loading package 'cleveref'}}{} + \fi + \ifx\usethmrestate\relax\else + \@ifpackageloaded{thm-restate}{\ClassWarning{Use document option 'thm-restate' instead}{Use document option 'thm-restate' instead directly loading package 'thm-restate'}}{} + \fi + \ifx\useautoref\relax + \@ifundefined{algorithmautorefname}{\newcommand{\algorithmautorefname}{Algorithm}}{\renewcommand{\algorithmautorefname}{Algorithm}}% + \fi +} + +\ifx\usecleveref\relax + \RequirePackage[capitalise, noabbrev]{cleveref} + \crefname{algocf}{Algorithm}{Algorithms} + \Crefname{algocf}{Algorithm}{Algorithms} + \newcommand{\crefrangeconjunction}{--} + \newcommand{\creflastconjunction}{, and\nobreakspace} +\fi +\ifx\useautoref\relax + \RequirePackage{aliascnt} +\fi +\newtheoremstyle{claimstyle}{\topsep}{\topsep}{}{0pt}{\sffamily}{. }{5pt plus 1pt minus 1pt}% + {$\vartriangleright$ \thmname{#1}\thmnumber{ #2}\thmnote{ (#3)}} +\theoremstyle{plain} +\newtheorem{theorem}{Theorem} +\ifx\numberwithinsect\relax + \numberwithin{theorem}{section} +\fi +\ifx\useautoref\relax + \addto\extrasenglish{% + \def\chapterautorefname{Chapter}% + \def\sectionautorefname{Section}% + \def\subsectionautorefname{Subsection}% + \def\subsubsectionautorefname{Subsubsection}% + \def\paragraphautorefname{Paragraph}% + \def\subparagraphautorefname{Subparagraph}% + } + \addto\extrasUKenglish{% + \def\chapterautorefname{Chapter}% + \def\sectionautorefname{Section}% + \def\subsectionautorefname{Subsection}% + \def\subsubsectionautorefname{Subsubsection}% + \def\paragraphautorefname{Paragraph}% + \def\subparagraphautorefname{Subparagraph}% + } + \addto\extrasUSenglish{% + \def\chapterautorefname{Chapter}% + \def\sectionautorefname{Section}% + \def\subsectionautorefname{Subsection}% + \def\subsubsectionautorefname{Subsubsection}% + \def\paragraphautorefname{Paragraph}% + \def\subparagraphautorefname{Subparagraph}% + } + \ifx\usethmrestate\relax + \newtheorem{lemma}[theorem]{Lemma} + \newtheorem{corollary}[theorem]{Corollary} + \newtheorem{proposition}[theorem]{Proposition} + \newtheorem{exercise}[theorem]{Exercise} + \newtheorem{definition}[theorem]{Definition} + \newtheorem{conjecture}[theorem]{Conjecture} + \newtheorem{observation}[theorem]{Observation} + \theoremstyle{definition} + \newtheorem{example}[theorem]{Example} + \theoremstyle{remark} + \newtheorem{note}[theorem]{Note} + \newtheorem*{note*}{Note} + \newtheorem{remark}[theorem]{Remark} + \newtheorem*{remark*}{Remark} + \theoremstyle{claimstyle} + \newtheorem{claim}[theorem]{Claim} + \newtheorem*{claim*}{Claim} + \else + \newaliascnt{lemma}{theorem} + \newtheorem{lemma}[lemma]{Lemma} + \aliascntresetthe{lemma} + \newcommand{\lemmaautorefname}{Lemma} + \newaliascnt{corollary}{theorem} + \newtheorem{corollary}[corollary]{Corollary} + \aliascntresetthe{corollary} + \newcommand{\corollaryautorefname}{Corollary} + \newaliascnt{proposition}{theorem} + \newtheorem{proposition}[proposition]{Proposition} + \aliascntresetthe{proposition} + \newcommand{\propositionautorefname}{Proposition} + \newaliascnt{exercise}{theorem} + \newtheorem{exercise}[exercise]{Exercise} + \aliascntresetthe{exercise} + \newcommand{\exerciseautorefname}{Exercise} + \newaliascnt{definition}{theorem} + \newtheorem{definition}[definition]{Definition} + \aliascntresetthe{definition} + \newcommand{\definitionautorefname}{Definition} + \newaliascnt{conjecture}{theorem} + \newtheorem{conjecture}[conjecture]{Conjecture} + \aliascntresetthe{conjecture} + \newcommand{\conjectureautorefname}{Conjecture} + \newaliascnt{observation}{theorem} + \newtheorem{observation}[observation]{Observation} + \aliascntresetthe{observation} + \newcommand{\observationautorefname}{Observation} + \theoremstyle{definition} + \newaliascnt{example}{theorem} + \newtheorem{example}[example]{Example} + \aliascntresetthe{example} + \newcommand{\exampleautorefname}{Example} + \theoremstyle{remark} + \newaliascnt{note}{theorem} + \newtheorem{note}[note]{Note} + \aliascntresetthe{note} + \newcommand{\noteautorefname}{Note} + \newtheorem*{note*}{Note} + \newaliascnt{remark}{theorem} + \newtheorem{remark}[remark]{Remark} + \aliascntresetthe{remark} + \newcommand{\remarkautorefname}{Remark} + \newtheorem*{remark*}{Remark} + \theoremstyle{claimstyle} + \newaliascnt{claim}{theorem} + \newtheorem{claim}[claim]{Claim} + \aliascntresetthe{claim} + \newcommand{\claimautorefname}{Claim} + \newtheorem*{claim*}{Claim} + \ifx\numberwithinsect\relax + \numberwithin{theorem}{section} + \numberwithin{lemma}{section} + \numberwithin{corollary}{section} + \numberwithin{proposition}{section} + \numberwithin{exercise}{section} + \numberwithin{definition}{section} + \numberwithin{conjecture}{section} + \numberwithin{observation}{section} + \numberwithin{example}{section} + \numberwithin{note}{section} + \numberwithin{remark}{section} + \numberwithin{claim}{section} + \fi + \fi +\else + \newtheorem{lemma}[theorem]{Lemma} + \newtheorem{corollary}[theorem]{Corollary} + \newtheorem{proposition}[theorem]{Proposition} + \newtheorem{exercise}[theorem]{Exercise} + \newtheorem{definition}[theorem]{Definition} + \newtheorem{conjecture}[theorem]{Conjecture} + \newtheorem{observation}[theorem]{Observation} + \theoremstyle{definition} + \newtheorem{example}[theorem]{Example} + \theoremstyle{remark} + \newtheorem{note}[theorem]{Note} + \newtheorem*{note*}{Note} + \newtheorem{remark}[theorem]{Remark} + \newtheorem*{remark*}{Remark} + \theoremstyle{claimstyle} + \newtheorem{claim}[theorem]{Claim} + \newtheorem*{claim*}{Claim} +\fi +\theoremstyle{plain} +\endinput +%% +%% End of file `lipics-v2021.cls'. diff --git a/martin.bib b/martin.bib new file mode 100644 index 0000000..2417828 --- /dev/null +++ b/martin.bib @@ -0,0 +1,310 @@ +@article{10.1145/3409006, +author = {Parreaux, Lionel}, +title = {The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl)}, +year = {2020}, +issue_date = {August 2020}, +publisher = {Association for Computing Machinery}, +address = {New York, NY, USA}, +volume = {4}, +number = {ICFP}, +url = {https://doi.org/10.1145/3409006}, +doi = {10.1145/3409006}, +abstract = {MLsub extends traditional Hindley-Milner type inference with subtyping while preserving compact principal types, an exciting new development. However, its specification in terms of biunification is difficult to understand, relying on the new concepts of bisubstitution and polar types, and making use of advanced notions from abstract algebra. In this paper, we show that these are in fact not essential to understanding the mechanisms at play in MLsub. We propose an alternative algorithm called Simple-sub, which can be implemented efficiently in under 500 lines of code (including parsing, simplification, and pretty-printing), looks more familiar, and is easier to understand. We present an experimental evaluation of Simple-sub against MLsub on a million randomly-generated well-scoped expressions, showing that the two systems agree. The mutable automaton-based implementation of MLsub is quite far from its algebraic specification, leaving a lot of space for errors; in fact, our evaluation uncovered several bugs in it. We sketch more straightforward soundness and completeness arguments for Simple-sub, based on a syntactic specification of the type system. This paper is meant to be light in formalism, rich in insights, and easy to consume for prospective designers of new type systems and programming languages. In particular, no abstract algebra is inflicted on readers.}, +journal = {Proc. ACM Program. Lang.}, +month = {aug}, +articleno = {124}, +numpages = {28}, +keywords = {subtyping, type inference, principal types} +} + +@inproceedings{PT98, + author = {Pierce, Benjamin C. and Turner, David N.}, + title = {Local type inference}, + booktitle = {Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, + series = {POPL '98}, + year = {1998}, + location = {San Diego, California, United States}, + pages = {252--265} +} + +@article{OZZ01, + author = "Martin Odersky and Matthias Zenger and Christoph Zenger", + title = "Colored local type inference", + journal = "Proc. 28th ACM Symposium on Principles of Programming Languages", + volume = "36", + number = "3", + pages = "41--53", + year = "2001", + xnote = "citeseer.ist.psu.edu/article/odersky01colored.html" } + + +@InProceedings{plue09_1, + author = {Martin Pl{\"u}micke}, + title = {Java type unification with wildcards}, + booktitle = {17th International Conference, INAP 2007, and 21st Workshop on Logic Programming, WLP 2007, W\"urzburg, Germany, October 4-6, 2007, Revised Selected Papers}, + year = {2009}, + editor = {Dietmar Seipel and Michael Hanus and Armin Wolf}, + Volume = {5437}, + publisher = {Springer-Verlag Heidelberg}, + pages = {223--240}, + SERIES = {Lecture Notes in Artificial Intelligence} +} + +@article{DM82, + author={Luis Damas and Robin Milner}, + title={Principal type-schemes for functional programs}, + journal={Proc. 9th Symposium on Principles of Programming Languages}, + year={1982} +} + +@article{Rob65, + author={J. A. Robinson}, + title={A Machine-Oriented Logic Based on the Resolution Principle}, + journal={Journal of ACM}, + volume={12(1)}, + pages={23-41}, + month=Jan, + year={1965}} + +@article{MM82, + author={A. Martelli and U. Montanari}, + title={An Efficient Unification Algorithm}, + journal={ACM Transactions on Programming Languages and Systems}, + volume={4}, + pages={258-282}, + year={1982}} + +@InProceedings{Plue07_3, + author = {Martin Pl{\"u}micke}, + title = {Typeless {P}rogramming in \textsf{{J}ava 5.0} with {W}ildcards}, + booktitle = {5th {I}nternational {C}onference on {P}rinciples and {P}ractices of {P}rogramming in {J}ava}, + pages = {73--82}, + year = {2007}, + editor = {Vasco Amaral and Lu\'is Veiga and Lu\'is Marcelino and H. Conrad Cunningham}, + series = {ACM International Conference Proceeding Series}, + volume = {272}, + month = {September} +} + +@inproceedings{plue15_2, + author = {Martin Pl{\"{u}}micke}, + title = {More Type Inference in {J}ava 8}, + booktitle = {Perspectives of System Informatics - 9th International Ershov Informatics + Conference, {PSI} 2014, St. Petersburg, Russia, June 24-27, 2014. + Revised Selected Papers}, + editor = {Andrei Voronkov and Irina Virbitskaite}, + volume = {8974}, + series = {Lecture Notes in Computer Science}, + pages = {248--256}, + year = {2015}, + publisher = {Springer} +} + +@phdthesis{GS89, + author = "Gert Smolka", + title = "Logic Programming over Polymorphically Order-Sorted Types", + school = {Department Informatik, University of Kaisers\-lautern}, + address = {Kaiserslautern, Germany}, + month = may, + year = 1989 +} + +@Article{MH91, + author = "Michael Hanus", + title = "Parametric order-sorted types in logic programming", + journal = "Proc. TAPSOFT 1991", + year = "1991", + volume = "LNCS", + number = "394", + pages = "181--200" +} + +@inproceedings{CB95, + author = "Christoph Beierle", + title = "Type Inferencing for Polymorphic Order-Sorted Logic Programs", + booktitle = "International Conference on Logic Programming", + pages = "765-779", + year = "1995", + OPturl = "citeseer.ist.psu.edu/beierle95type.html" } + +@incollection{HiTo92, + author = {Patricia M. Hill and Rodney W. Topor}, + editor = {Frank Pfenning}, + title = {A {S}emantics for {T}yped {L}ogic {P}rograms}, + booktitle = {Types in Logic Programming}, + year = {1992}, + pages = {1-62}, + publisher = {MIT Press}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} + + +@inproceedings{TEP05, + author = "Torgersen, Mads and Ernst, Erik and + Hansen, Christian Plesner", + title = "Wild {F}{J}", + booktitle = "Proceedings of FOOL 12", + year = 2005, + editor = "Wadler, Philip", + address = "Long Beach, California, USA", + month = Jan, + organization = "ACM", + publisher = "School of Informatics, University of + Edinburgh", + anote = "Electronic publication, at the URL given + below", + abstract = "This paper presents a formalization of + wildcards, which is one of the new features of + the Java programming language in version + JDK5.0. Wildcards help alleviating the + impedance mismatch between generics, or + parametric polymorphism, and traditional + object-oriented subtype polymorphism. They do + this by quantifying over parameterized types + with different type arguments. Wildcards take + inspiration from several sources including + use-site variance, and they could be considered + as a way to introduce a syntactically + light-weight kind of existential types into a + main-stream language. This formalization + describes the mechanism, in particular the + wildcard capture process where the existential + nature of wildcards becomes evident.", + url = "http://homepages.inf.ed.ac.uk/wadler/fool/", + annote = "wild-fj.pdf" +} + +@Article{BBDGV18, + author = {Lorenzo Bettini and Viviana Bono and Mariangiola Dezani-Ciancaglini and Paola Giannini and Betti, Venneri}, + title = {Java \& Lambda: A Featherweight Story}, + journal = {Logical Methods in Computer Science}, + year = {2018}, + OPTkey = {}, + volume = {14(3:17)}, + OPTnumber = {}, + pages = {1--24}, + OPTmonth = {}, + OPTnote = {}, + OPTannote = {} +} + +@inproceedings{plue17_2, + author = {Pl\"{u}micke, Martin and Stadelmeier, Andreas}, + title = {Introducing {S}cala-like Function Types into {J}ava-{TX}}, + booktitle = {Proceedings of the 14th International Conference on Managed Languages and Runtimes}, + series = {ManLang 2017}, + year = {2017}, + isbn = {978-1-4503-5340-3}, + location = {Prague, Czech Republic}, + pages = {23--34}, + numpages = {12}, + url_ = {http://doi.acm.org/10.1145/3132190.3132203}, + doi = {10.1145/3132190.3132203}, + acmid = {3132203}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {Java, function types, lambda expressions, type inference}, +} + +@InProceedings{Plue04_1, + author = {Martin Pl{\"u}micke}, + title = {Type {U}nification in \textsf{Generic--Java}}, + booktitle = {Proceedings of 18th {I}nternational {W}orkshop on {U}nification ({U}{N}{I}{F}'04)}, + year = {2004}, + address = {Cork}, + editor = {Michael Kohlhase}, + month = {July}, + OPturl = {http://www.lsv.ens-cachan.fr/unif/} +} + +@INPROCEEDINGS{AZ04, + author = {Davide Ancona and Elena Zucca}, + title = {Principal typings for {J}ava-like languages}, + booktitle = {In ACM Symp. on Principles of Programming Languages 2004}, + year = {2004}, + pages = {306--317}, + publisher = {ACM Press} +} + +@inproceedings{plue16_1, + author = {Martin Pl{\"{u}}micke}, + title = {Structural Type Inference in Java-like Languages}, + booktitle = {Gemeinsamer Tagungsband der Workshops der Tagung Software Engineering + 2016 {(SE} 2016), Wien, 23.-26. Februar 2016.}, + pages = {109--113}, + year = {2016}, + Optcrossref = {DBLP:conf/se/2016w}, + url = {http://ceur-ws.org/Vol-1559/paper09.pdf}, + timestamp = {Mon, 07 Mar 2016 13:17:33 +0100}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/se/Plumicke16}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{ADDZ05, + author = {Ancona, Davide and Damiani, Ferruccio and Drossopoulou, Sophia and Zucca, Elena}, + title = {Polymorphic Bytecode: Compositional Compilation for {J}ava-like Languages}, + booktitle = {Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, + series = {POPL '05}, + year = {2005}, + isbn = {1-58113-830-X}, + location = {Long Beach, California, USA}, + pages = {26--37}, + numpages = {12}, + url = {http://doi.acm.org/10.1145/1040305.1040308}, + doi = {10.1145/1040305.1040308}, + acmid = {1040308}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {compositional analysis, type systems}, +} + +@InProceedings{aModelForJavaWithWildcards, +author="Cameron, Nicholas +and Drossopoulou, Sophia +and Ernst, Erik", +editor="Vitek, Jan", +title="A Model for Java with Wildcards", +booktitle="ECOOP 2008 -- Object-Oriented Programming", +year="2008", +publisher="Springer Berlin Heidelberg", +address="Berlin, Heidelberg", +pages="2--26", +abstract="Wildcards are a complex and subtle part of the Java type system, present since version 5.0. Although there have been various formalisations and partial type soundness results concerning wildcards, to the best of our knowledge, no system that includes all the key aspects of Java wildcards has been proven type sound. This paper establishes that Java wildcards are type sound. We describe a new formal model based on explicit existential types whose pack and unpack operations are handled implicitly, and prove it type sound. Moreover, we specify a translation from a subset of Java to our formal model, and discuss how several interesting aspects of the Java type system are handled.", +isbn="978-3-540-70592-5" +} +@article{WildcardsNeedWitnessProtection, +author = {Bierhoff, Kevin}, +title = {Wildcards Need Witness Protection}, +year = {2022}, +issue_date = {October 2022}, +publisher = {Association for Computing Machinery}, +address = {New York, NY, USA}, +volume = {6}, +number = {OOPSLA2}, +url = {https://doi.org/10.1145/3563301}, +doi = {10.1145/3563301}, +abstract = {In this paper, we show that the unsoundness discovered by Amin and Tate (2016) in Java’s wildcards is avoidable, even in the absence of a nullness-aware type system. The key insight of this paper is that soundness in type systems that implicitly introduce existential types through subtyping hinges on still making sure there are suitable witness types when introducing existentially quantified type variables. To show that this approach is viable, this paper formalizes a core calculus and proves it sound. We used a static analysis based on our approach to look for potential issues in a vast corpus of Java code and found none (with 1 false positive). This confirms both that Java's unsoundness has minimal practical consequence, and that our approach can avoid it entirely with minimal false positives.}, +journal = {Proc. ACM Program. Lang.}, +month = {oct}, +articleno = {138}, +numpages = {22}, +keywords = {Null, Java Wildcards, Existential Types} +} +@InProceedings{TIforFGJ, + author = {Stadelmeier, Andreas and Pl\"{u}micke, Martin and Thiemann, Peter}, + title = {{Global Type Inference for Featherweight Generic Java}}, + booktitle = {36th European Conference on Object-Oriented Programming (ECOOP 2022)}, + pages = {28:1--28:27}, + series = {Leibniz International Proceedings in Informatics (LIPIcs)}, + ISBN = {978-3-95977-225-9}, + ISSN = {1868-8969}, + year = {2022}, + volume = {222}, + editor = {Ali, Karim and Vitek, Jan}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + address = {Dagstuhl, Germany}, + URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16256}, + URN = {urn:nbn:de:0030-drops-162560}, + doi = {10.4230/LIPIcs.ECOOP.2022.28}, + annote = {Keywords: type inference, Java, subtyping, generics} +} diff --git a/orcid.pdf b/orcid.pdf new file mode 100644 index 0000000..c31b039 Binary files /dev/null and b/orcid.pdf differ diff --git a/prolog.tex b/prolog.tex new file mode 100755 index 0000000..ba7e959 --- /dev/null +++ b/prolog.tex @@ -0,0 +1,206 @@ +\usepackage{xspace} +\usepackage{color,ulem} +\usepackage{listings} +\lstset{language=Java, + showspaces=false, + showtabs=false, + breaklines=true, + showstringspaces=false, + breakatwhitespace=true, + basicstyle=\ttfamily\fontsize{8}{9.6}\selectfont, %\footnotesize + escapeinside={(*@}{@*)}, + captionpos=b, +} +\lstdefinestyle{fgj}{backgroundcolor=\color{lime!20}} +\lstdefinestyle{tfgj}{backgroundcolor=\color{lightgray!20}} + + +\newcommand\mv[1]{{\tt #1}} +\newcommand{\ol}[1]{\overline{\tt #1}} +\newcommand{\exptype}[2]{\mathtt{#1 \texttt{<} #2 \texttt{>} }} +\newcommand\ddfrac[2]{\frac{\displaystyle #1}{\displaystyle #2}} + +\newcommand{\sarray}[2]{\begin{array}[t]{#1} #2 \end{array}} + +%\newcommand{\olsub}{\textrm{$\, \leq^\ast \,$}\ } +\newcommand{\olsub}{\textrm{$<:$}\ } + +\newcommand{\sub}\olsub%{\mbox{$<$}} + +\newcommand{\set}[1]{\{ #1 \} } + +\definecolor{red}{rgb}{1,0,0} +\newcommand{\red}[1]{\textcolor{red}{#1}} + +\newcommand{\commentarystar}[1]{\red{\({}^*\)}\marginpar[\tiny + \red{\({}^*\)#1}]{\tiny \red{\({}^*\)#1}}} +\newcommand{\commentary}[1]{\marginpar[\tiny + \red{#1}]{\tiny \red{#1}}} +\newcommand{\commentarymark}[1]{\color{red} #1\ensuremath{^*}\color{black}} +\newcommand{\commentarymargintext}[2]{\color{red} #1$^*$ + \color{black}\marginpar[\tiny \red{\({}^*\)#2}]{\tiny \red{\({}^*\)#2}}} +\newcommand{\commentaryintext}[2]{\color{red} #1\textrm{$^*${\tiny #2}}\color{black}} +\newcommand{\commentarymath}[2]{\color{red} #1^*\color{black}\)\marginpar[\tiny \red{\({}^*\)#2}]{\tiny \red{\({}^*\)#2}}\(} +\newcommand{\replaced}[2]{\erased{#1}\inserted{#2}} +\newcommand{\erased}[1]{\commentary{\sout{#1}}} +\newcommand{\inserted}[1]{\color{red}#1\color{black}\xspace} + +\newcommand\Erase[1]{|#1|} +\newcommand\Angle[1]{\langle#1\rangle} + +\newcommand\TFGJ{FGJ-GT\xspace} +\newcommand\FGJGT{FGJ-GT\xspace} +\newcommand\FGJType{\textbf{FGJType} } + +\newcommand\TVX{\mv X} +\newcommand\TVY{\mv Y} +\newcommand\TVZ{\mv Z} +\newcommand\TVW{\mv W} + +\newcommand\CL[1]{\textit{Cl}$_{#1}$} +\newcommand\subconstr{\lessdot} +\newcommand\eqconstr{\doteq} +\newcommand\subeq{\mathbin{\texttt{<:}}} +\newcommand\extends{\ensuremath{\triangleleft}} + +\newcommand\rulename[1]{\textup{\textsc{(#1)}}} +\newcommand{\generalizeRule}{General} + +%%% FJ-IT Type rules +\newcommand{\environmentvdash}{\Pi;\Delta;\Gamma \vdash} + +\newcommand{\fjtypeinference}{\textbf{FJTypeInference}} + +%%% Commands for FGJTYPE algorithm +\newcommand{\tv}[1]{\mathit{ #1 }} +%\newcommand{\fjtypeInsert}{\textbf{FJTypeInsert}} +\newcommand{\unifyGenerics}{\ensuremath{\Delta}}% {\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{\type}[1]{\mathtt{#1}} +\newcommand{\anyType}[1]{\mathit{#1}} +\newcommand{\gType}[1]{\texttt{#1}} +\newcommand{\mtypeEnvironment}{\ensuremath{\Pi}} +\newcommand{\methodAssumption}{\ensuremath{\mathtt{\lambda}}} +\newcommand{\localVarAssumption}{\ensuremath{\mathtt{\eta}}} +\newcommand{\expandLB}{\textit{expandLB}} + +\def\exptypett#1#2{\texttt{#1}\textrm{{\tt <#2}}\textrm{{\tt >}}\xspace} +\def\exp#1#2{#1(\,#2\,)\xspace} +\newcommand{\ldo}{, \ldots , } + +% WILDCARD specific: +\newcommand{\xtype}[2]{\ensuremath{\exists #1 . \type{#2}}} +\newcommand{\xtypevar}[1]{\ensuremath{\exists \emptyset . \type{#1}}} + +\newcommand{\wtypestore}[3]{\ensuremath{#1 = \wtype{#2}{#3}}} +%\newcommand{\wtype}[2]{\ensuremath{[#1\ #2]}} +\newcommand{\wtv}[1]{\ensuremath{\tv{#1}_?}} +\newcommand{\wcstore}{\ensuremath{\Delta}} + +%\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}_?}} +\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}}} +\newcommand{\wildcardEnv}{\ensuremath{\mathbb{W}}} +\newcommand{\wildcard}[3]{\ensuremath{\mathtt{#1 : [#3 .. #2]}}} +\newcommand{\cwildcard}[3]{\ensuremath{\mathtt{\overleftarrow{#1}^{#2}_{#3}}}} + +\newcommand{\generics}[1]{\ensuremath{\mathtt{\texttt{<} {#1} \texttt{>} }}} + +\newcommand{\lessdotCC}{\ensuremath{\lessdot^{\texttt{c}}}} + +\newcommand{\ccDecaptureRule}{\rulename{CC-Decapture}} +\newcommand{\ccInvalidate}{\rulename{CC-Invalidate}} + +\newcommand{\ruleWCEquals}[0]{\rulename{WC-Equals}} +\newcommand{\ruleReduceWC}[0]{\rulename{Reduce}} +\newcommand{\ruleReduce}[0]{\rulename{Reduce}} +\newcommand{\ruleSubstWC}[0]{\rulename{Subst-WC}} +\newcommand{\subclass}{\mathtt{\sqsubset}\mkern-5mu :} + +\newcommand{\TameFJ}{\text{TameFJ}} +\newcommand{\TamedFJ}{\textbf{TamedFJ}} +\newcommand{\TYPE}{\textbf{TYPE}} + +\newcommand{\vdashI}[0]{\ \ . \kern-0.8em \vdash } + + +\newcommand{\wildcardTV}[1]{\type{#1}_?} +\newcommand{\replaceWC}[2]{\ensuremath{[#1/#2]_?}} +\newcommand{\replaceAdapt}[2]{\ensuremath{[#1/#2]_\uparrow}} + +\newcommand{\wcEnv}[3]{#1 : [#2\ ..\ #3]} +\newcommand{\fresh}[1]{\textit{fresh}(#1)} + + +\newcommand{\typerule}[1]{\small\textsc{#1}} +\newcommand{\letstmt}[2]{\texttt{let}\ #1 \ \texttt{in} \ #2} +\newcommand{\elvis}[0]{\ensuremath{\ {?}{:}\ }} + +\newcommand{\wildFJ}[0]{\textbf{WildFJ}} + +%\newcommand{\wfresh}[0]{\textit{wfresh}} + +%COLORS: +\definecolor{change}{RGB}{201,201,255} +\definecolor{subst}{RGB}{241,203,255} +\definecolor{addition}{RGB}{225,247,213} +\definecolor{highlight}{RGB}{255,189,189} +\definecolor{frame}{HTML}{634b7d} +%\definecolor{gray}{RGB}{120, 120, 120} +%\definecolor{frame}{RGB}{241, 246, 249} + +\tcbset{colback=white,colframe=frame,fonttitle=\bfseries,coltitle=white} + +\newcommand{\deduction}[2]{ + \begin{array}[c]{l} +#1 \\ +\hline +\vspace*{-0.4cm}\\ +#2 +\end{array} +} + +\newcommand{\nextdeduction}[1] + { + \begin{array}{@{}l@{}r@{}} + \begin{array}[c]{l} + \hline + \vspace*{-0.4cm}\\ + #1 + \end{array} % \rulename{#3} + \end{array} + } + +\newcommand{\subst}[2]{ +\left[ #1 / #2 \right] +} + +\newenvironment{constraintset} + { +\begin{tcolorbox} + } + { +\end{tcolorbox} + } + +\newcommand{\wcNtype}[2]{#1 .\ntype{#2}} +\newcommand{\wctype}[3]{#1 .\exptype{#2}{#3}} +\newcommand{\wtype}[1]{\mathit{#1}} +\newcommand{\ntype}[1]{\mathtt{#1}} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "TIforGFJ" +%%% End: diff --git a/soundness.tex b/soundness.tex new file mode 100644 index 0000000..13f4b36 --- /dev/null +++ b/soundness.tex @@ -0,0 +1,191 @@ +\section{Soundness} + + + +% %This lemma can be used to proof Normalize rule! +% \begin{lemma}\label{lemma:wildcardReplacement} +% Wildcards with the same upper and lower bound can be replaced by their bounds without breaking subtype relations. +% \begin{description} +% \item[If] $\Delta \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash \type{T} <: \type{S}$ +% \item[and] $\type{U} = \type{L}$ and $\text{fv}(\type{U}) = \emptyset$ +% \item[Then] $\Delta \vdash [\type{U}/\type{X}]\type{T} <: [\type{U}/\type{X}]\type{S}$ +% \end{description} +% \end{lemma} +% \textit{Proof:} %TODO +% %By structural induction over the subtype relation +% %S-Refl: by assumption L <: L implies [\type{U}/\type{X}]L + +% \begin{lemma}\label{lemma:noAdditionalFV} +% Type solution $\sigma$ does not add additional free variables. +% \begin{description} +% \item[If] $(\sigma, \Delta) = \unify{}( \overline{ \type{S} \lessdot \type{T} } \cup C)$ +% \item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$ +% \item[Then] $fv(\sigma(\overline{ \type{S} })) = \emptyset, fv(\sigma(\overline{ \type{T} })) = \emptyset$ +% \end{description} +% \end{lemma} + +% \begin{lemma} +% % https://math.libretexts.org/Bookshelves/Mathematical_Logic_and_Proof/Book%3A_Mathematical_Reasoning__Writing_and_Proof_(Sundstrom)/07%3A_Equivalence_Relations/7.03%3A_Equivalence_Classes +% $\doteq$ is an equivalence relation on a constraint set $C$. + +% \begin{description} +% \item[If] $\Delta \vdash \overline{\type{T} <: \type{S}}$ and $\type{T} \doteq \type{S}$ +% \item[Then] $\Delta \vdash [\type{T}/\type{S}](\overline{\type{T} <: \type{S}})$ +% \end{description} +% \end{lemma} + +\begin{lemma} +The \unify{} algorithm only produces correct output for constraints not containing free variables. + +\begin{description} +\item[If] $(\sigma, \Delta) = \unify{}( \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdot \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$ +\item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$ +\item[Then] there exists a $\Delta'$ with: +$\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$ +and $\Delta, \Delta' \vdash \overline{\text{CC}(\sigma(\type{S'})) <: \sigma(\type{T'})}$ +% and $\sigma(\type{T'}) = \sigma(\type{T'})$. + +The function $\text{CC}$ is given as $\text{CC}(\wcNtype{\Delta}{N}) = \type{N}$ +\end{description} +\end{lemma} + +\textit{Proof:} +%(we are going backwards over the algorithm) +%first we have to determine the \Delta'' -> it's only the wildcards which are free in N +% during this proof we can use Delta'' as we like + +For every step in the \unify{} algorithm: +Assuming the unifier $\sigma$ is correct for a constraint set $C'$, the unifier is also correct for the +constraint set $C$ before the transformation. +\begin{description} +\item[Assumption:] $\unify{}(C) = (\Delta, \sigma)$, with $\Delta \vdash \sigma(C)$ +\item[Induction step:] For every case $C'$ which can be transformed to $C$ we have to show $\Delta \vdash \sigma(C')$ +\end{description} + +\unify{} terminates with $C = \emptyset$ for which the preposition holds: +$\Delta \vdash \sigma(\emptyset)$ + +We now show that for every transformation of a constraint set $C$ to a constraint set $C'$ +the preposition holds for $C$ using the assumption that it holds for $C'$ : +$\Delta \vdash \sigma(C') \implies \Delta \vdash \sigma(C)$ + +\begin{description} +\item[AddDelta] $C$ is not changed +\item[GenDelta] by definition, S-Var-Left, and S-Trans %The generated type variable is unique due to the solved form property. %and the solved form property (no $\tv{a}$ in $C$) +\item[GenSigma] by definition. +% holds for $\set{\tv{a} \doteq \type{G}}$ by definition. +% Holds for $C$ by assumption and because $\tv{a} \notin C$ by solved form definition ($[\type{G}/\tv{a}]C = C$). +\item[Ground] Assumption and S-Bot +\item[Sub-Elim] Assumption and S-Refl +\item[Force] by assumption and $\rwildcard{X} = \type{U}$ %TODO: step 5 should remove all X^T_T with T (make wildcards with same upper and lower bounds to normal types) +\item[Raise] Assumption, S-Trans +\item[Settle] Assumption, S-Trans +\item[Super] S-Extends ($\vdash \wctype{\Delta}{C}{\ol{T}} <: \wctype{\Delta}{D}{[\ol{T}/\ol{X}]\ol{N}}$), S-Trans +\item[\generalizeRule{}] by Assumption, because $C \subset C'$ +\item[Adapt] Assumption, S-Extends, S-Trans +\item[Adopt] Assumption, because $C \subset C'$ +%\item[Capture, Reduce] are always applied together. We have to destinct between two cases: +\item[Capture] +If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists. +If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) \neq \emptyset$ we have to show $\Delta' \vdash \text{CC}(\sigma(\wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}})) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$, +which holds by assumption with $\Delta'$ chosen in a way that $\text{fv}(\exptype{C}{\ol{S}}) \subseteq \Delta'$. The variables $\ol{C}$ in $\ol{S}$ can be renamed to $\ol{B}$, because $\ol{C}$ are fresh. +%If $\text{fv}(\wctype{\Delta}{C}{\ol{T}}) \neq \emptyset$ we have to show $\Delta \vdash \sigma(\exptype{C}{\ol{S}}) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$. +%$\Delta \vdash \sigma([\ol{C}/\ol{B}]\exptype{C}{\ol{S}}) <: \sigma(\wctype{\Delta}{C}{\ol{T}})$ holds by assumption and +%the variables $\ol{B}$ in $\ol{S}$ can be renamed to $\ol{C}$, because $\ol{C} \notin \ol{S}$ ($\ol{C}$ are fresh). +%The assumption implies $\text{fv}(\ol{S}) \subseteq \text{dom}(\Delta \cup \set{\overline{\wildcard{C}{\type{U'}}{\type{L'}}}})$ +%, which implies $\text{fv}(\ol{S}) \subseteq \text{dom}(\Delta \cup \set{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}})$. + +%We are doing a capture conversion. If $\type{T}$ does not contain free variables, this does not affect the subtype relation. +\item[Reduce] %Assumption and S-Exists. +If $\text{fv}(\exptype{C}{\ol{S}}) = \emptyset$ the preposition holds by Assumption and S-Exists. +If $\text{fv}(\exptype{C}{\ol{S}}) \neq \emptyset$ there exists a $\Delta'$ with +$\Delta' \vdash \text{CC}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$. +\item[Match] Assumption, S-Trans +\item[Trim] Assumption and S-Exists +\item[Remove] $C$ is not changed +\item[Circle] S-Refl +\item[Swap] by definition +\item[Erase] S-Refl +\item[Equals] by definition +% \item[Reduce] +% The renaming from $\rwildcard{C}$ to $\rwildcard{B}$ is not a problem. It's allowed to rename wildcards inside a type. +% Removing $\rwildcard{C}$ from the environment does not change anything because it was freshly generated and is used nowhere. + +% The rest follows directly from S-Exists. +% We can say: $\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$, +% because the input to the \unify{} algorithm has no free type variables and we never substitute a type with free type variables +% and none of the other steps of the algorithm generates a $\lessdot$ constraint containing free type variables on the right side. %TODO: proof + +% $\text{fv}(\ol{T}) \subseteq \text{dom}(\wildcardEnv \cup \overline{\wildcard{B}{\type{U'}}{\type{L'}}})$ +% TODO: The capture conversion has to be when substituting a $\wtv{a}$ variable. Then we have to rename! +% %Lets first try it without the capture conversion. And involve the wtvs in the second step +% % The algorithm works by never substituting wildcards + + + +% \unify{} cannot guarantee the premise $\text{dom}(\Delta, \Delta') \cap \text{fv}(\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N}) = \emptyset$. +% We loosen the soundness requirements and allow a arbitrary environment $\Delta''$ to be added to the right side of the subtype relation. +% This is still sufficient to proof soundness for the whole algorithm. +% We show that the need for the additional environment $\Delta''$ can be satisfied by a let statement. + +% \begin{itemize} +% \item $\Delta, \Delta' \vdash [\ol{T}/\ol{X}]\ol{L} <: \ol{T}$: S-Exists +% \item $\Delta, \Delta' \vdash \ol{T} <: [\ol{T}/\ol{X}]\ol{U}$: S-Exists +% \item $\textit{fv}(\ol{T}) \subseteq \text{dom}{\Delta, \Delta'}$: $\wildcardEnv$ holds all variables %TODO: Proof +% \end{itemize} +\item[Normalize] Assumption and lemma 5 \emph{substitution preserves subtyping}.%\ref{lemma:wildcardReplacement}. (Or Lemma 5 from the wildcard paper. \emph{substitution preserves subtyping}) +% The GenSigma step replaces both sides of $\rwildcard{A} \doteq \rwildcard{B}$ with the upper bound $\type{U}$. +% This works for every constraint, whether it contains free variables or not. +% It does not add to free variables of constraints because the upper bound does not contain any. +The GenSigma and Gen Delta steps remove Wildcards which have the same upper and lower bound. +$\rwildcard{A},\rwildcard{B} \notin \sigma(C)$ + +% sigma(T) = sigma(U) we have to show that T = U means \Delta \vdash [T/U]C \implies \Delta \vdash [U/T]C +% the constraints L <. U, U <. L lead to L =. U +%If L is List with X being free wildcard +%then U <. L will fail if U is type variable + + + + +% this is because bounds never contain free variables (is that true?) + +%This type contains free variables when A is replaced by an CC wildcard + +%This must fail: +\begin{verbatim} + A m(List> l, A) + +m(List> l, "hi") +\end{verbatim} +%This fails because of Equals rule (TODO: proof) + +\item[Tame] same reasoning as Normalize +\item[Bot] S-Bot +\item[Pit] S-Bot +\item[Upper] S-Trans and S-VarLeft +\item[Lower] S-Trans and S-VerRight +\item[Subst-WC] by S-Refl +\item[Subst] +$\sigma(C \cup \set{\tv{a} \doteq \type{T}}) = \sigma([\type{T}/\tv{a}]C \cup \set{\tv{a} \doteq \type{T}})$ +and +$\sigma(\wildcardEnv) = \sigma([\type{T}/\tv{a}]\wildcardEnv)$ +\item[Subst-WC] +%Proof by Lemma 5 \emph{Type substitution preserves subtyping} from \cite{WildcardsNeedWitnessProtection}. +Same as Subst +\end{description} + +\subsection{Type Inference Soundness} +The type solution is a correct one in respect to the type rules. + +Problem: +The capture conversion and let statements. +Constraint a <. b => CC(X.C) <: C +Why is X the only type used + +$\type{T} \lessdot \type{S}$: +If the left part of the constraint has no free variables the solution $\sigma(\type{T})$ will have neither. +This means that all used type variables on both sides are bound in the global environment or the environment of the left side +%X.C <: C +%C = C (both sides must be the same) +%the left side has no free variables! \ No newline at end of file diff --git a/unify.tex b/unify.tex new file mode 100644 index 0000000..63a92ce --- /dev/null +++ b/unify.tex @@ -0,0 +1,1080 @@ + +\section{Unify}\label{sec:unify} +\newcommand{\gtype}[1]{\type{#1}} +%\newcommand{\tw}[1]{\tv{#1}_?} +The \unify{} algorithm computes the type solution. + +\begin{description} + \item[Input:] List of constraints $C = \set{ \type{T} \lessdot \type{T}, \type{T} \doteq \type{T} \ldots}$ + +The input constraints must be of the following format: + +\begin{tabular}{lcll} + $c $ &$::=$ & $\type{T} \lessdot \type{U}$ & Constraint \\ + $\type{T}, \type{U}, \type{L} $ & $::=$ & $\tv{a} \mid \wtv{a} \mid \ntype{N}$ & Type variable or Wildcard Variable or Type \\ + $\ntype{N}, \ntype{S}$ & $::=$ & $\wctype{\overline{\wildcard{X}{U}{L}}}{C}{\ol{T}} $ & Class Type \\ +\end{tabular}\\[0.5em] + +\noindent +Additional requirements: +\begin{itemize} + \item The input only consists of $\lessdot$ constraints +% \item No free variables in type parameters. +% A constraint like $\tv{a} \lessdot \exptype{List}{\rwildcard{X}}$ is prohibited. +% $\tv{a} \lessdot \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ is valid. + \item the input is a list of constraints. It cannot be a set. + A constraint set containing the constraint $\tv{a} \lessdot \type{T}$ twice + is a different to one that contains it only once. + %\item every wildcard is bound to its enclosing type. +\item Naming scheme of every wildcard environment has to be the same. +%TODO: We need this so that wildcard substitutions get the correct name. also the Equals rule needs this condition +%Example: +Although alpha renaming of wildcards inside a type is allowed by the type system the \unify{} algorithm never does it. +Renaming wildcards leads to additional problems in the substitution rules and in the result containing substitutions with renamed wildcards. +For the \rulename{Equals} to work properly it is adviced to name all wildcards in a specific scheme. +For example by numbering them according to their appereance inside the type parameters +(e.g. $\wctype{\rwildcard{1}, \rwildcard{2}}{Pair}{\rwildcard{1}, \rwildcard{2}}$). +\end{itemize} + +\item[Output:] +Set of unifiers $Uni = \set{\sigma_1, \ldots, \sigma_n}$ and an environment $\Delta$ +\end{description} + +The \unify{} algorithm internally uses the following data types: + +\begin{tabular}{lcll} + $C $ &$::=$ &$\overline{c}$ & Constraint set \\ + $c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\ + $\type{T}, \type{U}, \type{L} $ & $::=$ & $\tv{a} \mid \wtv{a} \mid \gtype{G}$ & Type variable or Type \\ + $\gtype{G}$ & $::=$ & $\type{X} \mid \ntype{N}$ & Wildcard, or Class Type \\ + $\ntype{N}, \ntype{S}$ & $::=$ & $\wctype{\triangle}{C}{\ol{T}} $ & Class Type \\ + $\triangle$ & $::=$ & $\overline{\wtype{W}}$ & Wildcard Environment \\ + $\wtype{W}$ & $::=$ & $\wildcard{X}{U}{L}$ & Wildcard \\ +\end{tabular} + +The $\wtv{a}$ type variables are flagged as wildcard type variables. +These type variables can be substituted by a wildcard or a type with free wildcard variables. +As long as a type variable is flagged with as $\wtv{a}$ it will only be used by the subst-wc rule in step 1. +In step 2 all of the wildcard flags are dismissed. +The output therefore never contains these flags. + +\unify{} applies a capture conversion everywhere it is possible (see \rulename{Capture} rule). +Capture conversion removes a types bounding environment $\Delta$. +Type variables used in its type parameters are now bound to a global scope and not locally anymore. + +With \texttt{C} being class names and \texttt{A} being wildcard names. +The wildcard type $\wildcard{X}{U}{L}$ consist out of an upper bound $\type{U}$, a lower bound $\type{L}$ +and a name $\mathtt{X}$. + +The \rulename{Normalize} rule eliminates wildcards. % TODO +This is done by setting the upper and lower bound to the same value. +We generate wildcards with the \rulename{\generalizeRule} rule. +It is important to generate new wildcards in a standardized fashion. +When having two constraints $\type{T} \lessdot \tv{a}$ and $\type{T} \lessdot \tv{b}$, +then after applying the \rulename{\generalizeRule} rule the freshly generated constraints are +$\tv{a} \doteq \type{T'}, \tv{b} \doteq \type{T'}$. +Both type variables get assigned the same type. +This is necessary for the \rulename{Equals} rule to work properly. + + +\begin{figure} + \begin{center} + \leavevmode + \fbox{ + \begin{tabular}[t]{l@{~}l} + \rulename{Subst} & + $\begin{array}[c]{l} +\wildcardEnv \vdash C \cup \set{\tv{a} \doteq \type{T}}\\ + \hline +[\type{T}/\tv{a}]\wildcardEnv \vdash [\type{T}/\tv{a}] +C \cup \set{\tv{a} \doteq \type{T}} + \end{array} + \quad \begin{array}{c} + \tv{a} \notin \type{T} \\ + \text{fv}(\type{T}) = \emptyset + \end{array}$\\ +\\ +\rulename{Subst-WC} &$ + \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} \quad \wtv{a} \notin \type{G} +$ +\end{tabular}} +\end{center} +\caption{Substitution rules}\label{fig:subst-rules} +\end{figure} + + +\begin{figure} + \begin{center} + \leavevmode + \fbox{ + \begin{tabular}[t]{l@{~}l} + % \rulename{normalize} + % & $ + % \begin{array}[c]{l} + % \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}, \wildcard{B}{U'}{L'}} \vdash C \cup \, \set{ \rwildcard{A} \doteq \rwildcard{B} } \\ + % \hline + % \vspace*{-0.4cm}\\ + % \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}, \wildcard{B}{U'}{L'}} \vdash C \cup \, \set{ \type{L} \doteq \type{U} , \type{U} \doteq \type{U'}, \type{L} \doteq \type{L'} } + % \end{array} + % $ + % \\\\ + \rulename{Upper} + & $ + \begin{array}[c]{l} + \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdot \type{T} } \\ + \hline + \vspace*{-0.4cm}\\ + \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdot \type{T} } + \end{array} + $ + \\\\ + \rulename{Lower} + & $ + \begin{array}[c]{l} + \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{T} \lessdot \type{A} } \\ + \hline + \vspace*{-0.4cm}\\ + \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{T} \lessdot \type{L} } + \end{array} + $ + \\\\ + \rulename{Bot} + & $ + \begin{array}[c]{l} + \wildcardEnv \vdash C \cup \set{ \bot \lessdot \type{T} } \\ + \hline + \vspace*{-0.4cm}\\ + \wildcardEnv \vdash C + \end{array} + $ + \\\\ + \rulename{Pit} + & $ + \begin{array}[c]{l} + \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \bot } \\ + \hline + \vspace*{-0.4cm}\\ + \wildcardEnv \vdash C \cup \set{ \tv{a} \doteq \bot } + \end{array} + $ + \\\\ +\end{tabular}} +\end{center} +\caption{Wildcard reduce rules}\label{fig:wildcard-rules} +\end{figure} + +\begin{figure} + \begin{center} + \leavevmode + \fbox{ + \begin{tabular}[t]{l@{~}l} +\rulename{normalize} + & $ + \begin{array}[c]{l} + \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}, \wildcard{B}{U'}{L'}} \vdash C \cup \, \set{ \rwildcard{A} \doteq \rwildcard{B} } \\ + \hline + \vspace*{-0.4cm}\\ + \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}, \wildcard{B}{U'}{L'}} \vdash C \cup \, \set{ \type{L} \doteq \type{U} , \type{U'} \doteq \type{L'}, \type{U} \doteq \type{U'} } + \end{array} \quad + \text{fv}(\type{U}, \type{U'}, \type{L}, \type{L'}) = \emptyset + $ + \\\\ +\rulename{Tame} + & $ + \begin{array}[c]{l} + \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}} \vdash C \cup \, \set{ \rwildcard{A} \doteq \type{T} } \\ + \hline + \vspace*{-0.4cm}\\ + \wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}} \vdash C \cup \, \set{ \type{L} \doteq \type{T}, \type{U} \doteq \type{T} } + \end{array} \quad \text{fv}(\type{U}, \type{L}) = \emptyset + $ + \\\\ + % \rulename{Equals} %TODO + % & $ + % \begin{array}[c]{l} + % \wildcardEnv \vdash C \cup \, \set{ \type{N} \doteq \type{N'} } \\ + % \hline + % \vspace*{-0.4cm}\\ + % \wildcardEnv \vdash C \cup \, + % \set{ + % \type{N} \lessdot \type{N'}, \type{N'} \lessdot \type{N} + % } + % \end{array} \quad \text{fv}(\type{N}) = \text{fv}(\type{N'}) = \emptyset + % $ + % \\\\ + \rulename{Equals} %TODO + & $ + \begin{array}[c]{l} + \wildcardEnv \vdash C \cup \, \set{ \wctype{\Delta}{C}{\ol{T}} \doteq \wctype{\Delta}{C}{\ol{T'}} } \\ + \hline + \vspace*{-0.4cm}\\ + \wildcardEnv \vdash C \cup \, + \set{ + % \pi(\ol{T}) \doteq \pi(\ol{T'} ) + \ol{T} \doteq \ol{T'} + } + \end{array} +% \quad \begin{array}{l} +% \text{given a permutation}\ \pi\ \text{with:}\\ +% \pi(\Delta) = \pi(\Delta') +% \end{array} + $ + \\\\ + \rulename{Erase} + & $ + \begin{array}[c]{l} + \wildcardEnv \vdash C \cup \, \set{ \type{T} \doteq \type{T} } \\ + \hline + \vspace*{-0.4cm}\\ + \wildcardEnv \vdash C + \end{array} + $ + \\\\ + \rulename{Erase} + & $ + \begin{array}[c]{l} + \wildcardEnv \vdash C \cup \, \set{ \type{T} \lessdot \type{T} } \\ + \hline + \vspace*{-0.4cm}\\ + \wildcardEnv \vdash C + \end{array} + $ + \\\\ + \rulename{Swap} & $ + \begin{array}[c]{l} + \wildcardEnv \vdash C \cup \set{\type{G} \doteq \tv{a}}\\ + \hline + \wildcardEnv \vdash C \cup \set{\tv{a} \doteq \type{G}} + \end{array} + \quad + \begin{array}[c]{l} + \wildcardEnv \vdash C \cup \set{\type{G} \doteq \wtv{a}}\\ + \hline + \wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \type{G}} + \end{array} \quad + \begin{array}[c]{l} + \wildcardEnv \vdash C \cup \set{\type{N} \doteq \rwildcard{A}}\\ + \hline + \wildcardEnv \vdash C \cup \set{\rwildcard{A} \doteq \type{N}} + \end{array}$ + \\\\ +\rulename{Circle} & $ +\begin{array}[c]{l} + \wildcardEnv \vdash C \cup \, \set{\tv{a}_1 \lessdot + \tv{a}_2, \tv{a}_2 \lessdot \tv{a}_3, \dots, \tv{a}_n \lessdot \tv{a}_1}\\ + \hline + \wildcardEnv \vdash C \cup \, \set{\tv{a}_1 \doteq \tv{a}_2, \tv{a}_2 \doteq \tv{a}_3, \dots , \tv{a}_n \doteq \tv{a}_1} +\end{array} \quad n>0 + $ +\end{tabular}} +\end{center} +\caption{Constraint normalize rules}\label{fig:normalizing-rules} +\end{figure} + +The \rulename{match} rule generates fresh wildcards $\overline{\wildcard{A}{\tv{u}}{\tv{l}}}$. +Their upper and lower bounds are fresh type variables. + +%Unify only renames the wildcards in the reduce rule +% It's the only place where wildcards are coming into play (theres always a reduce step before a wildcard substitution is possible) + + +% die wildcard variablen sollten erst am Ende ausgetauscht werden gegen normale variablen +% das funktioniert, da die im Reduce step erstellten direkt substituiert werden +% die anderen erlauben Capture Conversion aber nur wenn der Methodentyp und Parametertyp schon feststeht! (gleich Mächtig wie TI in Java) +% a? <. T -> +% T <. a? -> +% a? =. T -> substitute! +% bei normalen Typvariablen werden keine Wildcards substituiert + +% \begin{tcolorbox} +% $ +% \wctype{\rwildcard{X}}{Box}{\rwildcard{X}} \lessdot \exptype{Box}{\tv{a}_?}, \\ +% \exptype{Box}{\tv{a}_?} \lessdot \wctype{\rwildcard{X}}{Box}{\rwildcard{X}} +% $ +% \end{tcolorbox} + +\begin{figure} +\begin{center} + \fbox{ + \begin{tabular}[t]{l@{~}l} + \rulename{Remove} + & $ + \begin{array}[c]{@{}ll} + \begin{array}[c]{l} + \wildcardEnv \vdash C \\ + % \cup \, \set{ \wtv{a} \lessdot \type{T} }\\ + \hline + \vspace*{-0.4cm}\\ +\wildcardEnv \vdash [\tv{a}/\wtv{a}]C + \end{array} + &\begin{array}[c]{l} + \wtv{a} \in C \\ + \tv{a} \ \text{fresh} + \end{array} + \end{array} + $ + \\\\ + % \rulename{Trim} + % & $ + % \begin{array}[c]{@{}ll} + % \begin{array}[c]{l} + % \wildcardEnv \vdash C + % \cup \, \set{ \wcNtype{\Delta}{N} \lessdot \wctype{\Delta', \wildcard{B}{\type{U}}{\type{L}}}{C}{\ol{S}} }\\ + % \hline + % \vspace*{-0.4cm}\\ + % C \cup \, \set{ \wcNtype{\Delta}{N} \lessdot \wctype{\Delta'}{C}{\ol{S}} } + % \end{array} + % &\begin{array}[c]{l} + % \rwildcard{B} \notin \ol{S} + % \end{array} + % \end{array} + % $ + % \\\\ + \end{tabular}} + \end{center} +\caption{Wildcard variable substitution rules}\label{fig:wtv-rules} +\end{figure} + +\begin{figure} + \begin{center} + \leavevmode + \fbox{ + \begin{tabular}[t]{l@{~}l} + \rulename{Match} + & $ + \begin{array}[c]{@{}ll} + \begin{array}[c]{l} + \wildcardEnv \vdash C \cup \, \set{ + \tv{a} \lessdot \wctype{\Delta}{D}{\ol{T}}, \tv{a} \lessdot \wctype{\Delta'}{D'}{\ol{T'}} }\\ + \hline + \vspace*{-0.4cm}\\ +\wildcardEnv \vdash C \cup \, \left\{ \begin{array}[c]{l} + \tv{a} \lessdot \wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}}, + \ol{\tv{l}} \lessdot \ol{\tv{u}}, \\ + \wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}} + \lessdot \wctype{\Delta}{D}{\ol{T}}, \\ + \wctype{\overline{\wildcard{A}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{A}}} + \lessdot \wctype{\Delta'}{D'}{\ol{T'}} +\end{array} +\right\} + \end{array} + &\begin{array}[c]{l} + \text{fresh}\ \overline{\wildcard{A}{\tv{u}}{\tv{l}}} \\ + \type{C} \ll \type{D}\\ + \type{C} \ll \type{D'} % TODO: THe match rule has to pick the most general type for C + \end{array} + \end{array} + $ + \\\\ + \ruleReduceWC{} + & + $ + \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}}, + \ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\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} + $ + \\\\ + \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}} \lessdot \wctype{\Delta}{C}{\ol{T}} } \\ + \hline + \vspace*{-0.4cm}\\ + \wildcardEnv \cup \overline{\wildcard{C}{\type{U'}}{\type{L'}}} + \vdash C \cup \, \set{ + [\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} \lessdot \wctype{\Delta}{C}{\ol{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} + $ + \\\\ + \rulename{Adopt} + & $ + \begin{array}[c]{@{}ll} + \begin{array}[c]{l} + \wildcardEnv \vdash C \cup \, \set{ + \tv{b} \lessdot \tv{a}, +\tv{a} \lessdot \type{N}, \tv{b} \lessdot \type{N'}} \\ + \hline + \vspace*{-0.4cm}\\ + \wildcardEnv \vdash C \cup \, \set{ + \tv{b} \lessdot \type{N}, + \tv{b} \lessdot \tv{a}, +\tv{a} \lessdot \type{N} , \tv{b} \lessdot \type{N'} + } + \end{array} + \end{array} + $ + \\\\ + \rulename{Adapt} + & + $ + \begin{array}[c]{@{}ll} + \begin{array}[c]{l} + \wildcardEnv \vdash C \cup \, \set{ \wctype{\Delta}{C}{\ol{T}} \lessdot + \wctype{\Delta'}{D'}{\ol{T'}} } \\ + \hline + \vspace*{-0.4cm}\\ + \wildcardEnv \vdash C \cup \, \set{ \wctype{\Delta}{D}{[\ol{\type{T}}/\ol{X}]\ol{S}} \lessdot \wctype{\Delta'}{D'}{\ol{T'}} } + + \end{array} + & \begin{array}[c]{l} + \type{C} \ll \type{D'} \\ + \texttt{class} \ \exptype{C}{\ol{X} \triangleleft \ol{N}} \triangleleft \exptype{D}{\ol{S}} + \end{array} + \end{array} + $ + \end{tabular}} + \end{center} +\caption{Constraint reduce rules}\label{fig:reduce-rules} +\end{figure} + +The new constraint generated by the adopt rule may be eliminated by the match rule. +The adopt rule still needs to be applied only once per constraint. + +Wildcards consist out of three parts. +A name, a scope and a upper and lower bound. + +% The \unify{} algorithm from \cite{plue09_1} substitutes type variables with wildcards. +% A constraint $\wctype{\wildcard{X}{\type{Object}}{\bot}}{C}{\rwildcard{X}} \lessdot \exptype{C}{\tv{a}}$ +% has no solution. +% Replacing the type variable $\tv{a}$ with the wildcard $\rwildcard{X}$ is not correct! +% The wildcard $\rwildcard{X}$ cannot leave its scope and the type $\exptype{C}{\rwildcard{X}}$ +% is considered invalid. + +Wildcards are not reflexive. A box of type $\wctype{\rwildcard{X}}{Box}{\rwildcard{X}}$ +is able to hold a value of any type. It could be a $\exptype{Box}{String}$ or a $\exptype{Box}{Integer}$ etc. +Also two of those boxes do not necessarily contain the same type. +But there are situations where it is possible to assume that. +For example the type $\wctype{\rwildcard{X}}{Pair}{\exptype{Box}{\rwildcard{X}}, \exptype{Box}{\rwildcard{X}}}$ +is a pair of two boxes, which always contain the same type. +Inside the scope of the \texttt{Pair} type, the wildcard $\rwildcard{X}$ stays the same. + +The algorithm starts with an empty wildcard environment $\wildcardEnv{}$. +Only the reduce rule adds wildcards to that environment. +And every added wildcard gets a fresh unique name. +This ensures the wildcard environment $\wildcardEnv{}$ never +gets the same wildcard twice. + +When a new type is generated by the \unify{} algorithm it always has the form +$\wctype{\ol{\rwildcard{A}}}{C}{\ol{\rwildcard{A}}}$. + +\textbf{Step 1:} +Apply the rules depicted in the figures \ref{fig:normalizing-rules}, \ref{fig:reduce-rules} and \ref{fig:wildcard-rules} exhaustively. +Starting with the \rulename{circle} rule. Afterwards the other rules in figure \ref{fig:normalizing-rules}. + +The first step of the algorithm is able to remove wildcards. +Removing a wildcard works by setting its lower and upper bound to be equal. +(Def: $\type{Object} = \wildcard{A}{Object}{Object}$). +The \rulename{Equals} rule is responsible for this. + +\textbf{Example:} +\begin{displaymath} + \begin{array}[c]{@{}ll} + \begin{array}[c]{l} + \wildcardEnv \cup \set{ \wildcard{X}{\tv{u}}{\tv{l}} } \vdash + C \cup \, \set{ \type{Object} \doteq \type{X}, \tv{l} \lessdot \tv{u} } \\ + \hline + \vspace*{-0.4cm}\\ + \wildcardEnv \cup \set{ \wildcard{X}{\tv{u}}{\tv{l}} } \vdash C \cup \, + \set{\type{Object} \lessdot \type{X}, \type{X} \lessdot \type{Object}, \tv{l} \lessdot \tv{u} + }\\ + \hline + \vspace*{-0.4cm}\\ + \wildcardEnv \cup \set{ \wildcard{X}{\tv{u}}{\tv{l}} } \vdash C \cup \, + \set{\type{Object} \lessdot \tv{l}, \tv{u} \lessdot \type{Object}, \tv{l} \lessdot \tv{u} + }\\ + \hline + \vspace*{-0.4cm}\\ + \ldots\\ + \hline + \vspace*{-0.4cm}\\ + \wildcardEnv \cup \set{ \wildcard{X}{\type{Object}}{\type{Object}} } \vdash C \\ + \end{array} + \end{array} +\end{displaymath} + +\begin{description} +\item [$\ll$ relation:] +The $\ll$ relation is the reflexive and transitive closure of the \texttt{extends} relations: +\begin{displaymath} + \begin{array}[c]{c} +\exptype{C}{\ol{X} \triangleleft \ol{N}} \triangleleft \exptype{D}{\ol{N}} \\ +\hline +\vspace*{-0.4cm}\\ +\texttt{C} \ll \texttt{D} +\end{array} +\quad +\begin{array}[c]{l} + \\ +\hline +\vspace*{-0.4cm}\\ +\texttt{C} \ll \texttt{C} +\end{array} +\quad +\begin{array}[c]{l} +\texttt{C} \ll \texttt{D}, \texttt{D} \ll \texttt{E} \\ +\hline +\vspace*{-0.4cm}\\ +\texttt{C} \ll \texttt{E} +\end{array} +\end{displaymath} +The algorithm uses it to determine if two types are possible subtypes of one another. +This is needed in the \rulename{adapt} and \rulename{match} rules. + +%\textbf{Wildcard renaming}\\ +\item[Wildcard renaming:] +The \rulename{reduce} rule separates wildcards from their environment. +At this point each wildcard gets a new and unique name. +To only rename the respective wildcards the reduce rule renames wildcards up to alpha conversion: +($[\ol{C}/\ol{B}]$ in the \rulename{reduce} rule) +\begin{align*} + [\type{A}/\type{B}]\type{B} &= \type{A} \\ + [\type{A}/\type{B}]\type{C} &= \type{C} & \text{if}\ \type{B} \neq \type{C}\\ + [\type{A}/\type{B}]\wcNtype{\Delta}{N} &= \wcNtype{\Delta}{[\type{A}/\type{B}]N} & \text{if}\ \type{B} \notin \Delta \\ + [\type{A}/\type{B}]\wcNtype{\Delta}{N} &= \wcNtype{\Delta}{N} & \text{if}\ \type{B} \in \Delta \\ +\end{align*} + +\item[Free Variables:] +The $\text{fv}$ function assumes every wildcard type variable to be a free variable aswell. + +%\textbf{Fresh Wildcards}\\ +\item[Fresh Wildcards:] +$\text{fresh}\ \overline{\wildcard{A}{\tv{u}}{\tv{l}}}$ generates fresh wildcards. +The new names $\ol{A}$ are fresh, aswell as the type variables $\ol{\tv{u}}$ and $\ol{\tv{l}}$, +which are used for the upper and lower bounds. +\end{description} +% \noindent +% \textbf{Example: (reduce-rule)} +% %The \ruleReduceWC{} resembles the \texttt{S-Exists} subtyping rule. +% %It converts wildcard types to fresh type variables. +% %For example take the input constraint $\exptype{Pair}{\ntype{Object},\tv{b}} \lessdot \wctype{\wildcard{A}{\tv{c}}{\tv{d}}}{Pair}{\wildcard{A}{\tv{c}}{\tv{d}},\wildcard{A}{\tv{c}}{\tv{d}}}$. +% %First we apply the \ruleReduceWC{} rule, which replaces $\wildcard{A}{\tv{c}}{\tv{d}}$ with a fresh type variable $\tv{a}$: +% We assume the input constraints $C = \exptype{Pair}{\ntype{Object},\tv{b}} \lessdot \wctype{\wildcard{A}{\tv{c}}{\tv{d}}}{Pair}{\wildcard{A}{\tv{c}}{\tv{d}},\wildcard{A}{\tv{c}}{\tv{d}}}$. +% The type on the right side $\wctype{\wildcard{A}{\tv{c}}{\tv{d}}}{Pair}{\wildcard{A}{\tv{c}}{\tv{d}},\wildcard{A}{\tv{c}}{\tv{d}}}$ +% \begin{align*} +% \ddfrac{ +% \exptype{Pair}{\ntype{Object},\tv{b}} \lessdot \wctype{\wildcard{A}{\tv{c}}{\tv{d}}}{Pair}{\wildcard{A}{\tv{c}}{\tv{d}},\wildcard{A}{\tv{c}}{\tv{d}}} +% }{ +% \ntype{Object} \doteq \tv{a}, \tv{b} \doteq \tv{a}, \tv{a} \lessdot \tv{c}, \tv{d} \lessdot \tv{a} +% } \ruleReduceWC{} +% \end{align*} + +% By substition we get the result: % $\tv{a} \doteq \type{Object}$, $\tv{a} \doteq \type{Object}$, $\ldots$. + +% \begin{align*} +% \ddfrac{ +% \ntype{Object} \doteq \tv{a}, \tv{b} \doteq \tv{a}, \tv{a} \lessdot \tv{c}, \tv{d} \lessdot \tv{a} +% }{ +% \tv{a} \doteq \ntype{Object} , \tv{b} \doteq \ntype{Object}, \ntype{Object} \lessdot \tv{c}, \tv{d} \lessdot \ntype{Object} +% } \rulename{Subst} +% \end{align*} +% \\[1em] + +\noindent +\textbf{Step 2:} +%If there are no $(\type{T} \lessdot \tv{a})$ constraints remaining in the constraint set $C$ +%resume with step 4. + +The rules in figure \ref{fig:step2-rules} offer multiple possibilities to deal with constraints of the form $\type{N} \lessdot \tv{a}$. +This builds a search tree over multiple possible solutions. +\unify{} has to try each branch and accumulate the resulting solutions into a solution set. + +\begin{figure} +\begin{center} + \fbox{ + \begin{tabular}[t]{l@{~}l} + \rulename{\generalizeRule} + & $ + \begin{array}[c]{l} + \wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \tv{a}\\ + \hline + \wildcardEnv \vdash C \cup \set{\wctype{\Delta}{C}{\ol{T}} \lessdot \tv{a}, + \tv{a} \doteq \wctype{\overline{\wildcard{X}{\tv{u}}{\tv{l}}}}{C}{\overline{\rwildcard{X}}}, + %\overline{\tv{l} \lessdot \tv{u}}, % not needed, due to subst and reduce rule which are used afterwards + \overline{\tv{u} \lessdot \type{S}} + } + \end{array} \quad \begin{array}[c]{l} + \texttt{class} \ \exptype{C}{\ol{X \triangleleft \type{S}}} \triangleleft \exptype{D}{\ol{N}} \\ + \text{fresh}\ \overline{\wildcard{X}{\tv{u}}{\tv{l}}} + \end{array} + $ + \\\\ + \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}} \triangleleft \exptype{D}{\ol{N}} \\ + \ol{X} \notin \wildcardEnv \cup \Delta + \end{array} + $ + \\\\ + \rulename{Settle} + & $ + \begin{array}[c]{l} + \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N}, + \tv{a} \lessdot^* \tv{b}} + \\ + \hline + \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot^* \tv{b}, \tv{b} \lessdot \type{N} } + \end{array} + $ + \\\\ + \rulename{Raise} + & $ + \begin{array}[c]{l} + \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N}, + \tv{a} \lessdot \tv{b}} + \\ + \hline + \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b} } + \end{array} + $ + \\\\ + \end{tabular}} + \end{center} +\caption{Step 2 branching: Multiple rules can be applied to the same constraint} +\label{fig:step2-rules} +\end{figure} + + +%For every $\type{T} \lessdot \tv{a}$ constraint, the unify algorithm has to consider every possible supertype of $\type{T}$. +%For every $\type{N}$ with $\type{T} \leq \type{N}$: ($\texttt{class} \ \exptype{T}{\ol{Y} \triangleleft \ol{N}} \triangleleft \type{N}$) +%There are two different ways of handling a $\type{T} \lessdot \tv{a}$ constraint: +%TODO: why the \generalizeRule is basically the Same rule for regular type placeholders + +% Replacing regular type placeholders causes problems related to method calls and capture conversion. + +% List same(List a, List b){} + +% \begin{lstlisting} +% List f; +% List problem(){ +% return same(problem(), problem()) ?: f; +% } +% \end{lstlisting} +% \begin{constraints} +% r <. List +% r <. List +% X.List <. r +% \end{constraints} +% %TODO + +\unify{} generates wildcard types for constraints of the form $\type{N} \lessdot \tv{a}$ with the \rulename{\generalizeRule} rule. +Otherwise only the wildcards already defined in the input constraints will be included in the result. +\rulename{\generalizeRule} attempts to give $\tv{a}$ a more general type by replacing only the type parameters with fresh wildcards. +The second variation sets $\tv{a}$ to the direct supertype of type \texttt{C}. +For the constraint $\texttt{Object} \lessdot \tv{a}$ the algorithm can only apply $\tv{a} \doteq \texttt{Object}$, +because \texttt{Object} has no other supertype than itself. + +Constraints of the form $\set{ \tv{a} \lessdot \type{N}, \tv{a} \lessdot^* \tv{b}}$ +need to be handled in a similiar fashion. +The type variable $\tv{b}$ could either be a sub or a supertype of the type $\type{N}$. +We have to consider both possibilities. +\\[1em] +% The specification of the \unify{} algorithm has only two rules generating $\doteq$-Constraints +% , \rulename{Reduce} and \rulename{Ground}. +% $\doteq$-Constraints and the accompaning substitutions are dangerous respective to the soundness of the algorithm. +% For the soundness proof of the \unify{} algorithm we have to show every generation of equals constraints +% and the subsequent application of the \rulename{subst} rule is correct. +% We try to use them as sparsely as possible to simplify the soundness proof. +% You can notice this at \rulename{Equals} or \rulename{Force}: +% Instead of setting $\type{U} \doteq \type{L}$, we say +% $\type{U} \lessdot \type{L}, \type{L} \lessdot \type{U}$. + +\noindent +\textbf{Step 3} +\textbf{(Eliminate Wildcard Variables):} +If no more rules in step 2 are applicable \unify{} has to eliminate all wildcard variables +and start over at step 1. +If $C$ does not contain any wildcard variables the algorithm proceeds with step 4. + +We apply the \rulename{Clean} rule exhaustively to $C''$: +\begin{gather*} + \begin{array}[c]{lll} + \rulename{Clean} & +\begin{array}[c]{l} + \wildcardEnv \vdash C\\ + \hline + [\tv{a}/\wtv{a}]\wildcardEnv, [\tv{a}/\wtv{a}]\sigma \vdash [\tv{a}/\wtv{a}]C %\cup \set{\tv{b} \doteq \tv{a}} +\end{array} +\quad \wtv{a} \in C +\end{array} +\end{gather*} + +% \begin{gather*} +% \begin{array}[c]{lll} +% \rulename{Subst} & +% \begin{array}[c]{l} +% \wildcardEnv \vdash C \cup \set{\tv{a} \doteq \wctype{\triangle}{C}{\ol{T}}}\\ +% \hline +% [\wctype{\triangle}{C}{\ol{T}}/\tv{a}]\wildcardEnv \vdash [\wctype{\triangle}{C}{\ol{T}}/\tv{a}] +% C \cup \set{\tv{a} \doteq \wctype{\triangle}{C}{\ol{T}}} +% \end{array} +% & \tv{a} \notin \ol{T} \\ +% & \\ +% \rulename{Subst-wc} & +% \begin{array}[c]{l} +% \wildcardEnv \vdash C \cup \set{\tv{a} \doteq \rwildcard{A}}\\ +% \hline +% [\rwildcard{A}/\tv{a}]\wildcardEnv \vdash [\rwildcard{A}/\tv{a}] C \cup \set{\tv{a} \doteq \rwildcard{A}} +% \end{array} +% \end{array} +% \end{gather*} + +%or $\type{T}$ is not of the form $\wctype{\triangle}{C}{\ol{G}}$ with $\text{fv}(\ol{G}) = \emptyset$. +%Here the $\text{fv}(\ol{G})$ also applies to type variables. +%$\tv{x} \doteq \exptype{C}{\tv{a}}$ is invalid, because $\tv{a}$ could become a free wildcard in that context. + +\noindent +\textbf{Step 4:} +We apply the rules in figure \ref{fig:cleanup-rules} exhaustively and proceed with step 5. +%and start over at step 1. +%If the constraint set is in solved form afterwards the algorithm proceeds with step 5. + +\begin{figure} + \begin{center} + \leavevmode + \fbox{ + \begin{tabular}[t]{l@{~}l} + \rulename{SubElim} + & $\begin{array}[c]{l} + \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \tv{b}}\\ + \hline + [\tv{a}/\tv{b}]\wildcardEnv \vdash [\tv{a}/\tv{b}]C \cup \set{ \tv{b} \doteq \tv{a} } + \end{array} + $ + \\\\ +\rulename{Ground} +& $\begin{array}[c]{@{}ll} +\begin{array}[c]{l} + \wildcardEnv \cup \overline{\set{\wildcard{X}{\type{U}}{\tv{a}}}} \vdash C \cup \, \set{ + \overline{\tv{a} \lessdot \type{T}} } \\ +\hline +\vspace*{-0.4cm}\\ +\wildcardEnv \cup \overline{\set{\wildcard{X}{\type{U}}{\bot}}} \vdash +C \cup \set{ \tv{a} \doteq \bot } +\end{array} +&\begin{array}[c]{l} +%\forall \wctype{\Delta}{C}{\ol{T}} \in C: \tv{a} \notin \ol{T} \\ +\tv{a} \notin C, \, \rwildcard{X} \notin C, \, \tv{a} \notin \overline{T} %\\ +%\text{length}( \overline{\tv{a} \lessdot \type{T}} ) > 1 +\end{array} +\end{array}$ +\\\\ +\rulename{Crunch} +& $\begin{array}[c]{@{}ll} +\begin{array}[c]{l} +\wildcardEnv \vdash C \cup \, \set{ \tv{a} \doteq \wctype{\Delta', \set{\overline{\wildcard{X}{\type{U}}{\type{L}}}}}{C}{\ol{S}} } \\ +\hline +\vspace*{-0.4cm}\\ +\wildcardEnv \vdash +C \cup \set{ \tv{a} \doteq \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}} +\end{array} +&\begin{array}[c]{l} + \ol{U} = \ol{L} +\end{array} +\end{array}$ +\\\\ +\rulename{Crunch} +& $\begin{array}[c]{@{}ll} +\begin{array}[c]{l} +\wildcardEnv \vdash C \cup \, \set{ \tv{a} \lessdot \wctype{\Delta', \set{\overline{\wildcard{X}{\type{U}}{\type{L}}}}}{C}{\ol{S}} } \\ +\hline +\vspace*{-0.4cm}\\ +\wildcardEnv \vdash +C \cup \set{ \tv{a} \lessdot \wctype{\Delta'}{C}{[\ol{U}/\ol{X}]\ol{S}}} +\end{array} +&\begin{array}[c]{l} + \ol{U} = \ol{L} +\end{array} +\end{array}$ +% \\\\ % The force rule is unnecessary because every type placeholder has an upper bound Object (a <. Object) The match rule eliminates those wildcards +% \rulename{Force} &$ +% \begin{array}[c]{@{}ll} +% \begin{array}[c]{l} +% \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} +% \vdash C \cup \, \set{ +% \tv{a} \lessdot \type{N} } \\ +% \hline +% \vspace*{-0.4cm}\\ +% \wildcardEnv +% \vdash +% C \cup \, \set{ \tv{a} \lessdot [\type{U}/\rwildcard{X}]\type{N}, +% \type{U} \doteq \type{L} } +% \end{array} +% &\begin{array}[c]{l} +% \type{X} \in \text{fv}(\type{N}) \\ +% %\Delta' = \Delta \cup \set{\wildcard{X}{\type{U}}{\type{L}}} +% \end{array} +% \end{array}$ +% \\\\ +% \rulename{FlatOut} &$ +% \begin{array}[c]{@{}ll} +% \begin{array}[c]{l} +% \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} +% \vdash C \cup \, \set{ +% \tv{a} \lessdot \wcNtype{\Delta}{N} } \\ +% \hline +% \vspace*{-0.4cm}\\ +% \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} +% \vdash +% C +% \end{array} +% &\begin{array}[c]{l} +% \type{X} \in \text{fv}(\wcNtype{\Delta}{N}) \\ +% \tv{a} \notin C , \, \tv{a} \notin \wildcardEnv, \tv{a} \notin \sigma +% \end{array} +% \end{array}$ + \end{tabular}} +\end{center} +\caption{Cleanup rules}\label{fig:cleanup-rules} +\end{figure} + +The cleanup step prepares the constraint set for the last step by applying the following concepts: +%Two transformations are done which also help to remove unnecessary types from the solution set. +\begin{description} +\item[Bottom type] +The bottom type $\bot$ is used to generate \texttt{? extends} wildcard definitions. +This is the only possible solution when dealing with multiple upper bounds: +$\tv{a} \lessdot \type{T}, \tv{a} \lessdot \type{S}$ is usually not a correct solution (given $\type{S}$ and $\type{T}$ are no subtypes of eachother). +But if $\tv{a}$ is a lower bound of a wildcard it can be set to $\bot$. +Those constraints only stay in the constraint set after the first step if $\type{S}$ and $\type{T}$ do not have a common subtype. +The \rulename{Ground} rule uses this concept to generate \texttt{extends} Wildcards. + +\item[Eliminating Wildcards] +Wildcards that have the same upper and lower bounds can be removed. +This is done by the \rulename{Crunch} rule. + +\textit{Example:} The type $\wctype{\wildcard{X}{\type{String}}{\type{String}}}{List}{\rwildcard{X}}$ +becomes $\exptype{List}{\type{String}}$. + + +%TODO: The a =. T (with T containing free variables) could be removed here. +% Not needed for the soundness of the algorithm, but handy for the implementation (check this when implementing the algorithm) +\end{description} + +\noindent +\textbf{Step 5 (Generating Result):} +Apply the rules in figure \ref{fig:generation-rules} until $\wildcardEnv = \emptyset$ and $C = \emptyset$. +The resulting $\Delta, \sigma$ is a correct solution. + +For this step to succeed there should only be four kinds of constraints left. +\begin{enumerate} +%\item\label{item:3} $\tv{a} \lessdot \tv{b}$ %, with $a$ and $b$ both isolated type variables +\item $\tv{a} \doteq \tv{b}$ +%\item $\wtv{a} \doteq \type{G}$ +\item\label{item:1} $\tv{a} \lessdot \wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}$, with $\text{fv}(\wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}) = \emptyset$ +\item\label{item:2} $\tv{a} \doteq \wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}$, with $\tv{a} \notin \ol{\type{T}}$ % and $\text{fv}(\wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}) = \emptyset$ +\item\label{item:3} $\tv{a} \doteq \rwildcard{X}$ +\end{enumerate} +% Constraints of the form $\tv{a} \doteq \rwildcard{X}$ are also possible. +% should we add those to the \Delta environment? +% How about removing them completely from the result set? Check with soundness condition + +%Each type placeholder $\tv{a}$ must solely appear on the left side of a constraint. +\unify{} fails if there is any $\tv{a} \doteq \type{T}$ such that $\tv{a}$ occurs in $\type{T}$. +For the cases \ref{item:1}, \ref{item:2}, and \ref{item:3} the placeholder $\tv{a}$ +cannot appear anywhere else in the constraint set. +Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will not be able to process every constraint. + +% After applying the GenDelta and GenSigma rules unifiers $\sigma$ do not contain +% a unifier of the form $\tv{a} \to \tv{b}$. +% Otherwise the found solution is incorrect. +% This only happens if the input constraints contain type variables with no upper bound constraint like $\tv{a} \lessdot \type{N}$. + +% \begin{displaymath} +% \deduction{ +% \wildcardEnv \cup \set{\wildcard{B}{\type{G}}{\type{G'}}} \vdash C \implies \Delta, \sigma +% }{ +% \wildcardEnv \vdash C \implies \Delta \cup \set{\wildcard{B}{\type{G}}{\type{G'}}}, \sigma +% }\quad \text{tph}(\type{G}) = \emptyset, \text{tph}(\type{G'}) = \emptyset, +% \rwildcard{B} \notin \text{dom}(\Delta) +% \quad \rulename{AddDelta} +% \end{displaymath} + +\begin{figure} +\begin{center} + \fbox{ + \begin{tabular}[t]{l@{~}l} + \rulename{GenDelta} + & $ + \deduction{ + \wildcardEnv \vdash C \cup \set{\tv{b} \lessdot \type{N} } \implies \Delta, \sigma + }{ + \wildcardEnv \vdash [\type{B}/\tv{b}]C \implies \Delta \cup \set{\wildcard{B}{\type{N}}{\bot}}, \sigma \cup \set{\tv{b} \to \type{B}} + } \quad + \begin{array}{l} + \text{tph}(\type{N}) = \emptyset, \text{fv}(\type{N}) = \emptyset \\ + \rwildcard{B} \ \text{fresh}, \tv{b} \notin \text{dom}(\sigma) + \end{array} + $ + \\\\ + \rulename{AddSigma} + & $ + \deduction{ + \wildcardEnv \vdash C \cup \set{\tv{a} \doteq \rwildcard{X}} \implies \Delta, \sigma + }{ + \wildcardEnv \vdash C \cup \set{\tv{a} \doteq \rwildcard{X}} \implies \Delta, \sigma + \cup \set{\tv{a} \to \rwildcard{X}} + } + $ + \\\\ + \rulename{GenSigma} + & $ + \deduction{ + \wildcardEnv \vdash C \cup + \set{\tv{a} \doteq \type{T} } \implies \Delta, \sigma + }{ + \wildcardEnv \vdash C \implies \Delta, \sigma \cup + \set{\tv{a} \to \type{T} } + } \quad + \begin{array}{l} + \text{tph}(\type{T}) = \emptyset \\ + \tv{a} \notin \text{dom}(\sigma) + \end{array} + $ + \\\\ + \end{tabular}} + \end{center} +\caption{Generate result} +\label{fig:generation-rules} +\end{figure} + +%TODO: Solved form is obsolete due to GenSigma/GenDelta +% \begin{figure} +% \begin{description} +% \item[Solved form] +% A set $C$ of constraints is in solved form if it only contains +% constraints of the following form: +% \begin{enumerate} +% %\item\label{item:3} $\tv{a} \lessdot \tv{b}$ %, with $a$ and $b$ both isolated type variables +% \item $\tv{a} \doteq \tv{b}$ +% %\item $\wtv{a} \doteq \type{G}$ +% \item\label{item:1} $\tv{a} \lessdot \wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}$, with $\text{fv}(\wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}) = \emptyset$ +% \item\label{item:2} $\tv{a} \doteq \wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}$, with $\tv{a} \notin \ol{\type{T}}$ % and $\text{fv}(\wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}) = \emptyset$ +% \end{enumerate} +% %Each type variable $\tv{a}$ can only appear once on a left side of a constraint. +% In case~\ref{item:1} the type variable $\tv{a}$ must not appear on the left of another constraint. +% In case~\ref{item:2} the type variabel $\tv{a}$ must not appear anywhere else in the constraint set $C$. +% % of the form~\ref{item:1} or~\ref{item:2} or ~\ref{item:3} . +% \end{description} +% \caption{Solved form definition}\label{def:solved-form} +% \end{figure} + +% Wildcards with the same name are interlinked. +% The \ruleReduceWC{} replaces all wildcards with the same name with type variables. +% We also use the fact that wildcards of the same name represent the same type at all times. +% So we can erase them in the \rulename{Same} rule. + +% We have to ensure that every wildcard definition is unique. +% When substituting types, every time a type with wildcard definitions is added somewhere, we have to rename those wildcards. + +%\subsection{Unify as Pseudocode} +% The subst rule can be applied multiple times to the same constraint, but its better to mark the a =. T constraint to do it only once +% The step 3 has to clone the constraint set and the wildcard environment and try every way + +% \section{High-Level rules} +% The \unify{} specification tries to be as simple as possible +% with each rule doing only one simple transformation. +% We define additional transformation rules, which deviate directly from the given algorithm. +% They come to use in the examples section. + +% \begin{figure} +% \begin{center} +% \leavevmode +% \fbox{ +% \begin{tabular}[t]{l@{~}l} +% \rulename{Encase} +% & $ +% \deduction{ +% \wildcardEnv \vdash C \cup \set{ \exptype{C}{\type{T}} \lessdot \wctype{\wildcard{X}{\type{U}}{\type{L}}}{C}{\rwildcard{X}} } +% }{ +% \wildcardEnv \vdash \subst{\type{T}}{\tv{x}}C \cup \set{ \type{T} \lessdot \type{U}, \type{L} \lessdot \type{T} } +% } +% $ +% \\\\ +% \rulename{Flatten} +% & $ +% \deduction{ +% \wildcardEnv \vdash C \cup \set{ \type{T} \lessdot \tv{a}, \tv{a} \lessdot \type{T} } +% }{ +% \wildcardEnv \vdash \subst{\type{T}}{\tv{a}}C \cup \set{ \tv{a} \doteq \type{T} } +% } +% $ +% \\\\ +% \rulename{Assimilate} +% & $ +% \deduction{ +% \wildcardEnv \vdash C \cup \set{\wctype{\wildcard{X}{\tv{u}}{\tv{l}}}{C}{\rwildcard{X}} \lessdot \exptype{C}{\type{T}}, \tv{l} \lessdot \tv{u} } +% }{ +% \wildcardEnv \vdash +% C \cup \set{\tv{u} \doteq \type{T}, \tv{l} \doteq \type{T}} +% } +% $ +% \\\\ +% \rulename{Narrow} +% & +% $\deduction{ +% \wildcardEnv \vdash C \cup \set{ +% \wctype{\wildcard{X}{\type{U}}{\type{L}}}{C}{\rwildcard{X}} \lessdot \wctype{\wildcard{X}{\type{U'}}{\type{L'}}}{C}{\rwildcard{X}} +% } +% }{ +% \wildcardEnv \vdash C \cup \set{ +% \type{L'} \lessdot \type{L}, \type{U} \lessdot \type{U'} +% } +% }$ +% \\\\ +% \rulename{Redeem} +% & +% $\deduction{ +% \wildcardEnv \vdash C \cup \set{\wctype{\Delta}{C}{\rwildcard{X}} \lessdot \wctype{\wildcard{X}{\type{Object}}{\bot}}{C}{\rwildcard{X}}} +% }{ +% \wildcardEnv \vdash C +% }$ +% \\\\ +% \rulename{Standoff} +% & +% $\deduction{ +% \wildcardEnv \cup \set{ \wildcard{X}{\type{U}}{\type{L}}, \wildcard{Y}{\type{U'}}{\type{L'}} } \vdash \rwildcard{X} \doteq \rwildcard{Y} +% }{ +% \wildcardEnv \cup \set{ \wildcard{X}{\type{U}}{\type{L}}, \wildcard{Y}{\type{U'}}{\type{L'}} } \vdash \rwildcard{U} \lessdot \type{L'}, \type{U'} \lessdot \type{L} +% }$ +% \\\\ +% \end{tabular}} +% \end{center} +% \caption{Common transformations}\label{fig:wildcard-rules} +% \end{figure}