417 lines
23 KiB
TeX
417 lines
23 KiB
TeX
|
|
\section{Global Type Inference Algorithm}
|
|
\label{sec:glob-type-infer}
|
|
|
|
This section gives an overview of the global type inference algorithm
|
|
with examples and identifies the challenges that we had to overcome in
|
|
the design of the 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=tamedfj, 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 the global type inference algorithm step by step.
|
|
Note that regular Java code snippets are displayed in a grey box, \TamedFJ{} programs are yellow
|
|
and constraints have a red background.
|
|
%This example is fully typed except for the method call \texttt{add} missing its type parameters.
|
|
In the Java code in Listing~\ref{lst:addExample}, the type of variable
|
|
\texttt{l} is an existential type so that it has to undergo a capture conversion
|
|
before being passed to a method call.
|
|
To this end we convert the program to A-Normal form (Listing~\ref{lst:addExampleLet}),
|
|
which introduces a let statement defining a new variable \texttt{v}.
|
|
The constraint generation step also assigns type placeholders to all variables missing a type annotation.
|
|
%In this case the variable \texttt{v} gets the type placeholder $\tv{v}$ (also shown in listing \ref{lst:addExampleCons})
|
|
%during the constraint generation step.
|
|
In this case the algorithm puts the type
|
|
placeholder $\tv{v}$ for the type of \texttt{v} before generating constraints (see Listing~\ref{lst:addExampleCons}).
|
|
These constraints mirror the typing rules of the \TamedFJ{} calculus (section~\ref{sec:tifj}).
|
|
% During the constraint generation step the type of the variable \texttt{v} is unknown
|
|
% and given the type placeholder $\tv{v}$.
|
|
The call to \texttt{add} generates the \emph{capture constraint} $\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$.
|
|
This constraint ($\lessdotCC$) is a kind of subtype constraint, which additionally
|
|
expresses that the left side of the constraint is subject to a capture conversion.
|
|
Next, the unification algorithm \unify{} (section~\ref{sec:unify}) solves the constraints.
|
|
Havin the constraints in listing \ref{lst:addExampleCons} as an input \unify{} changes the constraint
|
|
$\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}} \lessdot \tv{v}$
|
|
to $\tv{v} \doteq \wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$
|
|
therby finding a type solution for $\tv{v}$.
|
|
Afterwards every occurence of $\tv{v}$ in the constraint set is replaced by $\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$
|
|
leaving us with the following constraints which are now subject to a capture conversion by the \unify{} algorithm:
|
|
% Initially, no type is assigned to $\tv{v}$.
|
|
% % During the course of \unify{} more and more types emerge.
|
|
% As soon as a concrete type for $\tv{v}$ is appears during constraint
|
|
% solving, \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 \texttt{Y}, which is stored in the wildcard environment of the \unify{} algorithm.
|
|
Substituting \texttt{Y} for $\wtv{a}$ yields the constraints almost
|
|
solved: $\exptype{List}{\rwildcard{Y}} \lessdot
|
|
\exptype{List}{\rwildcard{Y}}$, $\type{String} \lessdot
|
|
\rwildcard{Y}$.
|
|
The first constraint is obviously satisfied and $\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 deduced from the solution of the \unify{} algorithm.% presented in Section~\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 capture converted wildcard $\wildcard{X}{\type{Object}}{\type{String}}$ can be used as
|
|
a type parameter of the 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{Notes on Capture Constraints}
|
|
Capture constraints must be stored in a multiset so that it is possible that two syntactically equal constraints remain in the same set.
|
|
The equality relation on Capture constraints is not reflexive.
|
|
|
|
Capture Constraints are bound to a variable.
|
|
For example a let statement like \lstinline{let x = v in x.get()} will create the capture constraint
|
|
$\tv{x} \lessdotCC_x \exptype{List}{\wtv{a}}$.
|
|
This time we annotated the capture constraint with an $x$ to show its relation to the variable \texttt{x}.
|
|
Let's do the same with the constraints generated by the \texttt{concat} method invocation in listing \ref{lst:faultyConcat},
|
|
creating the constraints \ref{lst:sameConstraints}.
|
|
|
|
\begin{figure}
|
|
\begin{minipage}[t]{0.49\textwidth}
|
|
\begin{lstlisting}[caption=Faulty Method Call,label=lst:faultyConcat,style=TamedFJ]{tamedfj}
|
|
List<?> v = ...;
|
|
|
|
let x = v in
|
|
let y = v in
|
|
concat(x, y) // Error!
|
|
\end{lstlisting}\end{minipage}
|
|
\hfill
|
|
\begin{minipage}[t]{0.49\textwidth}
|
|
\begin{lstlisting}[caption=Annotated constraints,mathescape=true,style=constraints,label=lst:sameConstraints]
|
|
$\tv{x} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{x}$
|
|
$\tv{y} \lessdotCC_\texttt{y} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{y}$
|
|
\end{lstlisting}
|
|
\end{minipage}
|
|
\end{figure}
|
|
|
|
|
|
During the \unify{} process it could happen that two syntactically equal capture constraints evolve,
|
|
but they are not the same because they are each linked to a different let introduced variable.
|
|
In this example this happens when we substitute $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\tv{x}$ and $\tv{y}$
|
|
resulting in:
|
|
%For example by substituting $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{x}]$ and $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{y}]$:
|
|
\begin{displaymath}
|
|
\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_x \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_y \exptype{List}{\wtv{a}}
|
|
\end{displaymath}
|
|
Thanks to the original annotations we can still see that those are different constraints.
|
|
After \unify{} uses the \rulename{Capture} rule on those constraints
|
|
it gets obvious that this constraint set is unsolvable:
|
|
\begin{displaymath}
|
|
\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}},
|
|
\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}
|
|
\end{displaymath}
|
|
|
|
%In this paper we do not annotate capture constraint with their source let statement.
|
|
This paper will not annotate capture constraints with variable names.
|
|
Instead we consider every capture constraint as distinct to other capture constraints even when syntactically the same,
|
|
because we know that each of them originates from a different let statement.
|
|
\textit{Hint:} An implementation of this algorithm has to consider that seemingly equal capture constraints are actually not the same
|
|
and has to allow doubles in the constraint set.
|
|
|
|
% %We see the equality relation on Capture constraints is not reflexive.
|
|
% A capture constraint is never equal to another capture constraint even when structurally the same
|
|
% ($\type{T} \lessdotCC \type{S} \neq \type{T} \lessdotCC \type{S}$).
|
|
% This is necessary to solve challenge \ref{challenge:1}.
|
|
% A capture constraint is bound to a specific let statement.
|
|
|
|
\textit{Note:}
|
|
In the special case \lstinline{let x = v in concat(x,x)} the constraints would look like
|
|
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}},
|
|
\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
|
|
and we could actually delete one of them without loosing information.
|
|
But this case will never occur in our algorithm, because the let
|
|
statements for our input programs are generated by transformation to ANF (see \ref{sec:anfTransformation}).
|
|
|
|
|
|
\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 Generic Java without wildcards
|
|
has been considered elsewher \cite{TIforFGJ}.
|
|
Adding wildcards to the calculus created new problems, which have not
|
|
been recognized by existing work on type unification for Java with wildcards~\cite{plue09_1}.
|
|
% what is the problem?
|
|
% Java does invisible capture conversion steps
|
|
Java's wildcard types are represented as existential types that have to be opened before they can be used.
|
|
Opening can either be done implicitly
|
|
(\cite{aModelForJavaWithWildcards}, \cite{javaTIisBroken}) or
|
|
explicitly via a let statement (\cite{WildcardsNeedWitnessProtection}).
|
|
For all variations it is vital to know the argument types with which a method is called.
|
|
In the absence of type annotations,
|
|
we do not know where an existential type will emerge and where a capture conversion is necessary.
|
|
Rather, the type inference algorithm has to figure out the placement
|
|
of existentials.
|
|
We identified 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 programs like the one shown in Listing~\ref{lst:addExample}
|
|
and rejects programs like the one 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}.
|
|
Because we know 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.
|
|
The element types of the lists may be unrelated, therefore the call to \texttt{concat} cannot succeed.
|
|
The problem gets apparent if we try to write the \texttt{concat}
|
|
method call in the \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{} transforms a constraint set into a correct type solution by
|
|
% 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 an arbitrary 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
|
|
% This problem is solved by assuming everything is a wildcard and lateron erasing excessive wildcards
|
|
% this is solved by having wildcards bound to a type. But this makes it necessary to remove wildcards lateron otherwise Unify would have to backtrack
|
|
The program in Listing~\ref{shuffleExample} exhibits a challenge involving wildcards and subtyping.
|
|
The method call \texttt{shuffle(l)} is incorrect, because \texttt{l} has type
|
|
$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ representing a list of unknown lists.
|
|
However, $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ is a subtype of
|
|
$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ which represents a list of lists, all of the same type $\rwildcard{X}$,
|
|
and can be passed safely to \texttt{shuffle}.
|
|
This behavior can also be explained by looking at the types and their capture converted versions:
|
|
\begin{center}
|
|
\begin{tabular}{l | l | l}
|
|
Java type & \TamedFJ{} representation & Capture Conversion \\
|
|
\hline
|
|
$\exptype{List}{\exptype{List}{\texttt{?}}}$ & $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ & $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ \\
|
|
$\exptype{List2D}{\texttt{?}}$ & $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ & $\exptype{List2D}{\rwildcard{X}}$ \\
|
|
%Supertype of $\exptype{List2D}{\texttt{?}}$ & $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ & $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ \\
|
|
\end{tabular}
|
|
\end{center}
|
|
%The direct supertype of $\exptype{List2D}{\rwildcard{X}}$ is $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
|
|
%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}
|
|
|
|
Given such a program the type inference algorithm has to allow the call \texttt{shuffle(l2d)} and
|
|
decline the call to \texttt{shuffle(l)}.
|
|
|
|
% 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 leave their scope}:
|
|
% Let's assume we have a variable \texttt{ls} with type $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$
|
|
% %When calling the \texttt{id} function with an element of this list we have to apply capture conversion.
|
|
% and the following program:
|
|
|
|
% \noindent
|
|
% \begin{minipage}{0.62\textwidth}
|
|
% \begin{lstlisting}
|
|
% let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = ls.get(0) in id(x) : (*@$\ntv{z}$@*)
|
|
% \end{lstlisting}\end{minipage}
|
|
% \hfill
|
|
% \begin{minipage}{0.36\textwidth}
|
|
% \begin{lstlisting}[style=constraints]
|
|
% (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$@*),
|
|
% (*@$\exptype{List}{\wtv{x}} \lessdot \ntv{z},$@*)
|
|
% \end{lstlisting}
|
|
% \end{minipage}
|
|
% % the variable z must not contain free variables (TODO)
|
|
|
|
Take the Java program in listing \ref{lst:mapExample} for example.
|
|
It uses map to apply a polymorphic method \texttt{id} to every element of a list
|
|
$\expr{l} :
|
|
\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$.
|
|
|
|
How do we get the \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 like in Listing~\ref{lst:mapExampleCons}.
|
|
|
|
\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 \TamedFJ{}:
|
|
|
|
\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 restriction has to be communicated 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}}}$, which would be 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 issue by distinguishing between wildcard placeholders
|
|
% and normal placeholders and introducing them as needed.
|
|
% $\ntv{z}$ is a normal placeholder and is not allowed to contain free variables.
|
|
\end{enumerate}
|