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

Cleanup and remove capture conversion chapter

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-03-05 18:31:50 +01:00
parent e15d61cdae
commit cbba453a73
3 changed files with 279 additions and 309 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

287
TIforWildFJ.tex
View File

@ -101,126 +101,7 @@ TODO: Abstract
\input{introduction} \input{introduction}
%We could do a translation from Java to \wildFJ explaining implicit capture conversion %\input{letfjTransformation}
\section{Soundness of Typing}
We show soundness with the type rules statet in \cite{WildcardsNeedWitnessProtection}.
A correct \FGJGT{} program can be converted to a correct \wildFJ{} program.
\begin{figure}
$\begin{array}{rcl}
| \texttt{x} |
& = & \texttt{x} \\
| \texttt{let} \ \texttt{x} : \type{T} = \texttt{e},\, \ol{x} : \ol{T} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x}) |
& = & |\texttt{e}|.\texttt{m}(\ol{|e|}) \\
| \texttt{let} \ \texttt{x} : \type{T} = \texttt{e}\ \texttt{in}\ \texttt{x}.\texttt{f} |
& = & |\texttt{e}|.\texttt{f} \\
| \texttt{e} \elvis{} \texttt{e} |
& = & |\texttt{e}| \elvis{} |\texttt{e}| \\
\end{array}$
\caption{Erasure} \label{fig:erasure}
\end{figure}
% A constraint Pair<A,B> <. a, then a has infinite possibilities:
% a =. X.Pair<X,X>
% a =. X,Y.Pair<X,Y>
% a =. X.Pair<Pair<X,X>,X>
% a =. X,Y.Pair<Pair<X,Y>,X>
% a =. X,Y.Pair<Pair<X,Y>,Y>
% There is no way to try out every single one of them.
Starting with the parameters of the method we gradually add every expression which only contains already captured expressions.
We have a typed expression
$|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} : \type{T} = \texttt{x in}$
$|\texttt{e.f}, \texttt{r}| = |\texttt{e}, x| \texttt{let} r = x.\texttt{f} \ \texttt{in}$
$|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} = \texttt{x in}$
%TODO: write the transform rules:
% |e.f, ret| = |e, r| let ret = r.f in
% |x, ret| = let ret = x in
% |e.m(e_), ret| = |e, r| |e_, a_| let ret = r.m(a_) in
Erasure functions:
$|\texttt{x}| = \texttt{let r} : \wcNtype{\Delta}{N} = \texttt{x in r}$
$\texttt{x} \longmapsto \texttt{let}\ \texttt{xx} : \type{T} = \texttt{x in xx}$
$\texttt{x}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in xf}$
$\begin{array}{l}
\texttt{e} \longmapsto \texttt{let}\ \texttt{xe} : \type{T} = \texttt{e}' \ \texttt{in xe} \\
\hline
\vspace*{-0.4cm}\\
\texttt{e}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in x}.f
\end{array}$
Example:
m(a, b) = a.m(b.f);
let xa = a in let xb = b in let xf = xb.f in let xm = xa.m(xf) in xm
% TODO: Now we have to proof that there is a LetFJ program for every TIFJ program!
% |let xr : T = x1.m(x2) in e| = [x1.m(x2)/xr]|e|
% |let xf : T = x1.f in e| = [x1.f/xf]|e|
% |let xr : T = x in e| = [xr/x]|e|
% |new C(x)| = new C(x)
% | let xr : T' = x in let xf : T = xr.f | = x.f
% let x : T' = e' in x = |e|
% ---------------------------------
% | let xr : T' = x in let xf : T = xr.f | = x.f
% let x : T' = e' in x = |e|
% -----------
% =
We need a language which only has let statemnts and expressions on capture converted variables
The idea is to use wildcard placeholders inside the method. Also in the bounds of wildcards.
This makes it possible to replace wildcards with free variables by setting upper and lower bound to that free variable.
Free variables then can flow freely inside the method body.
We have to show that a type solution implies that there is a possible transformation to a correct typed letFJ program.
If there is a possible method type then there must exist a let configuration.
% By starting with the parameter types and capturing them. Afterwards every capture creates free variables which are used inside
% TODO: Proof!
The normal type placeholders represent denotable types.
%TODO: the type rules stay the same. We generate let statements in a fashion which removes all wildcard types.
% what about wildcards getting returned by untyped methods? they can also be captured
% TODO: try soundness proof on the original type rules!
Removing of extensive wildcards:
$
\wctype{\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{X}, \rwildcard{Y}}
\lessdot \wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}} \\
\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \wtv{x}, \rwildcard{Y} \doteq \wtv{x} \\
\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \rwildcard{Y} \\
\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
\implies \wctype{\wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{Y}, \rwildcard{Y}}, \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
$
%e.f leads to constraints: r <c C<x> with return type equals the field type T.
% T can contain free variables from r. but also it can be used in another constraint and get free variables from inner let statements
% X.C<X> <c C<x> -> then T contains X variables
% let x1 = p1, x2 = p2 in
% let r1 = x1 in let r2 = p2 in let f1 = r2.f in let r3 = x1 in let m2 = r3.m2() let ret = r1.m(f1,m2)
% in ret
What about method invocation with no type yet. m2 :: a -> a
they are also encased in let expression so the return type can be capture converted.
Those methods and the parameter types of the current method are the only things not typed.
All the other types cannot change their type. The captured wildcards can only flow from top to bottom.
The return type of untyped methods has to be well-formed and cannot contain free variables.
Therefore no free variables will flow into those types.
\input{tRules} \input{tRules}
@ -228,172 +109,6 @@ Therefore no free variables will flow into those types.
\input{constraints} \input{constraints}
\section{Capture Conversion}
The input to our type inference algorithm does not contain let statements.
Those are added after computing a type solution.
Let statements act as capture conversion and only have to be applied in method calls involving wildcard types.
\begin{figure}
\begin{minipage}{0.45\textwidth}
\begin{lstlisting}[style=fgj]
<X> List<X> clone(List<X> l);
example(p){
return clone(p);
}
\end{lstlisting}
\end{minipage}%
\hfill
\begin{minipage}{0.5\textwidth}
\begin{lstlisting}[style=tfgj]
(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){
return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in
clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
}
\end{lstlisting}
\end{minipage}
\caption{Type inference adding capture conversion}\label{fig:addingLetExample}
\end{figure}
Figure \ref{fig:addingLetExample} shows a let statement getting added to the typed output.
The method \texttt{clone} cannot be called with the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
After a capture conversion \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$ with $\rwildcard{X}$ being a free variable.
Afterwards we have to find a supertype of $\exptype{List}{\rwildcard{X}}$, which does not contain free variables
($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in this case).
During the constraint generation step most types are not known yet and are represented by a type placeholder.
During a methodcall like the one in the \texttt{example} method in figure \ref{fig:ccExample} the type of the parameter \texttt{p}
is not known yet.
The type \texttt{List<?>} would be one possibility as a parameter type for \texttt{p}.
To make wildcards work for our type inference algorithm \unify{} has to apply capture conversions if necessary.
The type placeholder $\tv{r}$ is the return type of the \texttt{example} method.
One possible type solution is $\tv{p} \doteq \tv{r} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$,
which leads to:
\begin{verbatim}
List<?> example(List<?> p){
return clone(p);
}
\end{verbatim}
But by substituting $\tv{p} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in the constraint
$\tv{p} \lessdot \exptype{List}{\wtv{x}}$ leads to
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{x}}$.
To make this typing possible we have to introduce a capture conversion via a let statement:
$\texttt{return}\ (\texttt{let}\ \texttt{x} : \wctype{\rwildcard{X}}{List}{\rwildcard{X}} = \texttt{p}\ \texttt{in} \
\texttt{clone}\generics{\rwildcard{X}}(x) : \wctype{\rwildcard{X}}{List}{\rwildcard{X}})$
Inside the let statement the variable \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$
$
\begin{array}[c]{l}
\wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \rwildcard{G}}\\
\hline
[\type{G}/\wtv{a}]\wildcardEnv \vdash [\type{G}/\wtv{a}]C \cup \set{\tv{a} \doteq \type{G}}
\end{array}
$
This spawns additional problems.
%TODO
%we need the constraint set to be a list
%not on every constraint CC is allowed. The unify algorithm does not know the context in which a constraint was generated
%free type variables cannot leave the scope of the method call
\begin{figure}
\begin{minipage}{0.45\textwidth}
\begin{verbatim}
<X> List<X> clone(List<X> l){...}
example(p){
return clone(p);
}
\end{verbatim}
\end{minipage}%
\hfill
\begin{minipage}{0.35\textwidth}
\begin{constraintset}
\textbf{Constraints:}\\
$
\tv{p} \lessdot \exptype{List}{\wtv{x}}, \\
\tv{p} \lessdot \tv{r}, \\
\tv{p} \lessdot \type{Object},
\tv{r} \lessdot \type{Object}
$
\end{constraintset}
\end{minipage}
\caption{Type inference example}\label{fig:ccExample}
\end{figure}
In addition with free variables this leads to unwanted behaviour.
Take the constraint
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ for example.
After a capture conversion from $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ to $\exptype{List}{\rwildcard{Y}}$ and a substitution $\wtv{a} \doteq \rwildcard{Y}$
we get
$\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$.
Which is correct if we apply capture conversion to the left side:
$\exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$
If the input constraints did not intend for this constraint to undergo a capture conversion then \unify{} would produce an invalid
type solution due to:
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \nless: \exptype{List}{\rwildcard{X}}$
The reason for this is the \texttt{S-Exists} rule's premise
$\text{dom}(\Delta') \cap \text{fv}(\exptype{List}{\rwildcard{X}}) = \emptyset$.
Additionally free variables are not allowed to leave the scope of a capture conversion
introduced by a let statement.
%TODO we combat both of this with wildcard type placeholders (? flag)
Type placeholders which are not flagged as possible free variables ($\wtv{a}$) can never hold a free variable or a type containing free variables.
Constraint generation places these standard place holders at method return types and parameter types.
\begin{lstlisting}[style=fgj]
<X> List<X> clone(List<X> l);
(*@$\red{\tv{r}}$@*) example((*@$\red{\tv{p}}$@*) p){
return clone(p);
}
\end{lstlisting}
This prevents type solutions that contain free variables in parameter and return types.
When calling a method which already has a type annotation we have to consider adding a capture conversion in form of a let statement.
The constraint $\tv{p} \lessdot \exptype{List}{\wtv{x}}$ signals the \unify{} algorithm that here a capture conversion is possible.
$\sigma(\tv{p}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, \sigma(\tv{r}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, $ is a possible solution.
But only when adding a capture conversion:
\begin{lstlisting}[style=fgj]
<X> List<X> clone(List<X> l);
(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){
return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
}
\end{lstlisting}
\unify{}'s type solution for constraints involving free variables only holds under special circumstances.
Constraint $\tv{p} \lessdot \exptype{List}{\wtv{x}}$ only holds when a capture conversion is applied to the left side:
$\Delta, \Delta' \vdash CC(\sigma(\tv{p})) <: \sigma(\exptype{List}{\wtv{x}})$
and there is a an environment $\Delta'$ holding all type variables used inside the subtype relation.
This is done by packing the method call inside a let statement, which performs a capture conversion on all expressions used as parameters.
%TODO: Explain (do soundness and TYPE algorithm first)
A type solution of the \unify{} algorithm only guarantees correct subtyping for constraints not containing free variables.
Constraints like $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ only guarantee
$\Delta, \Delta' \vdash \sigma(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) <: \sigma(\exptype{List}{\wtv{a}})$ when
adding a $\Delta'$ environment and applying a capture conversion on the left side.
In this case the type solution would be $\tv{a} \to \rwildcard{X}$ leading to:
$\Delta, \set{\rwildcard{X}} \vdash \exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$
This is the reason input constraints containing free variables cannot be stored in a set.
$\wtv{a} \lessdot \wtv{b}$ is not the same as $\wtv{a} \lessdot \wtv{b}$.
Both constraints will end up the same after a substitution for both placeholders $\tv{a}$ and $\tv{b}$.
But afterwards a capture conversion is applied, which can generate different types on the left sides.
\begin{itemize}
\item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Y}}$
\item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Z}}$
\end{itemize}
Also the subtype relation is not symmetric for types involving free type variables.
$\type{T} \lessdot \type{S}$ and $\type{S} \lessdot \type{T}$ doesnt mean $\type{T} = \type{S}$, because we apply a capture conversion on every constraint.
Only for constraints without free variables symmetry is given.
% Can untyped methods also get a capture conversion? NO!
%TODO: Explain why capture conversion is needed (also in respect to martins algorithm)
\input{Unify} \input{Unify}
\section{Limitations} \section{Limitations}

180
introduction.tex
View File

@ -7,7 +7,7 @@
\section{Type Inference for Java} \section{Type Inference for Java}
%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),
or allowing to write typeless Java code which is then type infered and thereby type checked by our algorithm. or allowing to write typeless Java code which is then type infered and thereby type checked by our algorithm.
The algorithm proposed in this paper can determine a correct typing for the untyped Java source code example shown in figure \ref{fig:intro-example-typeless}. The algorithm proposed in this paper can determine a correct typing for the untyped Java source code example shown in figure \ref{fig:intro-example-typeless}.
Our algorithm is also capable of finding solutions involving wildcards as shown in figure \ref{fig:intro-example-typed}. Our algorithm is also capable of finding solutions involving wildcards as shown in figure \ref{fig:intro-example-typed}.
@ -21,14 +21,16 @@ The \fjtype{} algorithm calculates constraints based on this intermediate repres
which are then solved by the \unify{} algorithm which are then solved by the \unify{} algorithm
resulting in a correctly typed program (see figure \ref{fig:nested-list-example-typed}). resulting in a correctly typed program (see figure \ref{fig:nested-list-example-typed}).
\begin{itemize}
\item
We support capture conversion and Java style method calls. We support capture conversion and Java style method calls.
This requires existential types in a form which is not denotable by Java syntax \cite{aModelForJavaWithWildcards}. This requires existential types in a form which is not denotable by Java syntax \cite{aModelForJavaWithWildcards}.
\item
We present a novel approach to deal with existential types and capture conversion during constraint unification. We present a novel approach to deal with existential types and capture conversion during constraint unification.
The algorithm is split in two parts. A constraint generation step and an unification step. The algorithm is split in two parts. A constraint generation step and an unification step.
\item
We proof soundness and aim for a good compromise between completeness and time complexity. We proof soundness and aim for a good compromise between completeness and time complexity.
\end{itemize}
% Our algorithm finds a correct type solution for the following example, where the Java local type inference fails: % Our algorithm finds a correct type solution for the following example, where the Java local type inference fails:
% \begin{verbatim} % \begin{verbatim}
% class SuperPair<A,B>{ % class SuperPair<A,B>{
@ -47,7 +49,7 @@ We proof soundness and aim for a good compromise between completeness and time c
% } % }
% \end{verbatim} % \end{verbatim}
\begin{figure}[tp] \begin{figure}%[tp]
\begin{subfigure}[t]{\linewidth} \begin{subfigure}[t]{\linewidth}
\begin{lstlisting}[style=fgj] \begin{lstlisting}[style=fgj]
class List<A> { class List<A> {
@ -117,7 +119,7 @@ class Example {
% The goal is to proof soundness in respect to the type rules introduced by \cite{aModelForJavaWithWildcards} % The goal is to proof soundness in respect to the type rules introduced by \cite{aModelForJavaWithWildcards}
% and \cite{WildcardsNeedWitnessProtection}. % and \cite{WildcardsNeedWitnessProtection}.
\begin{figure}[tp] \begin{figure}%[tp]
\begin{subfigure}[t]{0.49\linewidth} \begin{subfigure}[t]{0.49\linewidth}
\begin{lstlisting}[style=fgj] \begin{lstlisting}[style=fgj]
genList() { genList() {
@ -158,17 +160,16 @@ List<?> genList() {
% The type inference algorithm has to find the correct type involving wildcards (\texttt{List<?>}). % The type inference algorithm has to find the correct type involving wildcards (\texttt{List<?>}).
\subsection{Java Wildcards} \subsection{Java Wildcards}
Wildcards are expressed by a \texttt{?} in Java and can be used as parameter types. Wildcards are expressed by a \texttt{?} in Java and can be used as type parameters.
Wildcards can be formalized as existential types \cite{WildFJ}.
\texttt{List<? extends Object>} and \texttt{List<? super String>} are both wildcard types
denoted in our syntax by $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$ and
$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
Wildcards add variance to Java type parameters. Wildcards add variance to Java type parameters.
Generally Java has invariant subtyping for polymorphic types. Generally Java has invariant subtyping for polymorphic types.
A \texttt{List<String>} is not a subtype of \texttt{List<Object>} for example A \texttt{List<String>} is not a subtype of \texttt{List<Object>} for example
even though it seems intuitive with \texttt{String} being a subtype of \texttt{Object}. even though it seems intuitive with \texttt{String} being a subtype of \texttt{Object}.
Wildcards can be formalized as existential types \cite{WildFJ}.
\texttt{List<? extends Object>} and \texttt{List<? super String>} are both wildcard types
denoted in our syntax by $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$ and
$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
$\exptype{List}{String} <: \wctype{\wildcard{X}{\bot}{\type{Object}}}{List}{\rwildcard{X}}$ $\exptype{List}{String} <: \wctype{\wildcard{X}{\bot}{\type{Object}}}{List}{\rwildcard{X}}$
means \texttt{List<String>} is a subtype of \texttt{List<? extend Object>}. means \texttt{List<String>} is a subtype of \texttt{List<? extend Object>}.
@ -179,17 +180,17 @@ In this case the name is $\rwildcard{X}$ and it's bound to the the type \texttt{
Those properties are needed to formalize capture conversion. Those properties are needed to formalize capture conversion.
Polymorphic method calls need to be wraped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}. Polymorphic method calls need to be wraped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}.
In Java this is done implicitly in a process called capture conversion. In Java this is done implicitly in a process called capture conversion.
When calling a polymorphic method like \texttt{<X> List<X> m(List<X> l1, List<X> l2)} with a \texttt{List<?>} % When calling a polymorphic method like \texttt{<X> List<X> m(List<X> l1, List<X> l2)} with a \texttt{List<?>}
it is not possible to substitute \texttt{?} for \texttt{X}. % it is not possible to substitute \texttt{?} for \texttt{X}.
This would lead to the method header \texttt{List<?> m(List<?> l1, List<?> l2)} % This would lead to the method header \texttt{List<?> m(List<?> l1, List<?> l2)}
where now a method invocation with \texttt{List<String>} and \texttt{List<Integer>} would be possible, % where now a method invocation with \texttt{List<String>} and \texttt{List<Integer>} would be possible,
because both are subtypes of \texttt{List<?>}. % because both are subtypes of \texttt{List<?>}.
Capture conversion solves this problem by generating a fresh type variable for every wildcard. % Capture conversion solves this problem by generating a fresh type variable for every wildcard.
Calling \texttt{<X> X head(List<X> l1)} with the type \texttt{List<?>} ($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$) % Calling \texttt{<X> X head(List<X> l1)} with the type \texttt{List<?>} ($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$)
creates a fresh type variable $\rwildcard{Y}$ resulting in % creates a fresh type variable $\rwildcard{Y}$ resulting in
$\generics{\rwildcard{Y}}\texttt{head}(\exptype{List}{\rwildcard{Y}})$ % $\generics{\rwildcard{Y}}\texttt{head}(\exptype{List}{\rwildcard{Y}})$
with $\rwildcard{Y}$ being used as generic parameter \texttt{X}. % with $\rwildcard{Y}$ being used as generic parameter \texttt{X}.
The $\rwildcard{Y}$ in $\exptype{List}{\rwildcard{Y}}$ is a free variable now. % The $\rwildcard{Y}$ in $\exptype{List}{\rwildcard{Y}}$ is a free variable now.
\subsection{Global Type Inference} \subsection{Global Type Inference}
% A global type inference algorithm works on an input with no type annotations at all. % A global type inference algorithm works on an input with no type annotations at all.
@ -383,3 +384,136 @@ concat(list, list);
The \unify{} algorithm only sees the constraints with no information about the program they originated from. 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}. 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}.
\subsection{Capture Conversion}
The input to our type inference algorithm does not contain let statements.
Those are added after computing a type solution.
Let statements act as capture conversion and only have to be applied in method calls involving wildcard types.
\begin{figure}
\begin{minipage}{0.45\textwidth}
\begin{lstlisting}[style=fgj]
<X> List<X> clone(List<X> l);
example(p){
return clone(p);
}
\end{lstlisting}
\end{minipage}%
\hfill
\begin{minipage}{0.5\textwidth}
\begin{lstlisting}[style=tfgj]
(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){
return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in
clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
}
\end{lstlisting}
\end{minipage}
\caption{Type inference adding capture conversion}\label{fig:addingLetExample}
\end{figure}
Figure \ref{fig:addingLetExample} shows a let statement getting added to the typed output.
The method \texttt{clone} cannot be called with the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
After a capture conversion \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$ with $\rwildcard{X}$ being a free variable.
Afterwards we have to find a supertype of $\exptype{List}{\rwildcard{X}}$, which does not contain free variables
($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in this case).
During the constraint generation step most types are not known yet and are represented by a type placeholder.
During a methodcall like the one in the \texttt{example} method in figure \ref{fig:ccExample} the type of the parameter \texttt{p}
is not known yet.
The type \texttt{List<?>} would be one possibility as a parameter type for \texttt{p}.
To make wildcards work for our type inference algorithm \unify{} has to apply capture conversions if necessary.
The type placeholder $\tv{r}$ is the return type of the \texttt{example} method.
One possible type solution is $\tv{p} \doteq \tv{r} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$,
which leads to:
\begin{verbatim}
List<?> example(List<?> p){
return clone(p);
}
\end{verbatim}
But by substituting $\tv{p} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in the constraint
$\tv{p} \lessdotCC \exptype{List}{\wtv{x}}$ leads to
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$.
To make this typing possible we have to introduce a capture conversion via a let statement:
$\texttt{return}\ (\texttt{let}\ \texttt{x} : \wctype{\rwildcard{X}}{List}{\rwildcard{X}} = \texttt{p}\ \texttt{in} \
\texttt{clone}\generics{\rwildcard{X}}(x) : \wctype{\rwildcard{X}}{List}{\rwildcard{X}})$
Inside the let statement the variable \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$
This spawns additional problems.
\begin{figure}
\begin{minipage}{0.45\textwidth}
\begin{verbatim}
<X> List<X> clone(List<X> l){...}
example(p){
return clone(p);
}
\end{verbatim}
\end{minipage}%
\hfill
\begin{minipage}{0.35\textwidth}
\begin{constraintset}
\textbf{Constraints:}\\
$
\tv{p} \lessdotCC \exptype{List}{\wtv{x}}, \\
\tv{p} \lessdot \tv{r}, \\
\tv{p} \lessdot \type{Object},
\tv{r} \lessdot \type{Object}
$
\end{constraintset}
\end{minipage}
\caption{Type inference example}\label{fig:ccExample}
\end{figure}
In addition with free variables this leads to unwanted behaviour.
Take the constraint
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ for example.
After a capture conversion from $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ to $\exptype{List}{\rwildcard{Y}}$ and a substitution $\wtv{a} \doteq \rwildcard{Y}$
we get
$\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$.
Which is correct if we apply capture conversion to the left side:
$\exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$
If the input constraints did not intend for this constraint to undergo a capture conversion then \unify{} would produce an invalid
type solution due to:
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \nless: \exptype{List}{\rwildcard{X}}$
The reason for this is the \texttt{S-Exists} rule's premise
$\text{dom}(\Delta') \cap \text{fv}(\exptype{List}{\rwildcard{X}}) = \emptyset$.
Additionally free variables are not allowed to leave the scope of a capture conversion
introduced by a let statement.
%TODO we combat both of this with wildcard type placeholders (? flag)
Type placeholders which are not flagged as possible free variables ($\wtv{a}$) can never hold a free variable or a type containing free variables.
Constraint generation places these standard place holders at method return types and parameter types.
\begin{lstlisting}[style=fgj]
<X> List<X> clone(List<X> l);
(*@$\red{\tv{r}}$@*) example((*@$\red{\tv{p}}$@*) p){
return clone(p);
}
\end{lstlisting}
This prevents type solutions that contain free variables in parameter and return types.
When calling a method which already has a type annotation we have to consider adding a capture conversion in form of a let statement.
The constraint $\tv{p} \lessdot \exptype{List}{\wtv{x}}$ signals the \unify{} algorithm that here a capture conversion is possible.
$\sigma(\tv{p}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, \sigma(\tv{r}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, $ is a possible solution.
But only when adding a capture conversion:
\begin{lstlisting}[style=fgj]
<X> List<X> clone(List<X> l);
(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){
return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
}
\end{lstlisting}
Capture constraints cannot be stored in a set.
$\wtv{a} \lessdotCC \wtv{b}$ is not the same as $\wtv{a} \lessdotCC \wtv{b}$.
Both constraints will end up the same after a substitution for both placeholders $\tv{a}$ and $\tv{b}$.
But afterwards a capture conversion is applied, which can generate different types on the left sides.
\begin{itemize}
\item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Y}}$
\item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Z}}$
\end{itemize}

121
letfjTransformation.tex Normal file
View File

@ -0,0 +1,121 @@
%We could do a translation from Java to \wildFJ explaining implicit capture conversion
\section{Soundness of Typing}
We show soundness with the type rules statet in \cite{WildcardsNeedWitnessProtection}.
A correct \FGJGT{} program can be converted to a correct \wildFJ{} program.
\begin{figure}
$\begin{array}{rcl}
| \texttt{x} |
& = & \texttt{x} \\
| \texttt{let} \ \texttt{x} : \type{T} = \texttt{e},\, \ol{x} : \ol{T} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x}) |
& = & |\texttt{e}|.\texttt{m}(\ol{|e|}) \\
| \texttt{let} \ \texttt{x} : \type{T} = \texttt{e}\ \texttt{in}\ \texttt{x}.\texttt{f} |
& = & |\texttt{e}|.\texttt{f} \\
| \texttt{e} \elvis{} \texttt{e} |
& = & |\texttt{e}| \elvis{} |\texttt{e}| \\
\end{array}$
\caption{Erasure} \label{fig:erasure}
\end{figure}
% A constraint Pair<A,B> <. a, then a has infinite possibilities:
% a =. X.Pair<X,X>
% a =. X,Y.Pair<X,Y>
% a =. X.Pair<Pair<X,X>,X>
% a =. X,Y.Pair<Pair<X,Y>,X>
% a =. X,Y.Pair<Pair<X,Y>,Y>
% There is no way to try out every single one of them.
Starting with the parameters of the method we gradually add every expression which only contains already captured expressions.
We have a typed expression
$|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} : \type{T} = \texttt{x in}$
$|\texttt{e.f}, \texttt{r}| = |\texttt{e}, x| \texttt{let} r = x.\texttt{f} \ \texttt{in}$
$|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} = \texttt{x in}$
%TODO: write the transform rules:
% |e.f, ret| = |e, r| let ret = r.f in
% |x, ret| = let ret = x in
% |e.m(e_), ret| = |e, r| |e_, a_| let ret = r.m(a_) in
Erasure functions:
$|\texttt{x}| = \texttt{let r} : \wcNtype{\Delta}{N} = \texttt{x in r}$
$\texttt{x} \longmapsto \texttt{let}\ \texttt{xx} : \type{T} = \texttt{x in xx}$
$\texttt{x}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in xf}$
$\begin{array}{l}
\texttt{e} \longmapsto \texttt{let}\ \texttt{xe} : \type{T} = \texttt{e}' \ \texttt{in xe} \\
\hline
\vspace*{-0.4cm}\\
\texttt{e}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in x}.f
\end{array}$
Example:
m(a, b) = a.m(b.f);
let xa = a in let xb = b in let xf = xb.f in let xm = xa.m(xf) in xm
% TODO: Now we have to proof that there is a LetFJ program for every TIFJ program!
% |let xr : T = x1.m(x2) in e| = [x1.m(x2)/xr]|e|
% |let xf : T = x1.f in e| = [x1.f/xf]|e|
% |let xr : T = x in e| = [xr/x]|e|
% |new C(x)| = new C(x)
% | let xr : T' = x in let xf : T = xr.f | = x.f
% let x : T' = e' in x = |e|
% ---------------------------------
% | let xr : T' = x in let xf : T = xr.f | = x.f
% let x : T' = e' in x = |e|
% -----------
% =
We need a language which only has let statemnts and expressions on capture converted variables
The idea is to use wildcard placeholders inside the method. Also in the bounds of wildcards.
This makes it possible to replace wildcards with free variables by setting upper and lower bound to that free variable.
Free variables then can flow freely inside the method body.
We have to show that a type solution implies that there is a possible transformation to a correct typed letFJ program.
If there is a possible method type then there must exist a let configuration.
% By starting with the parameter types and capturing them. Afterwards every capture creates free variables which are used inside
% TODO: Proof!
The normal type placeholders represent denotable types.
%TODO: the type rules stay the same. We generate let statements in a fashion which removes all wildcard types.
% what about wildcards getting returned by untyped methods? they can also be captured
% TODO: try soundness proof on the original type rules!
Removing of extensive wildcards:
$
\wctype{\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{X}, \rwildcard{Y}}
\lessdot \wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}} \\
\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \wtv{x}, \rwildcard{Y} \doteq \wtv{x} \\
\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \rwildcard{Y} \\
\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
\implies \wctype{\wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{Y}, \rwildcard{Y}}, \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
$
%e.f leads to constraints: r <c C<x> with return type equals the field type T.
% T can contain free variables from r. but also it can be used in another constraint and get free variables from inner let statements
% X.C<X> <c C<x> -> then T contains X variables
% let x1 = p1, x2 = p2 in
% let r1 = x1 in let r2 = p2 in let f1 = r2.f in let r3 = x1 in let m2 = r3.m2() let ret = r1.m(f1,m2)
% in ret
What about method invocation with no type yet. m2 :: a -> a
they are also encased in let expression so the return type can be capture converted.
Those methods and the parameter types of the current method are the only things not typed.
All the other types cannot change their type. The captured wildcards can only flow from top to bottom.
The return type of untyped methods has to be well-formed and cannot contain free variables.
Therefore no free variables will flow into those types.