stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Work in Progress

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-02-14 01:56:35 +01:00
parent 34530270c6
commit c880503ba5
6 changed files with 346 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
TIforWildFJ.tex
View File

@ -35,6 +35,7 @@
\newcommand{\mathcolorbox}[2]{\colorbox{#1}{$\displaystyle #2$}}
\usepackage{cancel}
\usepackage{tcolorbox}
\usepackage{arydshln}
\input{prolog}

98
constraints.tex
View File

@ -9,6 +9,19 @@
%\subsection{Well-Formedness}
The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
At points where a well-formed type is needed we use a normal type placeholder.
Inside a method call expression sub expressions (receiver, parameter) wildcard placeholders are used.
Here captured variables can flow freely.
A normal type placeholder cannot hold types containing free variables.
Normal type placeholders are assigned types which are also expressible with Java syntax.
So no types like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ or $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
Type variables declared in the class header are passed to \unify{}.
Those type variables count as regular types and can be held by normal type placeholders.
There are two different types of constraints:
\begin{description}
@ -140,34 +153,69 @@ The set of method assumptions returned by the \textit{mtypes} function is used t
There are two kinds of method calls.
The ones to already typed methods and calls to untyped methods.
\begin{displaymath}
\begin{array}{@{}l@{}l}
\typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \wtv{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{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdotCC \exptype{C}{\ol{X}},
\overline{\tv{r}} \lessdotCC \ol{T},
\wtv{a} \doteq \type{T},
\ol{X} \lessdot \ol{N},
\ol{Y} \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}
% \begin{displaymath}
% \typeExpr{}' ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a} ) = \
% \typeExpr{} ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \wtv{b} ) \cup \set{ \wtv{b} \lessdot \tv{a}}
% \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{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdot \exptype{C}{\ol{X}},
\overline{\tv{r}} \lessdot \ol{T},
\type{T} \lessdot \tv{a},
\ol{X} \lessdot \ol{N},
\ol{Y} \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}
\typeExpr{}' ({\mtypeEnvironment} , \texttt{return e;}, \tv{a} ) = \
\typeExpr{} ({\mtypeEnvironment} , \texttt{e}, \wtv{b} ) \cup \set{ \wtv{b} \lessdot \tv{a}} \quad \quad \tv{a}, \wtv{b} \ \text{fresh}
\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{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdot \exptype{C}{\ol{X}},
% \overline{\tv{r}} \lessdot \ol{T},
% \type{T} \lessdot \tv{a},
% \ol{X} \lessdot \ol{N},
% \ol{Y} \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:}

8
introduction.tex
View File

@ -163,6 +163,14 @@ List<?> genList() {
\subsection{Global Type Inference}
A global type inference algorithm works on an input with no type annotations at all.
%TODO: Describe global type inference and lateron why it is so hard to
Global type inference means that there are no type annotations at all.
\begin{verbatim}
m(l) {
return l.add(l);
}
\end{verbatim}
$\tv{l} \lessdotCC \exptype{List}{\wtv{x}}, \tv{l} \lessdotCC \wtv{x}$
\subsection{Java Wildcards}
Wildcards are expressed by a \texttt{?} in Java and can be used as parameter types.

37
martin.bib
View File

@ -352,3 +352,40 @@ keywords = {Null, Java Wildcards, Existential Types}
publisher={Addison-Wesley Professional}
}
@inproceedings{semanticWildcardModel,
title={Towards a semantic model for Java wildcards},
author={Summers, Alexander J and Cameron, Nicholas and Dezani-Ciancaglini, Mariangiola and Drossopoulou, Sophia},
booktitle={Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs},
pages={1--7},
year={2010}
}
@inproceedings{addingWildcardsToJava,
title={Adding wildcards to the Java programming language},
author={Torgersen, Mads and Hansen, Christian Plesner and Ernst, Erik and Von Der Ah{\'e}, Peter and Bracha, Gilad and Gafter, Neal},
booktitle={Proceedings of the 2004 ACM symposium on Applied computing},
pages={1289--1296},
year={2004}
}
@article{TamingWildcards,
author = {Tate, Ross and Leung, Alan and Lerner, Sorin},
title = {Taming wildcards in Java's type system},
year = {2011},
issue_date = {June 2011},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {46},
number = {6},
issn = {0362-1340},
url = {https://doi.org/10.1145/1993316.1993570},
doi = {10.1145/1993316.1993570},
abstract = {Wildcards have become an important part of Java's type system since their introduction 7 years ago. Yet there are still many open problems with Java's wildcards. For example, there are no known sound and complete algorithms for subtyping (and consequently type checking) Java wildcards, and in fact subtyping is suspected to be undecidable because wildcards are a form of bounded existential types. Furthermore, some Java types with wildcards have no joins, making inference of type arguments for generic methods particularly difficult. Although there has been progress on these fronts, we have identified significant shortcomings of the current state of the art, along with new problems that have not been addressed.In this paper, we illustrate how these shortcomings reflect the subtle complexity of the problem domain, and then present major improvements to the current algorithms for wildcards by making slight restrictions on the usage of wildcards. Our survey of existing Java programs suggests that realistic code should already satisfy our restrictions without any modifications. We present a simple algorithm for subtyping which is both sound and complete with our restrictions, an algorithm for lazily joining types with wildcards which addresses some of the shortcomings of prior work, and techniques for improving the Java type system as a whole. Lastly, we describe various extensions to wildcards that would be compatible with our algorithms.},
journal = {SIGPLAN Not.},
month = {jun},
pages = {614–627},
numpages = {14},
keywords = {existential types, joins, parametric types, single-instantiation inheritance, subtyping, type inference, wildcards}
}

6
soundness.tex
View File

@ -229,16 +229,18 @@ Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises.
% \end{lemma}
\begin{lemma} \label{lemma:unifyWeakening}
Removing constraints does not render \unify{} impossible.
Removing constraints does not render \unify{} impossible as long as the removed constraints do not share wildcard placeholders.
If there is a solution for a constraint set $C$, then there is also a solution for a subset of that constraint set.
\begin{description}
\item[If] $(\sigma, \Delta) = \unify{}( C \cup C')$
\item[If] $(\sigma, \Delta) = \unify{}( C \cup C')$ and $\text{wtv}(C) \cap \text{wtv}(C') = \emptyset$
\item[then] $ (\sigma', \Delta') = \unify{}( C')$
\end{description}
\end{lemma}
\textit{Proof:}
%TODO
% does this really work. We have to show that the algorithm never gets stuck as long as there is a solution
% maybe there are substitutions with types containing free variables that make additional solutions possible. Check!
\begin{lemma}\label{lemma:unifySoundness}
The \unify{} algorithm only produces correct output.

252
unify.tex
View File

@ -1,6 +1,55 @@
\section{Unify}\label{sec:unify}
%TODO: Remove lessdotC constraints. those have to be handeld during constraint generation
% is capture conversion for methods in the same class unsovable? Can it be reduced to polymorphic recursion?
% the other problem is, that there are infinite subtypes.
% For example for a type X^Infinite<X>.Infinite<X>
% here a correct subtype would be an instantiation of the class Omega extends Infinite<Omega>
The parameter types given to a generic method also affect their return type.
During constraint generation the algorithm does not know the parameter types yet.
We generate $\lessdotCC$ constraints and let \unify{} do the capture conversion.
$\lessdotCC$ constraints are kept until they reach the form $\type{G} \lessdotCC \type{G}$ and a capture conversion is possible.
% A method has infinte possibilities of being called and there is no most general type.
% P<X,Y> m(C<X> c, C<Y> c2)
% depending on
% A.P<A,A> <. A,B.P<A,B>
% % During the method call it is not sure what kind of return type is needed from the method.
% % The method P<A,B> make(A a, B b)
% % The type A,B.P<A,B> cannot be a subtype of P<X,X>
% % But if A^X_X and B^X_X
% % Could a constraint C<X> <. a? be expanded to a? = X^u?_l?.C<X>
% Why is there no most general type?
% - the return type depends on the parameter types
The most general type denotable in Java of a class $\exptype{C}{\ol{X}}$
is $\wctype{\ol{X}}{C}{\ol{X}}$
%Is there a direct subtype of a type N including generics? e.g. a <c C<C<x>>
% AND if yes! why is there not a most generic expression of a method head without the need of Capture Conversion?
% Pair<X,Y> m(List<X> l, List<Y> l2) => X,Y.Pair<X,Y> m()
% X.List<X> <. List<x>
% because we want the most specfic return type and the least specific parameter types!
A method is only equiped with generic parameters if they only appear in a <. T constraints
Polymorphic recursion makes it impossible to infer a generic type who is called in a more specific way.
Is it? Not ours for sure!
The problem is, that we don't know which type is the parameter of the method call.
And a method with a parameter \texttt{List<? extends A>} can have an infinite number of subtypes. %Does it?
% Y.List<Y> <c Z^List<x>.List<Z>
% Y <. List<x>
% X,Y^List<X>.List<Y> <c Z^List<x>.List<Z>
% The idea is to hold out until the left side of a $\lessdotCC$ constraint is known to be a named type
% and then check if the typing is still correct.
The wildcard placeholders are used for intermediat types.
It is not possible to create all super types of a type.
The General rule only creates the ones expressable by Java syntax, which still are infinitly many in some cases \cite{TamingWildcards}.
@ -148,17 +197,29 @@ This is necessary for the \rulename{Equals} rule to work properly.
\leavevmode
\fbox{
\begin{tabular}[t]{l@{~}l}
\rulename{Subst} &
$\begin{array}[c]{l}
\rulename{Subst} &
$\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{\ntv{a} \doteq \type{T}}\\
\hline
[\type{T}/\tv{a}]\wildcardEnv \vdash [\type{T}/\tv{a}]
C \cup \set{\ntv{a} \doteq \type{T}}
\end{array}
\quad \begin{array}{c}
\ntv{a} \notin \type{T} \\
\text{fv}(\type{T}) \subseteq \Delta', \, \text{wtv}(\type{T}) = \emptyset
\end{array}$\\
\\
\rulename{Remove} &
$\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{\ntv{a} \doteq \type{T}}\\
\hline
[\type{T}/\tv{a}]\wildcardEnv \vdash [\type{T}/\tv{a}]
C \cup \set{\ntv{a} \doteq \type{T}}
\end{array}
\quad \begin{array}{c}
\ntv{a} \notin \type{T} \\
\text{fv}(\type{T}) \subseteq \Delta'
\end{array}$\\
\hline
[\ntv{b}/\wtv{b}]\wildcardEnv \vdash [\ntv{b}/\wtv{b}]
C \cup \set{\ntv{a} \doteq [\ntv{b}/\wtv{b}]\type{T}}
\end{array}
\quad \begin{array}{c}
\wtv{b} \in \text{wtv}(\type{T})\\
\ntv{b} \ \text{fresh}
\end{array}$\\
\\
\rulename{Subst-WC} &$
\begin{array}[c]{l}
@ -438,7 +499,8 @@ Their upper and lower bounds are fresh type variables.
\end{array}
$
\\\\
\rulename{Prepare}
\rulename{Prepare} %The lessdotCC constraint only ensures that the left side looses its wildcardEnvironment.
%It does not ensure that the left side doesn't contain free variables. If you want to ensure that you have to give the left side a normal placeholder
&
$
\begin{array}[c]{@{}ll}
@ -452,7 +514,7 @@ Their upper and lower bounds are fresh type variables.
\end{array}
%\quad \ol{Y} = \textit{fresh}(\ol{X})
\quad \begin{array}[c]{l}
\text{fv}(\wctype{\Delta}{C}{\ol{S}}, \wctype{\Delta'}{C}{\ol{T}}) \subseteq \Delta_{in}
\text{fv}(\wctype{\Delta'}{C}{\ol{T}}) \subseteq \Delta_{in}
\end{array}
\end{array}
$
@ -682,6 +744,138 @@ which are used for the upper and lower bounds.
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.
\def\boxit#1#2{%
\smash{\color{red}\fboxrule=1pt\relax\fboxsep=2pt\relax%
\llap{\rlap{\fbox{\phantom{\rule{#1}{#2}}}}~}}\ignorespaces
}
\begin{figure}
\begin{center}
\fbox{
\begin{tabular}[t]{l@{~}l}
\rulename{Same}
& $
\begin{array}[c]{l}
\wildcardEnv \vdash
C \cup \type{G} \lessdot \tv{a}\\
\hline
\wildcardEnv \vdash
C \cup \set{
\tv{a} \doteq \type{G}
}
\end{array} \quad \begin{array}[c]{l}
\text{fv}(\type{G}) \in \Delta_{in}
\end{array}
$
\\\\
\cdashline{1-2} \\
\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}
$
\\\\
\cdashline{1-2} \\
\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,\, \Delta' = \Delta \cap \text{fv}([\ol{T}/\ol{X}]\ol{N})
\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}
\begin{figure}
\begin{center}
\fbox{
\begin{tabular}[t]{l@{~}l}
\rulename{Subst-X}
& $
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
C \cup \rwildcard{X} \lessdot \tv{a}\\
\hline
\wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
C \cup \set{
\tv{a} \doteq \rwildcard{X}
}
\end{array} \quad \begin{array}[c]{l}
\rwildcard{X} \in \Delta_{in}
\end{array}
$
\\\\
\cdashline{1-2} \\
\rulename{Gen-X}
& $
\begin{array}[c]{l}
\wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
C \cup \rwildcard{X} \lessdot \tv{a}\\
\hline
\wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
C \cup \set{
\type{U} \lessdot \tv{a}
}
\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}
\begin{figure}
\begin{center}
\fbox{
\begin{tabular}[t]{l@{~}l}
\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}
$
\\\\
\cdashline{1-2} \\
\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}
\begin{figure}
\begin{center}
@ -845,23 +1039,23 @@ If $C$ does not contain any wildcard variables the algorithm proceeds with step
\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}\\
\subst{\tv{a}}{\wtv{a}}\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{Remove} % kann beim Subst step gemacht werden und ist nur nötig wenn ein a =. T constraint mit wtv(T) > 1 entsteht
% & $
% \begin{array}[c]{@{}ll}
% \begin{array}[c]{l}
% \wildcardEnv \vdash C \\
% % \cup \, \set{ \wtv{a} \lessdot \type{T} }\\
% \hline
% \vspace*{-0.4cm}\\
% \subst{\tv{a}}{\wtv{a}}\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{Remove-Cons} & $
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{\type{S} \lessdotCC \type{T} } \\