Ecoop2024_TIforWildFJ/conclusion.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