163 lines
6.2 KiB
TeX
163 lines
6.2 KiB
TeX
%TODO: how are the challenges solved: Describe this in the last chapter with examples!
|
|
\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:
|
|
|
|
\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){...}
|
|
|
|
bool test(List<?> l){
|
|
return compare(make(l));
|
|
}
|
|
}
|
|
\end{lstlisting}
|
|
\end{minipage}%
|
|
\hfill
|
|
\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.
|
|
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}
|
|
|
|
|
|
$\ntv{x}$ will get the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and
|
|
from the constraint
|
|
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
|
|
\unify{} deducts $\wtv{a} \doteq \rwildcard{X}$ leading to
|
|
$\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{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}
|
|
|
|
% 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>
|
|
|
|
% % 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){}
|
|
|
|
% Pair<?,?> p ...
|
|
% List<?> l ...
|
|
|
|
% make(t) { return t; }
|
|
% triple(make(sameP(p)));
|
|
% triple(make(sameL(l)));
|
|
% \end{lstlisting}
|
|
|
|
% \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}).
|
|
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.
|
|
|
|
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}
|
|
% \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}
|
|
% <A> void m(List<A> a){}
|
|
|
|
% m2(l){
|
|
% l.add("String");
|
|
% }
|
|
% \end{verbatim}
|
|
|
|
%COnstraints:
|
|
%l <. List<a>
|
|
%String <. a
|
|
|
|
|