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

Final Version and Submission to ESOP Round 1

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-05-31 13:52:18 +02:00
parent 0e157cf427
commit f699cc075f
6 changed files with 292 additions and 340 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

224
conclusion.tex
View File

@ -1,40 +1,14 @@
\section{Properties of the Algorithm}
\begin{itemize}
\item Our algorithm is designed for extensibility with the final goal of full support for Java.
\unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
\end{itemize}
%TODO: how are the challenges solved: Describe this in the last chapter with examples!
\section{Soundness}\label{sec:soundness}
\begin{theorem}\label{testenv-theorem}
Type inference produces a correctly typed program.
\begin{description}
\item[If] $\fjtypeinference(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
\triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \mtypeEnvironment{}'$
\item[Then] $\texttt{class}\ \exptype{C}{\ol{X}
\triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \} \text{ok}$,
with $\ol{M} = $
\end{description}
\end{theorem}
To prove soundness we have to show two things.
The vital parts are method calls and field access.
The generated constraints have to resemble the \TamedFJ{}'s type system.
\section{Completeness}\label{sec:completeness}
\section{Discussion}\label{sec:completeness}
We couldn't verify it with an implementation yet, but we assume atleast the same functionality
as the global type inference algorithm for Featherweight Java without Wildcards \cite{TIforFGJ}.
When it comes to wildcards there is a limitation we couldn't find a good workaround:
\begin{example} This example does not work:
\begin{example} Limitation:
This example does not work:
\begin{minipage}{0.35\textwidth}
\begin{verbatim}
\noindent
\begin{minipage}{0.51\textwidth}
\begin{lstlisting}[style=java]
class Example{
<A> Pair<A,A> make(List<A> l){...}
<A> bool compare(Pair<A,A> p){...}
@ -43,75 +17,46 @@ class Example{
return compare(make(l));
}
}
\end{verbatim}
\end{lstlisting}
\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}
\begin{minipage}{0.48\textwidth}
\begin{lstlisting}[style=constraints]
(*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{x}}$@*),
(*@$\exptype{Pair}{\wtv{x},\wtv{x}} \lessdot \ntv{r}$@*),
(*@$\ntv{r} \lessdot \exptype{Pair}{\wtv{z}, \wtv{z}}$@*)
\end{lstlisting}
\end{minipage}
\end{example}
The algorithm can find a solution to every program which the Unify by Plümicke finds
a correct solution aswell.
It will not infer intermediat type like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X},\rwildcard{X}}$.
There is propably some loss of completeness when capture constraints get deleted.
This happens because constraints of the form $\tv{a} \lessdotCC \exptype{C}{\wtv{x}}$ are kept as long as possible.
Here the variable $\tv{a}$ maybe could hold a wildcard type,
but it gets resolved to a $\generics{\type{A} \triangleleft \type{N}}$.
This combined with a constraint $\type{N} \lessdot \wtv{x}$ looses a possible solution.
%The algorithm can find a solution to every program which the Unify by Plümicke finds
%a correct solution aswell.
We will not infer intermediat types like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X},\rwildcard{X}}$
for a normal type placeholder.
$\ntv{r}$ will get the type $\wctype{\rwildcard{X},\rwildcard{Y}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$
which renders the constraint set unsolvable.
This is our result:
\begin{verbatim}
class List<X> {
<Y extends X> void addTo(List<Y> l){
l.add(this.get());
}
}
\end{verbatim}
$
\tv{l} \lessdotCC \exptype{List}{\wtv{y}},
\type{X} \lessdot \wtv{y}
$
But the most general type would be:
\begin{verbatim}
class List<X> {
void addTo(List<? super X> l){
l.add(this.get());
}
}
\end{verbatim}
% This is our result:
% \begin{verbatim}
% class List<X> {
% <Y extends X> void addTo(List<Y> l){
% l.add(this.get());
% }
% }
% \end{verbatim}
% $
% \tv{l} \lessdotCC \exptype{List}{\wtv{y}},
% \type{X} \lessdot \wtv{y}
% $
% But the most general type would be:
% \begin{verbatim}
% class List<X> {
% void addTo(List<? super X> l){
% l.add(this.get());
% }
% }
% \end{verbatim}
\subsection{Discussion Pair Example}
\begin{verbatim}
<X> Pair<X,X> make(List<X> l){ ... }
<X> boolean compare(Pair<X,X> p) { ... }
List<?> l;
Pair<?,?> p;
compare(make(l)); // Valid
compare(p); // Error
\end{verbatim}
Our type inference algorithm is not able to solve this example.
When we convert this to \TamedFJ{} and generate constraints we end up with:
\begin{lstlisting}[style=tamedfj]
let m = let x = l in make(x) in compare(m)
\end{lstlisting}
\begin{constraintset}$
\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \ntv{x},
\ntv{x} \lessdotCC \exptype{List}{\wtv{a}}
\exptype{Pair}{\wtv{a}, \wtv{a}} \lessdot \ntv{m}, %% TODO: Mark this constraint
\ntv{m} \lessdotCC \exptype{Pair}{\wtv{b}, \wtv{b}}
$\end{constraintset}
$\ntv{x}$ will get the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and
from the constraint
@ -120,63 +65,74 @@ $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
$\exptype{Pair}{\rwildcard{X}, \rwildcard{X}} \lessdot \ntv{m}$.
Finding a supertype to $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ is the crucial part.
The correct substition for $\ntv{m}$ would be $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$.
The correct substition for $\ntv{r}$ would be $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$.
But this leads to additional branching inside the \unify{} algorithm and increases runtime.
%We refrain from using that type, because it is not denotable with Java syntax.
%Types used for normal type placeholders should be expressable Java types. % They are not!
This also just solves this specific issue and not the problem in general.
The prefered way of dealing with this example in our opinion would be the addition of a multi-let statement to the syntax.
\begin{lstlisting}[style=letfj]
let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = l, m = make(x) in compare(make(x))
\end{lstlisting}
% The prefered way of dealing with this example in our opinion would be the addition of a multi-let statement to the syntax.
We can make it work with a special rule in the \unify{}.
But this will only help in this specific example and not generally solve the issue.
A type $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ has atleast two immediate supertypes:
$\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ and
$\wctype{\rwildcard{X}, \rwildcard{Y}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$.
Imagine a type $\exptype{Triple}{\rwildcard{X},\rwildcard{X},\rwildcard{X}}$ already has
% TODO: how many supertypes are there?
%X.Triple<X,X,X> <: X,Y.Triple<X,Y,X> <:
%X,Y,Z.Triple<X,Y,Z>
% \begin{lstlisting}[style=letfj]
% let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = l, m = make(x) in compare(make(x))
% \end{lstlisting}
% TODO example:
\begin{lstlisting}[style=java]
<X> Triple<X,X,X> sameL(List<X> l)
<X,Y> Triple<X,Y,Y> sameP(Pair<X,Y> l)
<X,Y> void triple(Triple<X,Y,Y> tr){}
% We can make it work with a special rule in the \unify{}.
% But this will only help in this specific example and not generally solve the issue.
% A type $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ has atleast two immediate supertypes:
% $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ and
% $\wctype{\rwildcard{X}, \rwildcard{Y}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$.
% Imagine a type $\exptype{Triple}{\rwildcard{X},\rwildcard{X},\rwildcard{X}}$ already has
% % TODO: how many supertypes are there?
% %X.Triple<X,X,X> <: X,Y.Triple<X,Y,X> <:
% %X,Y,Z.Triple<X,Y,Z>
Pair<?,?> p ...
List<?> l ...
% % TODO example:
% \begin{lstlisting}[style=java]
% <X> Triple<X,X,X> sameL(List<X> l)
% <X,Y> Triple<X,Y,Y> sameP(Pair<X,Y> l)
% <X,Y> void triple(Triple<X,Y,Y> tr){}
make(t) { return t; }
triple(make(sameP(p)));
triple(make(sameL(l)));
\end{lstlisting}
% Pair<?,?> p ...
% List<?> l ...
\begin{constraintset}
$
\exptype{Triple}{\rwildcard{X}, \rwildcard{X}, \rwildcard{X}} \lessdot \ntv{t},
\ntv{t} \lessdotCC \exptype{Triple}{\wtv{a}, \wtv{b}, \wtv{b}}, \\
(\textit{This constraint is added later: } \exptype{Triple}{\rwildcard{X}, \rwildcard{Y}, \rwildcard{Y}} \lessdot \ntv{t})
$
% Triple<X,X,X> <. t
% ( Triple<X,Y,Y> <. t ) <- this constraint is added later
% t <. Triple<a?, b?, b?>
% make(t) { return t; }
% triple(make(sameP(p)));
% triple(make(sameL(l)));
% \end{lstlisting}
% t =. x.Triple<X,X,X>
\end{constraintset}
% \begin{constraintset}
% $
% \exptype{Triple}{\rwildcard{X}, \rwildcard{X}, \rwildcard{X}} \lessdot \ntv{t},
% \ntv{t} \lessdotCC \exptype{Triple}{\wtv{a}, \wtv{b}, \wtv{b}}, \\
% (\textit{This constraint is added later: } \exptype{Triple}{\rwildcard{X}, \rwildcard{Y}, \rwildcard{Y}} \lessdot \ntv{t})
% $
% % Triple<X,X,X> <. t
% % ( Triple<X,Y,Y> <. t ) <- this constraint is added later
% % t <. Triple<a?, b?, b?>
% % t =. x.Triple<X,X,X>
% \end{constraintset}
\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.
The problems introduced in the openening \ref{challenges} can be solved via our \unify{} algorithm. %(see examples \ref{example1} and \ref{example2}).
Additionally we could prove that type solutions generated by our type inference algorithm are correct respective to \TamedFJ{}'s type rules.
The important parts are lemma \ref{lemma:soundness} and \ref{lemma:unifySoundness}.
They prove that the \unify{} algorithm solves a constraint set according to our subtyping rules
and that the generated constraints match \TamedFJ{}'s type system.
%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 prove soundness and completeness for \unify{}.
The crucial parts introduced in this paper are capture constraints, wildcard placeholders and existential types.
Those data structures allow us to solve the problems introduced in chapter \ref{challenges}.
%Going further we try to prove soundness and completeness for \unify{}.
Our algorithm is designed for extensibility with the final goal of full support for Java.
\unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
% The tricks are:
% \begin{itemize}

178
constraints.tex
View File

@ -223,98 +223,6 @@ Those type variables count as regular types and can be held by normal type place
\end{array}
\end{array}
\end{displaymath}
\\[1em]
\noindent
\textbf{Example:}
\begin{verbatim}
class Class1{
<A> A head(List<X> l){ ... }
List<? extends String> get() { ... }
}
class Class2{
example(c1){
return c1.head(c1.get());
}
}
\end{verbatim}
%This example comes with predefined type annotations.
We assume the class \texttt{Class1} has already been processed by our type inference algorithm
leading to the following type annotations:
%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}
\texttt{m}: \generics{\type{A} \triangleleft \type{Object}} \
(\type{Class1},\, \exptype{List}{\type{A}}) \to \type{X}, \\
\texttt{get}: (\type{Class1}) \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\rwildcard{A}}
\end{array} \right\}
\end{displaymath}
At first we have to convert the example method to a syntactically correct \TamedFJ{} program.
Afterwards the the \fjtype{} algorithm is able to generate constraints.
\begin{minipage}{0.45\textwidth}
\begin{lstlisting}[style=tamedfj]
class Class2 {
example(c1) = let x = c1 in
let xp = x.get() in x.m(xp);
}
\end{lstlisting}
\end{minipage}%
\hfill
\begin{minipage}{0.5\textwidth}
\begin{constraintset}
$
\begin{array}{l}
\ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}, \\
\ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}, \\
\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{xp}, \\
\tv{xp} \lessdotCC \exptype{List}{\wtv{a}}
\end{array}
$
\end{constraintset}
\end{minipage}
Following is a possible solution for the given constraint set:
\begin{minipage}{0.55\textwidth}
\begin{lstlisting}[style=letfj]
class Class2 {
example(c1) = let x : Class1 = c1 in
let xp : (*@$\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*) = x.get()
in x.m(xp);
}
\end{lstlisting}
\end{minipage}%
\hfill
\begin{minipage}{0.4\textwidth}
\begin{constraintset}
$
\begin{array}{l}
\sigma(\ntv{x}) = \type{Class1} \\
%\tv{xp} \lessdot \exptype{List}{\wtv{x}}, \\
%\exptype{List}{\type{String}} \lessdot \tv{p1}, \\
\sigma(\tv{xp}) = \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \\
\end{array}
$
\end{constraintset}
\end{minipage}
For $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$ to be a correct solution for $\tv{xp}$
the constraint $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{a}}$
must be satisfied.
This is possible, because we deal with a capture constraint.
The $\lessdotCC$ constraint allows the left side to undergo a capture conversion
which leads to $\exptype{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{a}}$.
Now a substitution of the wildcard placeholder $\wtv{a}$ with $\rwildcard{A}$ leads to a satisfied constraint set.
The wildcard placeholders are not used as parameter or return types of methods.
Or as types for variables introduced by let statements.
They are only used for generic method parameters during a method invocation.
Type placeholders which are not flagged as wildcard placeholders ($\wtv{a}$) can never hold a free variable or a type containing free variables.
This practice hinders free variables to leave their scope.
The free variable $\rwildcard{A}$ generated by the capture conversion on the type $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$
cannot be used anywhere else then inside the constraints generated by the method call \texttt{x.m(xp)}.
\begin{displaymath}
\begin{array}{@{}l@{}l}
@ -353,6 +261,92 @@ cannot be used anywhere else then inside the constraints generated by the method
\end{array}
\end{array}
\end{displaymath}
\\[1em]
\noindent
\begin{example}
Given the following input program missing type annotations for the \texttt{example} method:
\begin{lstlisting}[style=java]
class Class1{
<A> A head(List<X> l){ ... }
List<? extends String> get() { ... }
}
class Class2{
example(c1){
return c1.head(c1.get());
}
}
\end{lstlisting}
%This example comes with predefined type annotations.
We assume the class \texttt{Class1} has already been processed by our type inference algorithm
leading to the following type annotations:
%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}
\texttt{m}: \generics{\type{A} \triangleleft \type{Object}} \
(\type{Class1},\, \exptype{List}{\type{A}}) \to \type{X}, \\
\texttt{get}: (\type{Class1}) \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\rwildcard{A}}
\end{array} \right\}
\end{displaymath}
At first we have to convert the example method to a syntactically correct \TamedFJ{} program.
Afterwards the the \fjtype{} algorithm is able to generate constraints.
\noindent
\begin{minipage}{0.52\textwidth}
\begin{lstlisting}[style=tamedfj]
class Class2 {
example(c1) = let x = c1 in
let xp = x.get() in x.m(xp);
}
\end{lstlisting}
\end{minipage}%
\hfill
\begin{minipage}{0.46\textwidth}
\begin{lstlisting}[style=constraints]
(*@$\ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}$@*),
(*@$\ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}$@*),
(*@$\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{xp}$@*),
(*@$\tv{xp} \lessdotCC \exptype{List}{\wtv{a}}$@*)
\end{lstlisting}
\end{minipage}
Following is a possible solution for the given constraint set:
\noindent
\begin{minipage}{0.55\textwidth}
\begin{lstlisting}[style=tamedfj]
class Class2 {
example(c1) = let x :Class1 = c1 in
let xp :(*@$\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*) = x.get()
in x.m(xp);
}
\end{lstlisting}
\end{minipage}%
\hfill
\begin{minipage}{0.43\textwidth}
\begin{lstlisting}[style=constraints]
(*@$\sigma(\ntv{x}) = \type{Class1}$@*),
(*@$\sigma(\tv{xp}) = \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*)
\end{lstlisting}
\end{minipage}
For $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$ to be a correct solution for $\tv{xp}$
the constraint $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{a}}$
must be satisfied.
This is possible, because we deal with a capture constraint.
The $\lessdotCC$ constraint allows the left side to undergo a capture conversion
which leads to $\exptype{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{a}}$.
Now a substitution of the wildcard placeholder $\wtv{a}$ with $\rwildcard{A}$ leads to a satisfied constraint set.
\end{example}
The wildcard placeholders are not used as parameter or return types of methods.
Or as types for variables introduced by let statements.
They are only used for generic method parameters during a method invocation.
Type placeholders which are not flagged as wildcard placeholders ($\wtv{a}$) can never hold a free variable or a type containing free variables.
This practice hinders free variables to leave their scope.
The free variable $\rwildcard{A}$ generated by the capture conversion on the type $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$
cannot be used anywhere else then inside the constraints generated by the method call \texttt{x.m(xp)}.
% Problem:
% <X, A extends List<X>> void t2(List<A> l){}

2
soundness.tex
View File

@ -91,7 +91,7 @@
% TODO:
% \end{lemma}
\begin{lemma}{Soundness:}
\begin{lemma}{Soundness:}\label{lemma:soundness}
\unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
\begin{description}
\item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = (\Delta', C)$

2
tRules.tex
View File

@ -40,7 +40,7 @@ class List<A extends Object> {
\begin{minipage}{0.49\textwidth}
\begin{align*}
&\mathrm{\Pi} = \set{\\
&\texttt{add} : \generics{\ol{A \triangleleft Object}}\ \exptype{List}{\type{A}},\type{A} \to \exptype{List}{\type{X}} \\
&\texttt{add} : \generics{\type{A} \triangleleft \type{Object}}\ \exptype{List}{\type{A}},\type{A} \to \exptype{List}{\type{A}} \\
&}
\end{align*}
\end{minipage}

50
typeinference.tex
View File

@ -342,24 +342,25 @@ decline the call to \texttt{shuffle(l)}.
% There is no solution for the subtype constraint:
% $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$
\item \label{challenge3} \textbf{Free variables cannot leave their scope}:
Let's assume we have a variable \texttt{ls} with type $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$
%When calling the \texttt{id} function with an element of this list we have to apply capture conversion.
and the following program:
\item \label{challenge3}
% \textbf{Free variables cannot leave their scope}:
% Let's assume we have a variable \texttt{ls} with type $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$
% %When calling the \texttt{id} function with an element of this list we have to apply capture conversion.
% and the following program:
\noindent
\begin{minipage}{0.62\textwidth}
\begin{lstlisting}
let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = ls.get(0) in id(x) : (*@$\ntv{z}$@*)
\end{lstlisting}\end{minipage}
\hfill
\begin{minipage}{0.36\textwidth}
\begin{lstlisting}[style=constraints]
(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$@*),
(*@$\exptype{List}{\wtv{x}} \lessdot \ntv{z},$@*)
\end{lstlisting}
\end{minipage}
% the variable z must not contain free variables (TODO)
% \noindent
% \begin{minipage}{0.62\textwidth}
% \begin{lstlisting}
% let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = ls.get(0) in id(x) : (*@$\ntv{z}$@*)
% \end{lstlisting}\end{minipage}
% \hfill
% \begin{minipage}{0.36\textwidth}
% \begin{lstlisting}[style=constraints]
% (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$@*),
% (*@$\exptype{List}{\wtv{x}} \lessdot \ntv{z},$@*)
% \end{lstlisting}
% \end{minipage}
% % the variable z must not contain free variables (TODO)
Take the Java program in listing \ref{lst:mapExample} for example.
It uses map to apply a polymorphic method \texttt{id} to every element of a list
@ -392,7 +393,8 @@ $\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}},
\exptype{List}{\wtv{x}} \lessdot \tv{z}$
stem from the body of the lambda expression
\texttt{id(x)}.
\textit{For clarification:} This method call would be represented as the following expression in \letfj{}:
\textit{For clarification:} This method call would be represented as the following expression in \TamedFJ{}:
\texttt{let x1 :$\wctype{\rwildcard{A}}{List}{\rwildcard{A}}$ = x in id(x) :$\tv{z}$}
The T-Let rule prevents us from using free variables created by the method call to \expr{id}
@ -403,12 +405,12 @@ the constraints.
If we naively substitute $\sigma(\tv{z}) = \exptype{List}{\rwildcard{A}}$
the return type of the \texttt{map} function would be the type
$\exptype{List}{\exptype{List}{\rwildcard{A}}}$, which would be unsound.
The type of \expr{l2} is the same as the one of \expr{l}:
$\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$
\textbf{Solution:}
We solve this issue by distinguishing between wildcard placeholders
and normal placeholders and introducing them as needed.
$\ntv{z}$ is a normal placeholder and is not allowed to contain free variables.
% The type of \expr{l2} is the same as the one of \expr{l}:
% $\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$
% \textbf{Solution:}
% We solve this issue by distinguishing between wildcard placeholders
% and normal placeholders and introducing them as needed.
% $\ntv{z}$ is a normal placeholder and is not allowed to contain free variables.
\end{enumerate}

176
unify.tex
View File

@ -732,28 +732,28 @@ After a substitution all $\tv{r}$ are replaced with this new existential type.
In this example a correct solution is $\sigma(\tv{u}) = \type{Object}$ and $\sigma(\tv{l}) = \bot$.
Remember that the substitution for the type placeholder $\tv{r}$ is $\wctype{\wildcard{X}{\ntv{u}}{\ntv{l}}}{List}{\rwildcard{X}}$
leading to \texttt{List<?>} as a return type for the \texttt{someList} method after applying $\sigma$.
leading to \texttt{List<?>} as a return type for the \texttt{someList} method after applying $\sigma$:
\begin{lstlisting}
\begin{lstlisting}[style=tamedfj]
List<? extends Object> someList(){
return new List("String") :? new List(42);
}
\end{lstlisting}
\subsection{Wildcard Elimination Example}
\begin{lstlisting}
<X> List<X> concat(List<X> l, List<X> l2){ ... }
someList(){
return new List("String") :? new List(42);
}
% \subsection{Wildcard Elimination Example}
% \begin{lstlisting}
% <X> List<X> concat(List<X> l, List<X> l2){ ... }
% someList(){
% return new List("String") :? new List(42);
% }
concat(someList(), someList());
\end{lstlisting}
% concat(someList(), someList());
% \end{lstlisting}
Let's add an additional method call to the previous example.
The \texttt{concat} method takes two lists of the same generic type.
\texttt{concat} cannot be invoked with two existential lists.
%TODO: Explain capture conversion
% Let's add an additional method call to the previous example.
% The \texttt{concat} method takes two lists of the same generic type.
% \texttt{concat} cannot be invoked with two existential lists.
% %TODO: Explain capture conversion
%\subsection{Description}
@ -1282,46 +1282,46 @@ $
\end{figure}
\subsection{Examples}
% \subsection{Examples}
\textit{Example} of the type reduction rules in figure \ref{fig:reductionRules} with the input
$\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$
The first step is the \rulename{Capture} rule.
%The right side of the constraint does not contain any free variables.
$\begin{array}{c}
\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}\\
\hline %Capture
\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdotCC \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
\end{array}$
% \textit{Example} of the type reduction rules in figure \ref{fig:reductionRules} with the input
% $\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$
% The first step is the \rulename{Capture} rule.
% %The right side of the constraint does not contain any free variables.
% $\begin{array}{c}
% \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}\\
% \hline %Capture
% \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdotCC \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
% \end{array}$
\begin{NiceTabular}{l}
$\ \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$ \\
$\nextdeduction{
\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdotCC \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
} $\\
$\nextdeduction{
\rwildcard{X} \vdash \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
} $\\
$\nextdeduction{
\rwildcard{X} \vdash \wctype{\rwildcard{Y}}{List}{\rwildcard{Y}} \doteq \wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X} \doteq \wtv{a}
} $\\
$\nextdeduction{
\wildcard{X}{Object}{\type{String}} \vdash
\type{String} \lessdot \mathcolorbox{addition}{\type{String}}, \tv{a} \doteq \rwildcard{X}
} $\\
$\nextdeduction{
\wildcard{X}{Object}{\type{String}} \vdash
\cancel{\type{String} \lessdot \rwildcard{X}}, \tv{a} \doteq \rwildcard{X}
} $\\
\CodeAfter
\begin{tikzpicture}
\node [right] at (2-|last) { \colorbox{white}{\rulename{Prepare}} } ;
\node [right] at (3-|last) { \colorbox{white}{\rulename{Capture}} } ;
\node [right] at (4-|last) { \colorbox{white}{\rulename{Reduce}} } ;
\node [right] at (5-|last) { \colorbox{white}{\rulename{Equals}} } ;
\node [right] at (6-|last) { \colorbox{white}{\rulename{Erase}} } ;
\end{tikzpicture}
\end{NiceTabular}
% \begin{NiceTabular}{l}
% $\ \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$ \\
% $\nextdeduction{
% \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdotCC \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
% } $\\
% $\nextdeduction{
% \rwildcard{X} \vdash \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
% } $\\
% $\nextdeduction{
% \rwildcard{X} \vdash \wctype{\rwildcard{Y}}{List}{\rwildcard{Y}} \doteq \wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X} \doteq \wtv{a}
% } $\\
% $\nextdeduction{
% \wildcard{X}{Object}{\type{String}} \vdash
% \type{String} \lessdot \mathcolorbox{addition}{\type{String}}, \tv{a} \doteq \rwildcard{X}
% } $\\
% $\nextdeduction{
% \wildcard{X}{Object}{\type{String}} \vdash
% \cancel{\type{String} \lessdot \rwildcard{X}}, \tv{a} \doteq \rwildcard{X}
% } $\\
% \CodeAfter
% \begin{tikzpicture}
% \node [right] at (2-|last) { \colorbox{white}{\rulename{Prepare}} } ;
% \node [right] at (3-|last) { \colorbox{white}{\rulename{Capture}} } ;
% \node [right] at (4-|last) { \colorbox{white}{\rulename{Reduce}} } ;
% \node [right] at (5-|last) { \colorbox{white}{\rulename{Equals}} } ;
% \node [right] at (6-|last) { \colorbox{white}{\rulename{Erase}} } ;
% \end{tikzpicture}
% \end{NiceTabular}
% \subsection{Capture Conversion during Unification}
% % The \unify{} algorithm applies a capture conversion when needed.
@ -1374,48 +1374,48 @@ $\begin{array}{c}
% \end{itemize}
\subsection{Completeness}\label{sec:completeness}
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}.
%thats not true. it can spawn X^T_T2.List<X> where T and T2 are types and we need to choose one inbetween them
Otherwise the algorithm could generate more solutions, but they have to be filterd out afterwards, because they cannot be translated into Java.
% \subsection{Completeness}\label{sec:completeness}
% 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}.
% %thats not true. it can spawn X^T_T2.List<X> where T and T2 are types and we need to choose one inbetween them
% Otherwise the algorithm could generate more solutions, but they have to be filterd out afterwards, because they cannot be translated into Java.
\letfj{} is not able to represent all Java programs. %TODO: this makes ist impossible for our algorithm to be complete on Java
% \letfj{} is not able to represent all Java programs. %TODO: this makes ist impossible for our algorithm to be complete on Java
%Loss of completeness:
% a <. b, b <c List<x>
% %Loss of completeness:
% % a <. b, b <c List<x>
% Example
\begin{lstlisting}
m(l){
return let x = l in x.add(1);
}
\end{lstlisting}
Here generality is lost.
Constraints: $\ntv{l} \lessdot \ntv{x}, \ntv{x} \lessdotCC \exptype{List}{\wtv{x}}$
% % Example
% \begin{lstlisting}
% m(l){
% return let x = l in x.add(1);
% }
% \end{lstlisting}
% Here generality is lost.
% Constraints: $\ntv{l} \lessdot \ntv{x}, \ntv{x} \lessdotCC \exptype{List}{\wtv{x}}$
Correct solution would be:
\begin{lstlisting}
m(List<? super Int> l){
return let x = l in x.add(1);
}
\end{lstlisting}
% Correct solution would be:
% \begin{lstlisting}
% m(List<? super Int> l){
% return let x = l in x.add(1);
% }
% \end{lstlisting}
Our solution:
\begin{lstlisting}
<X extends List<Integer> m(X l){
return let x = l in x.add(1);
}
m(List<? super Integer>)
\end{lstlisting}
$\tv{a} \lessdotCC \type{T}$ constraints allow for existential types on the left side,
because there will be a capture conversion.
We do not cover this and only apply capture conversion when the left side is known.
So $\tv{a}$ will not be assigned a existential type, which explains our less general solution.
% Our solution:
% \begin{lstlisting}
% <X extends List<Integer> m(X l){
% return let x = l in x.add(1);
% }
% m(List<? super Integer>)
% \end{lstlisting}
% $\tv{a} \lessdotCC \type{T}$ constraints allow for existential types on the left side,
% because there will be a capture conversion.
% We do not cover this and only apply capture conversion when the left side is known.
% So $\tv{a}$ will not be assigned a existential type, which explains our less general solution.
If all of the program is given this may be not much of an issue.
The $\tv{a} \lessdotCC \type{T}$ constraint is kept until the end and if the method
is called and $\tv{a}$ gets a type, then this type can be an existential type aswell.
% If all of the program is given this may be not much of an issue.
% The $\tv{a} \lessdotCC \type{T}$ constraint is kept until the end and if the method
% is called and $\tv{a}$ gets a type, then this type can be an existential type aswell.
% Problem: There are infinite subtypes to a type Pair<x,y> when capture conversion is allowed