668 lines
34 KiB
TeX
668 lines
34 KiB
TeX
|
|
%TODO:
|
|
% -Explain <c
|
|
% - Kapitel 1.2 + 1.3 ist noch zu komplex
|
|
% - Constraints und Unifikation erklären, bevor Unifikation erwähnt wird
|
|
|
|
%Inhalt:
|
|
% Global type inference example (the sameList example)
|
|
% Wildcards are needed because Java has side effects
|
|
% Capture Conversion
|
|
% 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{Introduction}
|
|
\label{sec:introduction}
|
|
|
|
Type inference is a hallmark of functional programming, where it
|
|
improves readability and conciseness while
|
|
enabling safe rapid prototyping by allowing the compiler to deduce
|
|
types automatically without explicit type annotations. It allows
|
|
developers to safely refactor their programs before fixing function
|
|
signatures. In object-oriented programming (OOP), however, the use of
|
|
type inference is more restricted. It is often employed for local
|
|
variables and the instantiation of generic type parameters, offering
|
|
similar readability and conciseness benefits as in functional
|
|
programming. In languages like Java, the overall architecture of
|
|
method signatures must be designed by the programmer up-front.
|
|
|
|
Java features a limited form of local type inference for local
|
|
variables defined with the \texttt{var} keyword, lambda expressions,
|
|
and method calls. Java infers the type of variables defined with
|
|
\texttt{var}. The rationale here is that instantiations of generic
|
|
types (e.g., maps of maps) are often unwiedly and they can be easily
|
|
inferred from the initializing expression. The type of a lambda
|
|
expression is inferred from the target type, i.e., the type of the
|
|
method argument that accepts the lambda. The rationale is the intended
|
|
use of lambdas as callback functions for listeners etc. For calls
|
|
to generic methods, Java infers the most specific instantiation of the
|
|
generic parameters for each individual call.
|
|
|
|
The local type inference features of Java add some convenience, but
|
|
programmers still have to provide method signatures beforehand. So there
|
|
is scope for a global type inference algorithm that infers
|
|
method signatures even if no type information (except class headers
|
|
and types of field variables) is given.
|
|
We present such a global type inference algorithm for Featherweight
|
|
Generic Java with wildcards, a Java core calculus with generics and
|
|
wildcards in the tradition of Featherweight Java \cite{FJ} and its
|
|
extensions \cite{WildFJ,WildcardsNeedWitnessProtection}. Our approach can also be used for regular Java programs,
|
|
but we limit the formal presentation to this core calculus.
|
|
|
|
%The goal is to find a correct typing for a given Java program.
|
|
Our algorithm enables programmers to write Java code with only a
|
|
minimum of type annotations (class headers and types of field
|
|
variables), it can fill in missing type annotations in partially
|
|
type-annotated programs, and it can suggest better (more general)
|
|
types for ordinary, typed Java programs.
|
|
|
|
Listing~\ref{lst:intro-example-typeless} shows an example input of a
|
|
method implementation without any type annotation. Our algorithm
|
|
infers the type annotations in Listing~\ref{lst:intro-example-typed}:
|
|
it adds the type arguments to \texttt{List} at object creation and it
|
|
infers the most specific return type \texttt{List<?>}, which is a
|
|
wildcard type. Our algorithm is the first to infer wildcard types that
|
|
comes with a soundness proof.
|
|
Previous work on global type inference for Java either does not
|
|
consider wildcards or it simplifies the problem by not modeling key
|
|
features of Java wildcards.
|
|
|
|
|
|
%The algorithm proposed in this paper can determine a correct typing for the untyped Java source code example shown in listing \ref{lst:intro-example-typeless}.
|
|
%In this case our algorithm would also be able to propose a solution including wildcards as shown in listing \ref{lst:intro-example-typed}.
|
|
|
|
%This paper extends a type inference algorithm for Featherweight Java \cite{TIforFGJ} by adding wildcards.
|
|
%The last step to create a type inference algorithm compatible to the Java type system.
|
|
|
|
|
|
\begin{figure}[tp]
|
|
\begin{minipage}{0.43\textwidth}
|
|
\begin{lstlisting}[style=java,label=lst:intro-example-typeless,caption=Missing return type]
|
|
genList() {
|
|
if( ... ) {
|
|
return new List(1);
|
|
} else {
|
|
return new List("Str");
|
|
}
|
|
}
|
|
\end{lstlisting}
|
|
\end{minipage}%
|
|
\hfill
|
|
\begin{minipage}{0.55\textwidth}
|
|
\begin{lstlisting}[style=tfgj,caption=Type inference solution,label=lst:intro-example-typed]
|
|
List<?> genList() {
|
|
if( ... ) {
|
|
return new List<Integer>(1);
|
|
} else {
|
|
return new List<String>("Str");
|
|
}
|
|
}
|
|
\end{lstlisting}
|
|
\end{minipage}
|
|
\end{figure}
|
|
|
|
|
|
|
|
Global Type Inference for Featherweight Java \cite{TIforFGJ} is a
|
|
sound, but incomplete inference algorithm for Featherweight Generic
|
|
Java. It does not support wildcards, which means that it infers the
|
|
return type \texttt{Object} for the method \texttt{genList} in
|
|
Listing~\ref{lst:intro-example-typeless}. Like our algorithm, their
|
|
algorithm restricts to monomorphic recursion, which leads to
|
|
incompleteness.
|
|
|
|
|
|
A type unification algorithm for Java with wildcards \cite{plue09_1} states the same capabilities,
|
|
but it does not handle capture conversion correctly because it only supports types which are expressible in Java syntax (more details in
|
|
section~\ref{challenges}).
|
|
Moreover, it appears that the subtype relation changes depending on whether a type is used as an argument to a method invocation.
|
|
We resolve this problem by modeling Java wildcards as existential
|
|
types \cite{WildFJ,WildcardsNeedWitnessProtection}, which also serve
|
|
as the basis of our soundness proof.
|
|
% forces us to define a new kind of subtype constraint. %, the current state of the art
|
|
%and is able to deal with types that are not directly denotable in Java.
|
|
|
|
|
|
%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.
|
|
|
|
|
|
\begin{lstlisting}[caption=Part of a valid Java program, style=tfgj, label=lst:tiExample,float=tp]
|
|
<T> List<T> emptyList() { ... }
|
|
|
|
List<String> ls = emptyList();
|
|
\end{lstlisting}
|
|
Standard Java provides type inference in a restricted form % namely {Local Type Inference}.
|
|
which only works for local environments where the surrounding context has known types.
|
|
The example in Listing~\ref{lst:tiExample} exhibits the main differences to our global type inference algorithm.
|
|
The method call \texttt{emptyList} lacks its type parameters.
|
|
Java relies on a matching algorithm \cite{javaTIisBroken} to instantiate \texttt{T} with \texttt{String}
|
|
resulting in the correct expected type \texttt{List<String>}.
|
|
This local type inference depends on the type annotation on the left side of the assignment.
|
|
When calling the \texttt{emptyList} method without this type context
|
|
its return value will be inferred as \texttt{List<Object>}.
|
|
Therefore, Java rejects the code snippet in Listing~\ref{lst:tiLimit}:
|
|
it infers the type \texttt{List<Object>} for
|
|
\texttt{emptyList()} instead of the required
|
|
$\exptype{List}{\exptype{List}{String}}$.
|
|
\begin{lstlisting}[caption=Limitations of Java's Type Inference,
|
|
label=lst:tiLimit, float=tp]
|
|
emptyList().add(new List<String>())
|
|
.get(0)
|
|
.get(0); //Typing Error
|
|
\end{lstlisting}
|
|
%List<String> <. A
|
|
%List<A> <: List<B>, B <: List<C>
|
|
% B = A and therefore A on the left and right side of constraints.
|
|
% this makes matching impossible
|
|
Hence, the second call to \texttt{get} produces a type error.
|
|
|
|
The type inference algorithm presented in this paper correctly instantiates the type parameter \texttt{T} of the \texttt{emptyList}
|
|
method with \texttt{List<List<String>>} and render this code snippet correct.
|
|
|
|
|
|
% %motivate constraints:
|
|
% To solve this example our Type Inference algorithm will create constraints
|
|
% $
|
|
% \exptype{List}{\tv{a}} \lessdot \tv{b},
|
|
% \tv{b} \lessdot \exptype{List}{\tv{c}},
|
|
% \tv{c} \lessdot \exptype{List}{\tv{d}}
|
|
% $
|
|
|
|
|
|
|
|
%\subsection{Conclusion}
|
|
% Additions: TODO
|
|
% - Global Type Inference Algorithm, no type annotations are needed
|
|
% - Soundness Proof
|
|
% - Easy to implement
|
|
% - Capture Conversion support
|
|
% - Existential Types support
|
|
We summarize our contributions:
|
|
\begin{itemize}
|
|
\item
|
|
We introduce the language \tifj{} (section \ref{sec:tifj}),
|
|
a Featherweight Java derivative including generics, wildcards, and type inference.
|
|
\item
|
|
Our algorithm handles existential types in a form which is not
|
|
denotable by Java syntax \cite{aModelForJavaWithWildcards}. Thus, we support capture conversion and Java style method calls.
|
|
\item
|
|
We present a novel approach to deal with existential types and capture conversion during constraint unification.
|
|
% \item The algorithm is split in two parts. A constraint generation step and an unification step.
|
|
% Input language and constraint generations can be extended without altering the unification part.
|
|
\item
|
|
We prove 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:
|
|
% \begin{verbatim}
|
|
% class SuperPair<A,B>{
|
|
% A a;
|
|
% B b;
|
|
% }
|
|
% class Pair<A,B> extends SuperPair<B,A>{
|
|
% A a;
|
|
% B b;
|
|
|
|
% <X> X choose(X a, X b){ return b; }
|
|
|
|
% String m(List<? extends Pair<Integer, String>> a, List<? extends Pair<Integer, String>> b){
|
|
% return choose(choose(a,b).value.a,b.value.b);
|
|
% }
|
|
% }
|
|
% \end{verbatim}
|
|
|
|
|
|
% \subsection{Wildcards}
|
|
% Java subtyping involving generics is invariant.
|
|
% For example \texttt{List<String>} is not a subtype of \texttt{List<Object>}.
|
|
% %Wildcards introduce variance by allowing \texttt{List<String>} to be a subtype of \texttt{List<?>}.
|
|
|
|
% \texttt{List<Object>} is not a valid return type for the method \texttt{genList}.
|
|
% The type inference algorithm has to find the correct type involving wildcards (\texttt{List<?>}).
|
|
|
|
\section{Java Wildcards}
|
|
\label{sec:java-wildcards}
|
|
|
|
As Java is an imperative language, subtyping for generic types is invariant.
|
|
%but it incooperates use-site variance via so called wildcard types.
|
|
Even though \texttt{String} is subtype of \texttt{Object},
|
|
a \texttt{List<String>} is not a subtype of \texttt{List<Object>}:
|
|
because someone might store an \texttt{Integer} in the list, which is
|
|
compatible with \texttt{Object}, but not with \texttt{String} (see Listing~\ref{lst:invarianceExample}).
|
|
|
|
Invariance is overly restrictive in read-only or write-only
|
|
contexts. Hence, Java incooperates use-site variance by allowing wildcards (\texttt{?}) in types.
|
|
For example, the type \texttt{List<?>} (short for \texttt{List<? extends Object>}, with \texttt{?} being a placeholder for any type)
|
|
is a supertype of \texttt{List<String>} and \texttt{List<Object>}.
|
|
%The \texttt{?} is a wildcard type which can be replaced by any type as needed.
|
|
%
|
|
Listing~\ref{lst:wildcardIntro} shows a use of wildcards that renders the assignment \texttt{lo = ls} correct.
|
|
The program still does not compile, because the addition of an \texttt{Integer} to \texttt{lo} is still incorrect.
|
|
|
|
\begin{figure}[tp]
|
|
\begin{minipage}{0.48\textwidth}
|
|
\begin{lstlisting}[caption=Java Invariance Example,label=lst:invarianceExample]{java}
|
|
List<String> ls = ...;
|
|
List<Object> lo = ...;
|
|
lo = ls; // typing error!
|
|
lo.add(new Integer(1));
|
|
\end{lstlisting}
|
|
\end{minipage}
|
|
\hfill
|
|
\begin{minipage}{0.5\textwidth}
|
|
\begin{lstlisting}[caption=Use-Site Variance Example,label=lst:wildcardIntro]{java}
|
|
List<String> ls = ...;
|
|
List<? extends Object> lo = ...;
|
|
lo = ls; // correct
|
|
lo.add(new Integer(1)); // error!
|
|
\end{lstlisting}
|
|
\end{minipage}
|
|
\end{figure}
|
|
|
|
Wildcard types like \texttt{List<?>} are virtual types, i.e., the run-time
|
|
type of an object is always a fully instantiated type like
|
|
\texttt{List<String>} or \texttt{List<Object>}.
|
|
The issue is that the run-time type underlying a wildcard type can
|
|
change at any time, for example when multiple threads share a reference to the same field.
|
|
Hence, a wildcard \texttt{?} must be considered a different type everytime it is accessed.
|
|
For that reason, the call to the method \texttt{concat} with two wildcard lists in Listing~\ref{lst:concatError} is rejected.
|
|
% 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}[tp]
|
|
\begin{lstlisting}[caption=Wildcard Example with faulty call to a concat method,label=lst:concatError]{java}
|
|
<X> List<X> concat(List<X> l1, List<X> l2){
|
|
return l1.addAll(l2);
|
|
}
|
|
|
|
List<?> l1 = new List<String>("foo");
|
|
List<?> l2 = new List<Integer>(1); // List containing Integer
|
|
|
|
concat(l1, l2); // Error! Would concat two different lists
|
|
\end{lstlisting}
|
|
\end{figure}
|
|
|
|
To determine the correctness of method calls involving wildcard types Java's typechecker
|
|
makes use of a concept called \textbf{capture conversion}.
|
|
% was designed to make Java wildcards useful.
|
|
% - without capture conversion
|
|
% - is used to open wildcard types
|
|
% -
|
|
One way to formalize this concept is by replacing wildcards with
|
|
existential types and modeling capture conversion with suitably
|
|
inserted let statements \cite{WildcardsNeedWitnessProtection}.
|
|
Our Featherweight Java derivative called \TamedFJ{} is modeled after
|
|
Bierhoff's calculus \cite{WildcardsNeedWitnessProtection} (see section~\ref{sec:tifj}).
|
|
To express the example in Listing~\ref{lst:wildcardIntro} in our calculus we first translate the wildcard types:
|
|
\texttt{List<? extends Object>} becomes
|
|
$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$,
|
|
where the existentially bound variable \texttt{A} has a lower bound
|
|
$\bot$ and an upper bound $\type{Object}$.
|
|
Before we can call the \texttt{add} method on this type we perform
|
|
capture conversion by inserting a let statement:
|
|
\begin{lstlisting}
|
|
let v : (*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$@*) = lo in v.<A>add(new Integer(1));
|
|
\end{lstlisting}
|
|
The variable \expr{lo} (from Listing~\ref{lst:wildcardIntro}) is
|
|
assigned to a new immutable variable \expr{v} with type
|
|
$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$,
|
|
but inside the let statement the variable \expr{v} will be treated as
|
|
$\exptype{List}{\rwildcard{A}}$.
|
|
Here $\rwildcard{A}$ is a fresh variable or a captured wildcard.
|
|
The only information we have about $\rwildcard{A}$ is that it is a
|
|
supertype of $\bot$ and a subtype of $\type{Object}$
|
|
It is important to give the captured wildcard type $\rwildcard{A}$ an unique name which is used nowhere else.
|
|
This approach also clarifies why the method call to \texttt{concat}
|
|
in listing \ref{lst:concatError} is rejected (see Listing~\ref{lst:concatTamedFJ}).
|
|
\begin{figure}[tp]
|
|
\begin{lstlisting}[style=TamedFJ,caption=\TamedFJ{} representation of the concat call from listing \ref{lst:concatError}, 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}
|
|
|
|
% % TODO intro to Featherweight Java
|
|
% is a formal model of the Java programming language reduced to a core set of instructions.
|
|
% - We extend this model by existential types and let expressions.
|
|
% - We copy this from \ref{WildFJ} but make type annotations optional
|
|
% - Our calculus is called \TamedFJ{}
|
|
% - \TamedFJ{} binds every method argument with a let statement.
|
|
|
|
% 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.
|
|
% Let's have a look at a representation of the \texttt{add} call from the last line in listing \ref{lst:wildcardIntro} with our calculus \TamedFJ{}:
|
|
% %The \texttt{add} call in listing \ref{lst:wildcardIntro} needs to be encased by a \texttt{let} statement in our calculus.
|
|
% %This makes the capture converion explicit.
|
|
% \begin{lstlisting}
|
|
% let v : (*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$@*) = lo in v.<A>add(new Integer(1));
|
|
% \end{lstlisting}
|
|
% The method call is encased in a \texttt{let} statement and
|
|
% \expr{lo} is assigned to a new variable \expr{v} of \linebreak[2]
|
|
% \textbf{Existential Type} $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$.
|
|
% Our calculus uses existential types \cite{WildFJ} to formalize wildcards:
|
|
% \texttt{List<? extends Object>} is translated to $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$
|
|
% and \texttt{List<? super String>} is expressed as $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
|
|
% The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound,
|
|
% and a type they are bound to.
|
|
% In this case the name is $\rwildcard{A}$ and it's bound to the the type \texttt{List}.
|
|
% Inside the \texttt{let} statement the variable \expr{v} has the type
|
|
% $\exptype{List}{\rwildcard{A}}$.
|
|
% This is an explicit version of \linebreak[2]
|
|
% \textbf{Capture Conversion},
|
|
% which makes use of the fact that a concrete type must be behind every wildcard type.
|
|
% There is no instantiation of a \texttt{List<?>},
|
|
% but there exists some unknown type $\exptype{List}{\rwildcard{A}}$, with $\rwildcard{A}$ inbetween the bounds $\bot$ (bottom type, subtype of all types) and
|
|
% \texttt{Object}.
|
|
% Inside the body of the let statement \expr{v} is treated as a value with the constant type $\exptype{List}{\rwildcard{A}}$.
|
|
% Existential types enable us to formalize \textit{Capture Conversion}.
|
|
% Polymorphic method calls need to be wrapped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}.
|
|
% In Java this is done implicitly in a process called capture conversion (as proposed in Wild FJ \cite{WildFJ}).
|
|
|
|
|
|
\section{Global Type Inference Algorithm}
|
|
|
|
\begin{figure}[h]
|
|
\begin{minipage}{0.49\textwidth}
|
|
\begin{lstlisting}[style=tfgj, caption=Valid Java program, label=lst:addExample]
|
|
<A> List<A> add(List<A> l, A v)
|
|
|
|
List<? super String> l = ...;
|
|
add(l, "String");
|
|
\end{lstlisting}
|
|
\end{minipage}\hfill
|
|
\begin{minipage}{0.49\textwidth}
|
|
\begin{lstlisting}[style=tamedfj, caption=\TamedFJ{} representation, label=lst:addExampleLet]
|
|
<A> List<A> add(List<A> l, A v)
|
|
List<? super String> l = ...;
|
|
let v:(*@$\tv{v}$@*) = l
|
|
in add(v, "String");
|
|
\end{lstlisting}
|
|
\end{minipage}\\
|
|
\begin{minipage}{0.49\textwidth}
|
|
\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:addExampleCons]
|
|
(*@$\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}} \lessdot \tv{v}$@*)
|
|
(*@$\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$@*)
|
|
(*@$\type{String} \lessdot \wtv{a}$@*)
|
|
\end{lstlisting}
|
|
\end{minipage}\hfill
|
|
\begin{minipage}{0.49\textwidth}
|
|
\begin{lstlisting}[style=letfj, caption=Type solution, label=lst:addExampleSolution]
|
|
<A> List<A> add(List<A> l, A v)
|
|
List<? super String> l = ...;
|
|
let l2:(*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = l
|
|
in <X>add(l2, "String");
|
|
\end{lstlisting}
|
|
\end{minipage}
|
|
\end{figure}
|
|
|
|
% \begin{description}
|
|
% \item[input] \tifj{} program
|
|
% \item[output] type solution
|
|
% \item[postcondition] the type solution applied to the input must yield a valid \letfj{} program
|
|
% \end{description}
|
|
|
|
%Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
|
|
Listings \ref{lst:addExample}, \ref{lst:addExampleLet}, \ref{lst:addExampleCons}, and
|
|
\ref{lst:addExampleSolution} showcase our global type inference algorithm step by step.
|
|
In this example we know that the type of the variable \texttt{l} is an existential type and has to undergo a capture conversion
|
|
before being passed to a method call.
|
|
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}.
|
|
Afterwards unknown types are replaced by type placeholders ($\tv{v}$ for the type of \texttt{v}) and constraints are generated (see \ref{lst:addExampleCons}).
|
|
These constraints mirror the type rules of our \TamedFJ{} calculus.
|
|
% 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}}$.
|
|
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.
|
|
Now our unification algorithm \unify{} (defined in chapter \ref{sec:unify}) is used to solve these constraints.
|
|
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.
|
|
%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:
|
|
|
|
\begin{displaymath}
|
|
\prftree[r]{Capture}{
|
|
\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}, \, \type{String} \lessdotCC \wtv{a}
|
|
}{
|
|
\wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
|
|
}
|
|
\end{displaymath}
|
|
|
|
%Capture Constraints $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ allow for a capture conversion,
|
|
%which converts a constraint of the form $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ to $(\exptype{C}{\rwildcard{X}} \lessdot \type{T})$
|
|
The constraint $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$
|
|
allows \unify{} to do a capture conversion to $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
|
|
The captured wildcard $\rwildcard{X}$ gets a fresh name and is stored in the wildcard environment of the \unify{} algorithm.
|
|
Leaving us with the solution $\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$, $\type{String} \lessdot \rwildcard{Y}$
|
|
The constraint $\type{String} \lessdot \rwildcard{Y}$ is satisfied
|
|
because $\rwildcard{Y}$ has $\type{String}$ as lower bound.
|
|
|
|
|
|
A correct Featherweight Java program including all type annotations and an explicit capture conversion via let statement is shown in listing \ref{lst:addExampleSolution}.
|
|
This program can be deducted from the type solution of our \unify{} algorithm presented in chapter \ref{sec:unify}.
|
|
In the body of the let statement the type $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$
|
|
becomes $\exptype{List}{\rwildcard{X}}$ and the wildcard $\wildcard{X}{\type{Object}}{\type{String}}$ is free and can be used as
|
|
a type parameter to method call \texttt{<X>add(v, "String")}.
|
|
|
|
% The input to our type inference algorithm is a modified version of the calculus in \cite{WildcardsNeedWitnessProtection} (see chapter \ref{sec:tifj}).
|
|
% First \fjtype{} (see section \ref{chapter:constraintGeneration}) generates constraints
|
|
% and afterwards \unify{} (section \ref{sec:unify}) computes a solution for the given constraint set.
|
|
% Constraints consist out of subtype constraints $(\type{T} \lessdot \type{T})$ and capture constraints $(\type{T} \lessdotCC \type{T})$.
|
|
% \textit{Note:} a type $\type{T}$ can either be a named type, a type placeholder or a wildcard type placeholder.
|
|
% A subtype constraint is satisfied if the left side is a subtype of the right side according to the rules in figure \ref{fig:subtyping}.
|
|
% \textit{Example:} $\exptype{List}{\ntv{a}} \lessdot \exptype{List}{\type{String}}$ is fulfilled by replacing type placeholder $\ntv{a}$ with the type $\type{String}$.
|
|
% Subtype constraints and type placeholders act the same as the ones used in \emph{Type Inference for Featherweight Generic Java} \cite{TIforFGJ}.
|
|
% The novel capture constraints and wildcard placeholders are needed for method invocations involving wildcards.
|
|
|
|
% The central piece of this type inference algorithm, the \unify{} process, is described with implication rules (chapter \ref{sec:unify}).
|
|
% We try to keep the branching at a minimal amount to improve runtime behavior.
|
|
% Also the transformation steps of the \unify{} algorithm are directly related to the subtyping rules of our calculus.
|
|
% There are no informal parts in our \unify{} algorithm.
|
|
% It solely consist out of transformation rules which are bound to simple checks.
|
|
|
|
\subsection{Challenges}\label{challenges}
|
|
%TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
|
|
|
|
% Wildcards are not reflexive.
|
|
% ( on the equals property ), every wildcard has to be capture converted when leaving its scope
|
|
|
|
% do not substitute free type variables
|
|
|
|
Global Type inference for Featherweight Java with generics but without wildcards is solved already.
|
|
But adding Wildcards to the calculus creates new problems we did not foresee
|
|
and which have not been recognized by an existing type unification algorithm for Java with wildcards \ref{plue09_1}.
|
|
% what is the problem?
|
|
% Java does invisible capture conversion steps
|
|
Java Wildcard types are represented as existential types and have to be opened before they can be used.
|
|
This can either be done implicitly (\cite{aModelForJavaWithWildcards}, \cite{javaTIisBroken}) or explicitly via let statements (\cite{WildcardsNeedWitnessProtection}).
|
|
For all of those variations it is vital to know the argument types with which a method is called.
|
|
But our input program does not contain any type annotations.
|
|
We do not know where an existential type will emerge and where a capture conversion is necessary.
|
|
This has to be figured out during the type inference algorithm.
|
|
We detected three main challenges related to Java Wildcards and Global Type Inference:
|
|
\begin{enumerate}
|
|
\item \label{challenge:1}
|
|
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.
|
|
|
|
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.
|
|
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}}$.
|
|
|
|
% \textbf{Solution:}
|
|
% Capture Conversion during Unify.
|
|
|
|
\item
|
|
\unify{} morphs a constraint set into a correct type solution
|
|
gradually assigning types to type placeholders during that process.
|
|
Solved constraints are removed and never considered again.
|
|
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}}$.
|
|
\begin{verbatim}
|
|
anyList() = new List<String>() :? new List<Integer>()
|
|
|
|
add(anyList(), anyList().head());
|
|
\end{verbatim}
|
|
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
|
|
\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}}$
|
|
is solved by removing the wildcard $\rwildcard{X}$ if possible.
|
|
|
|
this problem is solved by ANF transformation
|
|
|
|
\item \textbf{Wildcards as Existential Types:}
|
|
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}
|
|
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 \label{challenge3} \textbf{Free Variables cannot leaver their scope}:
|
|
|
|
\begin{example}
|
|
Take the Java program in listing \ref{lst:mapExample} for example.
|
|
It maps every element of a list
|
|
$\expr{l} : \exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$
|
|
to a polymorphic \texttt{id} method.
|
|
We want to use our \unify{} algorithm to determine the correct type for the
|
|
variable \expr{l2}.
|
|
Although we do not specify constraint generation for language constructs like
|
|
lambda expressions used in this example,
|
|
we can imagine that the constraints have to look something like this:
|
|
|
|
\begin{minipage}{0.45\textwidth}
|
|
\begin{lstlisting}[caption=List Map Example,label=lst:mapExample]
|
|
<X> List<X> id(List<X> l){ ... }
|
|
List<List<?>> ls;
|
|
l2 = l.map(x -> id(x));
|
|
\end{lstlisting}\end{minipage}
|
|
\hfill
|
|
\begin{minipage}{0.45\textwidth}
|
|
\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:mapExampleCons]
|
|
(*@$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}}$@*)
|
|
(*@$\exptype{List}{\wtv{x}} \lessdot \tv{z},$@*)
|
|
(*@$\exptype{List}{\tv{z}} \lessdot \tv{l2}$@*)
|
|
\end{lstlisting}
|
|
\end{minipage}
|
|
|
|
The constraints
|
|
$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}},
|
|
\exptype{List}{\wtv{x}} \lessdot \tv{z}$
|
|
stem from the body of the lambda expression
|
|
\texttt{id(x)}.
|
|
\textit{For clarification:} This method call would be represented as the following expression in \letfj{}:
|
|
\texttt{let x1 :$\wctype{\rwildcard{A}}{List}{\rwildcard{A}}$ = x in id(x) :$\tv{z}$}
|
|
|
|
The T-Let rule prevents us from using free variables created by the method call to \expr{id}
|
|
to be used in the return type $\tv{z}$.
|
|
But this has to be signaled to the \unify{} algorithm, which does not know about the origin and context of
|
|
the constraints.
|
|
If we naively substitute $\sigma(\tv{z}) = \exptype{List}{\rwildcard{A}}$
|
|
the return type of the \texttt{map} function would be the type $\exptype{List}{\exptype{List}{\rwildcard{A}}}$.
|
|
This type solution is unsound.
|
|
The type of \expr{l2} is the same as the one of \expr{l}:
|
|
$\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$
|
|
|
|
\textbf{Solution:}
|
|
We solve this by distinguishing between wildcard placeholders and normal placeholders.
|
|
$\ntv{z}$ is a normal placeholder and is not allowed to contain free variables.
|
|
|
|
\end{example}
|
|
|
|
\end{enumerate}
|
|
|
|
%TODO: Move this part. or move the third challenge some underneath.
|
|
|
|
%%% Local Variables:
|
|
%%% mode: latex
|
|
%%% TeX-master: "TIforWildFJ"
|
|
%%% End:
|