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

hange Equals rule. Add explanations

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-02-06 18:04:31 +01:00
parent 98a66bbced
commit f40299a36c
3 changed files with 157 additions and 159 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

81
introduction.tex
View File

@ -17,6 +17,68 @@ In Java this is done implicitly by a process called capture conversion \cite{Jav
The type system in \cite{WildcardsNeedWitnessProtection} makes this process explicit by using \texttt{let} statements.
Our type inference algorithm will accept an input program without let statements and add them where necessary.
We figured the \texttt{let} statements to be obsolete for our use case.
Once the type inference algorithm found a correct type solution
\begin{figure}[tp]
\begin{subfigure}[t]{\linewidth}
\begin{lstlisting}[style=fgj]
class List<A> {
List<A> add(A v) { ... }
}
class Example {
m(l, la, lb){
return l
.add(la.add(1))
.add(lb.add("str"));
}
}
\end{lstlisting}
\caption{Java method with missing return type}
\label{fig:nested-list-example-typeless}
\end{subfigure}
~
\begin{subfigure}[t]{\linewidth}
\begin{lstlisting}[style=tfgj]
class List<A> {
List<A> add(A v) { ... }
}
class Example {
m((*@$\exptype{List}{\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}}$@*) l, List<Integer> la, List<String> lb){
return l
.add(la.add(1))
.add(lb.add("str"));
}
}
\end{lstlisting}
\caption{Featherweight Java Representation}
\label{fig:nested-list-example-typed}
\end{subfigure}
~
\begin{subfigure}[t]{\linewidth}
\begin{lstlisting}[style=tfgj]
class List<A> {
List<A> add(A v) { ... }
}
class Example {
m(List<List<? extends Object>> l, List<Integer> la, List<String> lb){
return l
.add(la.add(1))
.add(lb.add("str"));
}
}
\end{lstlisting}
\caption{Java Representation}
\label{fig:nested-list-example-typed}
\end{subfigure}
%\caption{Example code}
%\label{fig:intro-example-code}
\end{figure}
%TODO
% The goal is to proof soundness in respect to the type rules introduced by \cite{aModelForJavaWithWildcards}
% and \cite{WildcardsNeedWitnessProtection}.
@ -59,23 +121,27 @@ In Java this is done implicitly.
%Our type inference algorithm has to add let statements surrounding method invocations.
\begin{figure}[tp]
\begin{subfigure}[t]{0.49\linewidth}
\begin{constraintset}
\begin{subfigure}[t]{\linewidth}
\begin{lstlisting}[style=fgj]
List<? super Integer> ls = ...;
ls.add(new Integer());
List<? super Integer> ls = ...;
ls.add(new Integer());
\end{lstlisting}
\caption{Method invocation}
\label{fig:intro-example-typeless}
\end{subfigure}
~
\begin{subfigure}[t]{0.49\linewidth}
\end{constraintset}
\begin{constraintset}
\begin{subfigure}[t]{\linewidth}
\begin{lstlisting}[style=tfgj]
List<? super Integer> ls = ...;
let x : (*@ $\wctype{\wildcard{X}{\texttt{Object}}{\texttt{Integer}}}{List}{\rwildcard{X}}$ @*) = ls in ls.add(new Integer());
let x : (*@ $\wctype{\wildcard{X}{\texttt{Object}}{\texttt{Integer}}}{List}{\rwildcard{X}}$ @*) = ls in x.add(new Integer());
\end{lstlisting}
\caption{Capture Conversion by \texttt{let}-statement}
\label{fig:intro-example-typed}
\end{subfigure}
\end{constraintset}
\end{figure}
% \subsection{Wildcards}
@ -115,6 +181,7 @@ This paper describes a \unify{} algorithm to solve these constraints and calcula
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
@ -184,8 +251,6 @@ The main challenge was to find an algorithm which computes $\sigma(\tv{a}) = \rw
% A wildcard type is only treated like a wildcard while his definition is in scope (during the reduce rule)
% \subsection{Capture Conversion}
% \begin{verbatim}
% <A> List<A> add(A a, List<A> la) {}

6
soundness.tex
View File

@ -348,7 +348,11 @@ holds with any $\Delta'$ so that $(\text{fv}(\exptype{C}{\ol{S}}) \cup \text{fv}
\item[Circle] S-Refl
\item[Swap] by definition
\item[Erase] S-Refl
\item[Equals] by definition
\item[Equals] %by definition
%TODO
% Unify does never contain wildcard environments with unused wildcards. Therefore after N <: N' and N' <: N, both types have the same wildcard environment
% \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.

229
unify.tex
View File

@ -1,5 +1,50 @@
\section{Unify}\label{sec:unify}
\subsection{Description}
The \unify{} algorithm tries to find a solution for a set of constraints like
$\set{\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}}$.
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}$.
The algorithm works in a recursive fashion.
The input constraints are transformed until they reach a irreducible state,
which the last step of the algorithm eventually transforms into a solution.
A constraint set is convertable to a correct type solution, if it only contains constraints of the form
$\tv{a} \doteq \type{T}$ (where $\tv{a} \notin \text{tph}(\type{T})$) and $\tv{a} \lessdot \type{T}$.
We call this \textit{Solved Form}.
The \unify{} algorithm applies conversions according to the subtyping rules (depicted in figure \ref{fig:subtyping}).
At every step we try to find a reduction, which brings us closer to solved form without excluding any possible solution.
A $\bot \lessdot \type{T}$ constraint is always satisfied and can be ignored. It will be removed by the \rulename{Bot} rule.
For the type placeholder $\tv{a}$ in the constraint $\tv{a} \lessdot \bot$ only the $\bot$ type is a possible substitution,
which is set by the \rulename{Pit} rule.
Example:
$\exptype{List}{\tv{a}} \lessdot \wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$
The \rulename{Reduce} rule converts this to
$\set{\tv{a} \doteq \wtv{x}, \wtv{x} \lessdot \type{Object}, \bot \lessdot \wtv{x} }$.
After applying \rulename{Swap} and \rulename{Subst-WC} on $\tv{a} \doteq \wtv{x}$ we get
$\set{\tv{a} \lessdot \type{Object}, \bot \lessdot \tv{a}}$ and can now apply the \rulename{Bot} rule.
The \rulename{Erase} rule will remove redundant $\type{T} \doteq \type{T}$ constraints.
But what about constraints like $\wctype{\wildcard{X}{\tv{a}}{\tv{b}}}{List}{\rwildcard{X}} \doteq \wctype{\wildcard{Y}{\type{Object}}{\tv{String}}}{List}{\rwildcard{Y}}$
The \rulename{Equals} rule converts this to
% The equals rule is complicated, because
% X.List<X> =. Y.List<Y> -> is the same
% X^String.List<X> =. X.List<X> -> is not!
% T =. T => T <. T
% Special cases: lessdotCC, Normalize/Tame rule,
The $\lessdotCC$ constraints and the wildcard placeholders $\wtv{a}$ are kept as long as possible.
%TODO: Example where lessdotCC constraints get spared until they can be captured
\subsection{Algorithm}
\newcommand{\gtype}[1]{\type{#1}}
%\newcommand{\tw}[1]{\tv{#1}_?}
The \unify{} algorithm computes the type solution.
@ -99,10 +144,10 @@ C \cup \set{\tv{a} \doteq \type{T}}
\\
\rulename{Subst-WC} &$
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \rwildcard{G}}\\
\wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \rwildcard{T}}\\
\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}
[\type{T}/\wtv{a}]\wildcardEnv \vdash [\type{T}/\wtv{a}]C
\end{array} \quad \wtv{a} \notin \type{T}
$
\end{tabular}}
\end{center}
@ -203,37 +248,37 @@ $
\end{array} \quad \text{fv}(\type{U}, \type{L}) \subseteq \Delta_in
$
\\\\
% \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
\rulename{Equals} %TODO
& $
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \, \set{ \wctype{\Delta}{C}{\ol{T}} \doteq \wctype{\Delta}{C}{\ol{T'}} } \\
\wildcardEnv \vdash C \cup \, \set{ \type{N} \doteq \type{N'} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash C \cup \,
\set{
% \pi(\ol{T}) \doteq \pi(\ol{T'} )
\ol{T} \doteq \ol{T'}
\type{N} \lessdot \type{N'}, \type{N'} \lessdot \type{N}
}
\end{array}
\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}
@ -262,9 +307,9 @@ $
\end{array}
\quad
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{\type{G} \doteq \wtv{a}}\\
\wildcardEnv \vdash C \cup \set{\type{T} \doteq \wtv{a}}\\
\hline
\wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \type{G}}
\wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \type{T}}
\end{array} \quad
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{\type{N} \doteq \rwildcard{A}}\\
@ -389,7 +434,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{S}}, \wctype{\Delta'}{C}{\ol{T}}) \subseteq \Delta_{in}
\end{array}
\end{array}
$
@ -469,9 +514,16 @@ $\wctype{\ol{\rwildcard{A}}}{C}{\ol{\rwildcard{A}}}$.
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}.
\begin{figure}
If we find an illicit constraint assigning a type containing free variables to a type placeholder not flagged as a wildcard placeholder the algorithm fails.
$\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \cap \Delta_in \neq \emptyset$ $\implies$ fail!
$\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \cap \Delta_{in} \neq \emptyset$ $\implies$ fail!
% if T <. S with not T << S
% T <. S with fv(T) cup fv(S) not empty (free variables in a non capture conversion constraint)
\caption{Fail conditions}
\end{figure}
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.
@ -975,23 +1027,6 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
\end{array}
$
\\\\
%TODO: make Subst-WC to keep the wildcard flag on variables (the remove rule is not allowed to alter those constraints)
% TODO: change solved-form accordingly
% we can then proof (in soundness for TYPE), that when a constraint a <. T -> X.C<X> <. T , then only variables in X and Delta are used in T
\rulename{AddSigma} %This rule adds the substitutions for a? variables
& $
\deduction{
\wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \type{T}} \implies \Delta, \sigma
}{
\wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \type{T}} \implies \Delta, \sigma
\cup \set{\wtv{a} \to \rwildcard{T}}
} \quad
\begin{array}{l}
\tph(\type{T}) = \emptyset \\
\tv{a} \notin \text{dom}(\sigma)
\end{array}
$
\\\\
\rulename{GenSigma}
& $
\deduction{
@ -1013,112 +1048,6 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
\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}
\subsection{Capture Conversion during Unification}
The \unify{} algorithm applies a capture conversion when needed.
A constraint of the form $\wcNtype{\Delta'}{N} \lessdot \type{T}$,