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

Restructure challenges

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-05-14 13:32:06 +02:00
parent 8c6085f3b1
commit b1d3c4d525
2 changed files with 54 additions and 99 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
constraints.tex
View File

@ -43,6 +43,9 @@ We preemptively enclose every expression in a let statement before using it as a
% This behaviour emulates Java's implicit capture conversion.
%TODO: how are the challenges solved:
The \unify{} algorithm only sees the constraints with no information about the program they originated from.
\subsection{ANF transformation}\label{sec:anfTransformation}
\newcommand{\anf}[1]{\ensuremath{\tau}(#1)}

150
introduction.tex
View File

@ -181,8 +181,44 @@ if not for the Java type system which rejects the assignment \texttt{lo = ls}.
Listing \ref{lst:wildcardIntro} shows the use of wildcards rendering the assignment \texttt{lo = ls} correct.
The program still does not compile, because now the addition of an Integer to \texttt{lo} is rightfully deemed incorrect by Java.
% Goal: Motivate the TamedFJ language. Why do we need it (Capture Conversion)
This behaviour is emulated by our language \TamedFJ{},
Wildcard types are virtual types.
There is no instantiation of a \texttt{List<?>}.
It is a placeholder type which can hold any kind of list like
\texttt{List<String>} or \texttt{List<Object>}.
This type can also change at any given time, for example when multiple threads
are using the same field of type \texttt{List<?>}.
A wildcard \texttt{?} must be considered a different type everytime it is accessed.
Therefore calling the method \texttt{concat} with two wildcard lists in the example in listing \ref{lst:concatError} is incorrect.
% The \texttt{concat} method does not create a new list,
% but adds all elements from the second argument to the list given as the first argument.
% This is allowed in Java, because both lists are of the polymorphic type \texttt{List<X>}.
% As shown in listing \ref{lst:concatError} this leads to a inconsistent \texttt{List<String>}
% if Java would treat \texttt{?} as a regular type and instantiate the type variable \texttt{X}
% of the \texttt{concat} function with \texttt{?}.
\begin{figure}
\begin{lstlisting}[caption=Concat Example,label=lst:concatError]{java}
<X> List<X> concat(List<X> l1, List<X> l2){
return l1.addAll(l2);
}
List<String> ls = new List<String>();
List<?> l1 = ls;
List<?> l2 = new List<Integer>(1);
concat(l1, l2);
\end{lstlisting}
\begin{lstlisting}[style=TamedFJ,caption=\TamedFJ{} representation, label=lst:concatTamedFJ]
let l1' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l1 in
let l2' : (*@$\wctype{\rwildcard{Y}}{List}{\exptype{List}{\rwildcard{Y}}}$@*) = l2 in
concat(l1', l2') // Error!
\end{lstlisting}
\end{figure}
To enable the use of wildcards in argument types of a method invocation
Java uses a process called \textit{Capture Conversion}.
This behaviour is emulated by our language \TamedFJ{};
a Featherweight Java \cite{FJ} derivative with added wildcard support
and a global type inference feature (syntax definition in section \ref{sec:tifj}).
%\TamedFJ{} is basically the language described by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection} with optional type annotations.
@ -246,7 +282,7 @@ add(l, "String");
\end{lstlisting}
\end{minipage}\hfill
\begin{minipage}{0.49\textwidth}
\begin{lstlisting}[style=letfj, caption=\letfj{} representation, label=lst:addExampleLet]
\begin{lstlisting}[style=letfj, caption=\TamedFJ{} representation, label=lst:addExampleLet]
<A> List<A> add(List<A> l, A v)
let l2 : (*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = l
@ -255,7 +291,7 @@ let l2 : (*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcar
\end{minipage}
\end{figure}
The Example in listing \ref{lst:addExample} is a valid Java program. Here Java uses local type inference \cite{JavaLocalTI}
In listing \ref{lst:addExample} Java uses local type inference \cite{JavaLocalTI}
to determine the type parameters to the \texttt{add} method call.
A \TamedFJ{} representation including all type annotations and an explicit capture conversion via let statement is shown in listing \ref{lst:addExampleLet}.
%In \letfj{} there is no local type inference and all type parameters for a method call are mandatory (see listing \ref{lst:addExampleLet}).
@ -294,7 +330,7 @@ The \texttt{shuffle} method in this case is invoked with the type $\wctype{\rwil
which is a subtype of $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
After capture conversion \texttt{l2d'} has the type $\exptype{List}{\exptype{List}{\rwildcard{X}}}$
and \texttt{shuffle} can be invoked with the type parameter $\rwildcard{X}$:
\begin{lstlisting}[style=letfj]
\begin{lstlisting}[style=TamedFJ]
let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in <X>shuffle(l2d')
\end{lstlisting}
@ -457,106 +493,24 @@ A problem arises when replacing type variables with wildcards.
Lets have a look at a few challenges:
\begin{itemize}
\item
%Passing wildcard types to a polymorphic method call comes with additional challenges.
% TODO: Here the concat example!
%- Wildcards are not reflexive
%- Wildcards are opaque types. Behind a Java Wildcard is a real type.
Wildcard types are virtual types.
There is no instantiation of a \texttt{List<?>}.
It is a placeholder type which can hold any kind of list like
\texttt{List<String>} or \texttt{List<Object>}.
This type can also change at any given time, for example when multiple threads
are using the same field of type \texttt{List<?>}.
A wildcard \texttt{?} must be considered a different type everytime it is accessed.
Therefore calling the method \texttt{concat} with two wildcard lists in the example in listing \ref{lst:concatError} is incorrect.
The \texttt{concat} method does not create a new list,
but adds all elements from the second argument to the list given as the first argument.
This is allowed in Java, because both lists are of the polymorphic type \texttt{List<X>}.
As shown in listing \ref{lst:concatError} this leads to a inconsistent \texttt{List<String>}
if Java would treat \texttt{?} as a regular type and instantiate the type variable \texttt{X}
of the \texttt{concat} function with \texttt{?}.
To enable the use of wildcards in argument types of a method invocation
Java uses a process called \textit{Capture Conversion}.
\begin{lstlisting}[caption=Concat Example,label=lst:concatError]{java}
<X> List<X> concat(List<X> l1, List<X> l2){
return l1.addAll(l2);
}
List<String> ls = new List<String>();
List<?> l1 = ls;
List<?> l2 = new List<Integer>(1);
concat(l1, l2);
\end{lstlisting}
%Existential types enable us to formalize Java's method call behavior and the so called Capture Conversion.
\begin{displaymath}
%TODO:
\begin{array}{l}
\begin{array}{@{}c}
\textit{mtype}(\texttt{concat}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \\
\texttt{l1} : \wctype{\rwildcard{A}}{List}{\rwildcard{A}}, \texttt{l2} : \wctype{\rwildcard{B}}{List}{\rwildcard{B}} \\
\exptype{List}{\rwildcard{A}} \nless: [{\color{red}?}/\type{X}]\exptype{List}{\type{X}} \quad \quad
\exptype{List}{\rwildcard{B}} \nless: [{\color{red}?}/\type{X}]\exptype{List}{\type{X}}
\\
\hline
\vspace*{-0.3cm}\\
\texttt{concat}(\expr{l1}, \expr{l2}) : {\color{red}\textbf{Errror}}
\end{array}
\end{array}
\end{displaymath}
%A method call in Java makes use of the fact that a real type is behind a wildcard type
\item \begin{example} \label{intro-example1}
The first one is a valid Java program.
The type \texttt{List<? super String>} is \textit{capture converted} to a fresh type variable $\rwildcard{X}$
which is used as the generic method parameter \texttt{A}.
Java uses capture conversion to replace the generic \texttt{A} by a capture converted version of the
\texttt{? super String} wildcard.
Knowing that the type \texttt{String} is a subtype of any type the wildcard \texttt{? super String} can inherit
One challenge is to design the algorithm in a way that it finds a correct solution for the program shown in listing \ref{lst:addExample}
and rejects the program in listing \ref{lst:concatError}.
The first one is a valid Java program,
because the type \texttt{List<? super String>} is \textit{capture converted} to a fresh type variable $\rwildcard{X}$
which is used as the generic method parameter for the call to \texttt{add} as shown in listing \ref{lst:addExampleLet}.
Knowing that the type \texttt{String} is a subtype of the free variable $\rwildcard{X}$
it is safe to pass \texttt{"String"} for the first parameter of the function.
\begin{verbatim}
<A> List<A> add(List<A> l, A v) {}
List<? super String> list = ...;
add(list, "String");
\end{verbatim}
\end{example}
\item \begin{example}\label{intro-example2}
This example displays an incorrect Java program.
The second program shown in listing \ref{lst:concatError} is incorrect.
The method call to \texttt{concat} with two wildcard lists is unsound.
Each list could be of a different kind and therefore the \texttt{concat} cannot succeed.
\begin{verbatim}
<A> List<A> concat(List<A> l1, List<A> l2) { ... }
List<?> getList() { ... }
concat(getList(), getList());
\end{verbatim}
The \letfj{} representation in listing \ref{letfjConcatFail} clarifies this.
Inside the let statement the variables hold the types
$\set{ \texttt{x1} : \exptype{List}{\rwildcard{X}}, \texttt{x2} : \exptype{List}{\rwildcard{Y}}}$.
The problem gets apparent when we try to write the \texttt{concat} method call in our \TamedFJ{} calculus (listing \ref{lst:concatTamedFJ}):
\texttt{l1'} and \texttt{l2'} are two different lists inside the body of the let statements, namely
$\exptype{List}{\rwildcard{X}}$ and $\exptype{List}{\rwildcard{Y}}$.
For the method call \texttt{concat(x1, x2)} no replacement for the generic \texttt{A}
exists to satisfy
$\exptype{List}{\type{A}} <: \exptype{List}{\type{X}},
\exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$.
\begin{lstlisting}[style=letfj,caption=Incorrect method call,label=letfjConcatFail]
let x1 : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = getList() in
let x2 : (*@$\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}$@*) = getList() in
concat(x1, x2)
\end{lstlisting}
% $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}, \\
% \wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
\end{example}
% \item
% \unify{} morphs a constraint set into a correct type solution
@ -649,5 +603,3 @@ $\ntv{z}$ is a normal placeholder and is not allowed to contain free variables.
\end{itemize}
%TODO: Move this part. or move the third challenge some underneath.
The \unify{} algorithm only sees the constraints with no information about the program they originated from.
The main challenge was to find an algorithm which computes $\sigma(\wtv{a}) = \rwildcard{X}$ for example \ref{intro-example1} but not for example \ref{intro-example2}.