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

Restructure. Add to Introduction and cleanup

Browse Source
This commit is contained in:
JanUlrich 2024-05-24 22:25:31 +02:00
parent 9f088eb29d
commit 4c67504ba1
2 changed files with 124 additions and 109 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
constraints.tex
View File

@ -125,7 +125,7 @@ m(l, v){
\end{minipage}% \end{minipage}%
\hfill \hfill
\begin{minipage}{0.5\textwidth} \begin{minipage}{0.5\textwidth}
\begin{lstlisting}[style=tfgj,caption=converted to A-Normal form,label=lst:anfoutput] \begin{lstlisting}[style=tfgj,caption=A-Normal form,label=lst:anfoutput]
m(l, v) = m(l, v) =
let x1 = l in let x1 = l in
let x2 = v in x1.add(x2) let x2 = v in x1.add(x2)
@ -161,15 +161,15 @@ $
%\hline %\hline
\end{array} \end{array}
$ $
\caption{A-Normal form}\label{fig:anf-syntax} \caption{Syntax of a \TamedFJ{} program in A-Normal Form}\label{fig:anf-syntax}
\end{figure} \end{figure}
\subsection{Constraint Generation Algorithm} \subsection{Constraint Generation Algorithm}
Generally subtype constraints for an expression mirror the subtype relations in the premise of the respective type rule introduced in section \ref{sec:tifj}. % Generally subtype constraints for an expression mirror the subtype relations in the premise of the respective type rule introduced in section \ref{sec:tifj}.
Unknown types at the time of the constraint generation step are replaced with type placeholders. % Unknown types at the time of the constraint generation step are replaced with type placeholders.
The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call. % The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion. % Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
The parameter types given to a generic method also affect their return type. The parameter types given to a generic method also affect their return type.
During constraint generation the algorithm does not know the parameter types yet. During constraint generation the algorithm does not know the parameter types yet.

221
introduction.tex
View File

@ -10,7 +10,36 @@
% Capture Conversion % Capture Conversion
% Explain difference between local and global type inference % Explain difference between local and global type inference
% \begin{recap}\textbf{TI for FGJ without Wildcards:}
% \TFGJ{} generates subtype constraints $(\type{T} \lessdot \type{T})$ consisting of named types and type placeholders.
% For example the method invocation \texttt{concat(l, new Object())} generates the constraints
% $\tv{l} \lessdot \exptype{List}{\tv{a}}, \type{Object} \lessdot \tv{a}$.
% Subtyping without the use of wildcards is invariant \cite{FJ}:
% Therefore the only possible solution for the type placeholder $\tv{a}$ is $\tv{a} \doteq \type{Object}$. % in Java and Featherweight Java.
% The correct type for the variable \texttt{l} is $\exptype{List}{\type{Object}}$ (or a direct subtype).
% %- usually the type of e must be subtypes of the method parameters
% %- in case of a polymorphic method: type placeholders resemble type parameters
% The type inference algorithm for Featherweight Generic Java \cite{TIforFGJ} (called \TFGJ{}) is complete and sound:
% It is able to find a type solution for a Featherweight Generic Java program, which has no type annotations at all,
% if there is any.
% It's only restriction is that no polymorphic recursion is allowed.
% \end{recap}
\section{Type Inference for Java} \section{Type Inference for Java}
- Type inference helps rapid development
- used in Java already (var keyword)
- keeps source code clean
Java comes with a local type inference algorithm
used for lambda expressions, method calls, and the \texttt{var} keyword.
A type inference algorithm that is able to recreate any type annotation
even when no type information is given at all is called a global type inference algorithm.
The global type inference algorithm presented here is able to deal with all Java types including wildcard types.
It can also be used for regular Java programs.
%The goal is to find a correct typing for a given Java program. %The goal is to find a correct typing for a given Java program.
Type inference for Java has many use cases and could be used to help programmers by inserting correct types for them, Type inference for Java has many use cases and could be used to help programmers by inserting correct types for them,
finding better type solutions for already typed Java programs (for example more generical ones), finding better type solutions for already typed Java programs (for example more generical ones),
@ -43,9 +72,17 @@ involving a wildcard type.
\item[Type Unification for Java with Wildcards] \item[Type Unification for Java with Wildcards]
An existing unification algorithm for Java with wildcards \cite{plue09_1} states the same capabilities, An existing unification algorithm for Java with wildcards \cite{plue09_1} states the same capabilities,
but exposes some errors when it comes to method invocations. but exposes some errors when it comes to method invocations.
Especially the problems shown in chapter \ref{challenges} are handled incorrectly. Especially the challenges shown in chapter \ref{challenges} are handled incorrectly.
The algorithm presented in this paper is able to solve all those challenges correctly The main reasons are that Plümickes algorithm only supports types which are expressible in Java syntax
and it's correctness is proven using a Featherweight Java calculus \cite{WildFJ}. and its soundness is proven towards a self-defined subtype ordering, but never against a complete type system.
It appears that the subtype relation changes depending on whether a type is used as an argument to a method invocation.
We resolve this by denoting Java wildcards as existential types
and introducing a second kind of subtype constraint. %, the current state of the art
%and is able to deal with types that are not directly denotable in Java.
Additionally the soundness of our algorithm is proven using a Featherweight Java calculus \cite{WildFJ}.
%The algorithm presented in this paper is able to solve all those challenges correctly
%and it's correctness is proven using a Featherweight Java calculus \cite{WildFJ}.
%But they are all correctly solved by our new type inference algorithm presented in this paper. %But they are all correctly solved by our new type inference algorithm presented in this paper.
\item[Java Type Inference] \item[Java Type Inference]
@ -329,14 +366,16 @@ In this example we know that the type of the variable \texttt{l} is an existenti
before being passed to a method call. before being passed to a method call.
This is done by converting the program to A-Normal form \ref{lst:addExampleLet}, This is done by converting the program to A-Normal form \ref{lst:addExampleLet},
which introduces a let statement defining a new variable \texttt{v}. which introduces a let statement defining a new variable \texttt{v}.
Afterwards constraints are generated \ref{lst:addExampleCons}. Afterwards unknown types are replaced by type placeholders ($\tv{v}$ for the type of \texttt{v}) and constraints are generated (see \ref{lst:addExampleCons}).
During the constraint generation step the type of the variable \texttt{v} is unknown These constraints mirror the type rules of our \TamedFJ{} calculus.
and given the type placeholder $\tv{v}$. % During the constraint generation step the type of the variable \texttt{v} is unknown
% and given the type placeholder $\tv{v}$.
The methodcall to \texttt{add} spawns the constraint $\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$. The methodcall to \texttt{add} spawns the constraint $\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$.
Here we introduce a capture constraint ($\lessdotCC$) %a new type of subtype constraint Here we introduce a capture constraint ($\lessdotCC$) %a new type of subtype constraint
expressing that the left side of the constraint is subject to a capture conversion. expressing that the left side of the constraint is subject to a capture conversion.
At the start of our global type inference algorithm no types are assigned yet. Now our unification algorithm \unify{} (defined in chapter \ref{sec:unify}) is used to solve these constraints.
During the course of \unify{} - our unification algorithm used to solve the generated constraint set (see chapter \ref{sec:unify})- more and more types emerge. In the starting set of constraints no type is assigned to $\tv{v}$ yet.
During the course of \unify{} more and more types emerge.
As soon as a concrete type for $\tv{v}$ is given \unify{} can conduct a capture conversion if needed. As soon as a concrete type for $\tv{v}$ is given \unify{} can conduct a capture conversion if needed.
%The constraints where this is possible are marked as capture constraints. %The constraints where this is possible are marked as capture constraints.
In this example $\tv{v}$ will be set to $\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$ leaving us with the following constraints: In this example $\tv{v}$ will be set to $\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$ leaving us with the following constraints:
@ -381,81 +420,6 @@ a type parameter to method call \texttt{<X>add(v, "String")}.
% There are no informal parts in our \unify{} algorithm. % There are no informal parts in our \unify{} algorithm.
% It solely consist out of transformation rules which are bound to simple checks. % It solely consist out of transformation rules which are bound to simple checks.
One problem is the divergence between denotable and expressable types in Java \cite{semanticWildcardModel}.
A wildcard in the Java syntax has no name and is bound to its enclosing type:
$\exptype{List}{\exptype{List}{\type{?}}}$ equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
During type checking \emph{intermediate types}
%like $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$
%or $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$
can emerge, which have no equivalent in the Java syntax.
%Our type inference algorithm uses existential types internally but spawns type solutions compatible with Java.
Example: % This program is not typable with the Type Inference algorithm from Plümicke
\begin{lstlisting}[style=java,label=shuffleExample,caption=Intermediate Types Example]
class List<X> extends Object {...}
class List2D<X> extends List<List<X>> {...}
<X> void shuffle(List<List<X>> list) {...}
List<List<?>> l = ...;
List2D<?> l2d = ...;
shuffle(l); // Error
shuffle(l2d); // Valid
\end{lstlisting}
Java is using local type inference to allow method invocations which are not describable with regular Java types.
The \texttt{shuffle} method in this case is invoked with the type $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$
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=TamedFJ]
let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in <X>shuffle(l2d')
\end{lstlisting}
\begin{recap}\textbf{TI for FGJ without Wildcards:}
\TFGJ{} generates subtype constraints $(\type{T} \lessdot \type{T})$ consisting of named types and type placeholders.
For example the method invocation \texttt{concat(l, new Object())} generates the constraints
$\tv{l} \lessdot \exptype{List}{\tv{a}}, \type{Object} \lessdot \tv{a}$.
Subtyping without the use of wildcards is invariant \cite{FJ}:
Therefore the only possible solution for the type placeholder $\tv{a}$ is $\tv{a} \doteq \type{Object}$. % in Java and Featherweight Java.
The correct type for the variable \texttt{l} is $\exptype{List}{\type{Object}}$ (or a direct subtype).
%- usually the type of e must be subtypes of the method parameters
%- in case of a polymorphic method: type placeholders resemble type parameters
The type inference algorithm for Featherweight Generic Java \cite{TIforFGJ} (called \TFGJ{}) is complete and sound:
It is able to find a type solution for a Featherweight Generic Java program, which has no type annotations at all,
if there is any.
It's only restriction is that no polymorphic recursion is allowed.
\end{recap}
%
For the example shown in listing \ref{shuffleExample} the method call \texttt{shuffle(l2d)} creates the constraints:
\begin{constraintset}
\begin{center}
$
\begin{array}{l}
\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
\\
\hline
\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
\\
\hline
\textit{Capture Conversion:}\
\exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\wtv{x}}}
\\
\hline
\textit{Solution:} \wtv{x} \doteq \rwildcard{X} \implies \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\rwildcard{X}}}
\end{array}
$
\end{center}
\end{constraintset}
The method call \texttt{shuffle(l)} is invalid however,
because \texttt{l} has the type
$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
There is no solution for the subtype constraint:
$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$
\subsection{Challenges}\label{challenges} \subsection{Challenges}\label{challenges}
%TODO: Wildcard subtyping is infinite see \cite{TamingWildcards} %TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
@ -486,28 +450,79 @@ exists to satisfy
$\exptype{List}{\type{A}} <: \exptype{List}{\type{X}}, $\exptype{List}{\type{A}} <: \exptype{List}{\type{X}},
\exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$. \exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$.
% \item \item
% \unify{} morphs a constraint set into a correct type solution \unify{} morphs a constraint set into a correct type solution
% gradually assigning types to type placeholders during that process. gradually assigning types to type placeholders during that process.
% Solved constraints are removed and never considered again. Solved constraints are removed and never considered again.
% In the following example \unify{} solves the constraint generated by the expression In the following example \unify{} solves the constraint generated by the expression
% \texttt{l.add(l.head())} first, which results in $\ntv{l} \lessdot \exptype{List}{\wtv{a}}$. \texttt{l.add(l.head())} first, which results in $\ntv{l} \lessdot \exptype{List}{\wtv{a}}$.
% \begin{verbatim} \begin{verbatim}
% anyList() = new List<String>() :? new List<Integer>() anyList() = new List<String>() :? new List<Integer>()
% add(anyList(), anyList().head()); add(anyList(), anyList().head());
% \end{verbatim} \end{verbatim}
% The type for \texttt{l} can be any kind of list, but it has to be a invariant one. The type for \texttt{l} can be any kind of list, but it has to be a invariant one.
% Assigning a \texttt{List<?>} for \texttt{l} is unsound, because the type list hiding behind Assigning a \texttt{List<?>} for \texttt{l} is unsound, because the type list hiding behind
% \texttt{List<?>} could be a different one for the \texttt{add} call than the \texttt{head} method call. \texttt{List<?>} could be a different one for the \texttt{add} call than the \texttt{head} method call.
% An additional constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ An additional constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
% is solved by removing the wildcard $\rwildcard{X}$ if possible. is solved by removing the wildcard $\rwildcard{X}$ if possible.
\item \textbf{Capture Conversion during \unify{}:} this problem is solved by ANF transformation
The example in \ref{lst:addExample} needs to be solvable.
Here a capture conversion during the unification step of our algorithm has to be conducted. \item \textbf{Wildcards as Existential Types:}
Otherwise the \texttt{add} method is not callable with the existential type One problem is the divergence between denotable and expressable types in Java \cite{semanticWildcardModel}.
$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$. A wildcard in the Java syntax has no name and is bound to its enclosing type:
$\exptype{List}{\exptype{List}{\type{?}}}$ equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
During type checking \emph{intermediate types}
can emerge, which have no equivalent in the Java syntax.
\begin{lstlisting}[style=java,label=shuffleExample,caption=Intermediate Types Example]
class List<X> extends Object {...}
class List2D<X> extends List<List<X>> {...}
<X> void shuffle(List<List<X>> list) {...}
List<List<?>> l = ...;
List2D<?> l2d = ...;
shuffle(l); // Error
shuffle(l2d); // Valid
\end{lstlisting}
Java is using local type inference to allow method invocations which are not describable with regular Java types.
The \texttt{shuffle} method in this case is invoked with the type $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$
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=TamedFJ]
let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in <X>shuffle(l2d')
\end{lstlisting}
For the example shown in listing \ref{shuffleExample} the method call \texttt{shuffle(l2d)} creates the constraints:
\begin{constraintset}
\begin{center}
$
\begin{array}{l}
\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
\\
\hline
\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
\\
\hline
\textit{Capture Conversion:}\
\exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\wtv{x}}}
\\
\hline
\textit{Solution:} \wtv{x} \doteq \rwildcard{X} \implies \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\rwildcard{X}}}
\end{array}
$
\end{center}
\end{constraintset}
The method call \texttt{shuffle(l)} is invalid however,
because \texttt{l} has the type
$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
There is no solution for the subtype constraint:
$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$
\item \textbf{Free Variables cannot leaver their scope}: \item \textbf{Free Variables cannot leaver their scope}: