616 lines
29 KiB
TeX
616 lines
29 KiB
TeX
|
|
\section{Constraint generation}\label{chapter:constraintGeneration}
|
|
% Method names are not unique.
|
|
% It is possible to define the same method in multiple classes.
|
|
% The \TYPE{} algorithm accounts for that by generating Or-Constraints.
|
|
% This can lead to multiple possible solutions.
|
|
|
|
%\subsection{Well-Formedness}
|
|
|
|
|
|
% But it can be easily adapted to Featherweight Java or Java.
|
|
% We add T <. a for every return of an expression anyway. If anything returns a Generic like X it is not directly used in a method call like X <c T
|
|
|
|
The constraint generation works on the \TamedFJ{} language.
|
|
This step is mostly the same as in \cite{TIforFGJ} except for field access and method invocation.
|
|
We will focus on those two parts where also the new capture constraints and wildcard type placeholders are introduced.
|
|
|
|
%In \TamedFJ{} capture conversion is implicit.
|
|
%To emulate Java's behaviour we assume the input program not to contain any let statements.
|
|
%They will be added by an ANF transformation (see chapter \ref{sec:anfTransformation}).
|
|
|
|
Before generating constraints the input is transformed by an ANF transformation (see section \ref{sec:anfTransformation}).
|
|
|
|
%Constraints are generated on the basis of the program in A-Normal form.
|
|
%After adding the missing type annotations the resulting program is valid under the typing rules in \cite{WildFJ}.
|
|
|
|
%This is shown in chapter \ref{sec:soundness}
|
|
|
|
%\section{\TamedFJ{}: Syntax and Typing}\label{sec:tifj}
|
|
|
|
% The syntax forces every expression to undergo a capture conversion before it can be used as a method argument.
|
|
% Even variables have to be catched by a let statement first.
|
|
% This behaviour emulates Java's implicit capture conversion.
|
|
|
|
\subsection{ANF transformation}\label{sec:anfTransformation}
|
|
\newcommand{\anf}[1]{\ensuremath{\tau}(#1)}
|
|
%https://en.wikipedia.org/wiki/A-normal_form)
|
|
Featherweight Java's syntax involves no \texttt{let} statement
|
|
and terms can be nested freely similar to Java's syntax.
|
|
Our calculus \TamedFJ{} uses let statements to explicitly apply capture conversion to wildcard types,
|
|
but we don't know which expressions will spawn wildcard types because there are no type annotations yet.
|
|
To emulate Java's behaviour we have to preemptively add capture conversion in every suitable place.
|
|
%To convert it to \TamedFJ{} additional let statements have to be added.
|
|
This is done by a \textit{A-Normal Form} \cite{aNormalForm} transformation shown in figure \ref{fig:anfTransformation}.
|
|
After this transformation every method invocation is preceded by let statements which perform capture conversion on every argument before passing them to the method.
|
|
See the example in listings \ref{lst:anfinput} and \ref{lst:anfoutput}.
|
|
\begin{figure}
|
|
\begin{minipage}{0.45\textwidth}
|
|
\begin{lstlisting}[style=fgj,caption=\TamedFJ{} example,label=lst:anfinput]
|
|
m(l, v){
|
|
return l.add(v);
|
|
}
|
|
\end{lstlisting}
|
|
\end{minipage}%
|
|
\hfill
|
|
\begin{minipage}{0.5\textwidth}
|
|
\begin{lstlisting}[style=tfgj,caption=A-Normal form,label=lst:anfoutput]
|
|
m(l, v) =
|
|
let x1 = l in
|
|
let x2 = v in x1.add(x2)
|
|
\end{lstlisting}
|
|
\end{minipage}
|
|
\end{figure}
|
|
|
|
\begin{figure}
|
|
\begin{center}
|
|
$\begin{array}{lrcl}
|
|
%\text{ANF}
|
|
& \anf{\expr{x}} & = & \expr{x} \\
|
|
& \anf{\texttt{new} \ \type{C}(\overline{t})} & = & \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}}) \\
|
|
& \anf{t.f} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \expr{x}.f \\
|
|
& \anf{t.\texttt{m}(\overline{t})} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \expr{x}.\texttt{m}(\overline{\expr{x}}) \\
|
|
& \anf{t_1 \elvis{} t_2} & = & \anf{t_1} \elvis{} \anf{t_2} \\
|
|
& \anf{\texttt{let}\ x = \expr{t}_1 \ \texttt{in}\ \expr{t}_2} & = & \texttt{let}\ x = \anf{\expr{t}_1} \ \texttt{in}\ \anf{\expr{t}_2}
|
|
\end{array}$
|
|
\end{center}
|
|
\caption{ANF Transformation $\tau$}\label{fig:anfTransformation}
|
|
\end{figure}
|
|
|
|
\begin{figure}
|
|
\center
|
|
$
|
|
\begin{array}{lrcl}
|
|
%\hline
|
|
\text{Terms} & t & ::= & \expr{x} \\
|
|
& & \ \ | & \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}_c}) \\
|
|
& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \expr{x}_c.f \\
|
|
& & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \expr{x}_c.\texttt{m}(\overline{\expr{x}_c}) \\
|
|
& & \ \ | & t \elvis{} t \\
|
|
%\hline
|
|
\end{array}
|
|
$
|
|
\caption{Syntax of a \TamedFJ{} program in A-Normal Form}\label{fig:anf-syntax}
|
|
\end{figure}
|
|
|
|
\subsection{Constraint Generation Algorithm}
|
|
% Generally subtype constraints for an expression mirror the subtype relations in the premise of the respective type rule introduced in section \ref{sec:tifj}.
|
|
% Unknown types at the time of the constraint generation step are replaced with type placeholders.
|
|
|
|
% The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
|
|
% Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
|
|
|
|
The parameter types given to a generic method also affect their return type.
|
|
During constraint generation the algorithm does not know the parameter types yet.
|
|
We generate $\lessdotCC$ constraints and let \unify{} do the capture conversion.
|
|
$\lessdotCC$ constraints are kept until they reach the form $\type{G} \lessdotCC \type{G}$ and a capture conversion is possible.
|
|
% TODO: Challenge examples!
|
|
|
|
At points where a well-formed type is needed we use a normal type placeholder.
|
|
Inside a method call expression sub expressions (receiver, parameter) wildcard placeholders are used.
|
|
Here captured variables can flow freely.
|
|
A normal type placeholder cannot hold types containing free variables.
|
|
Normal type placeholders are assigned types which are also expressible with Java syntax.
|
|
So no types like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ or $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
|
|
|
|
It is possible to feed the \unify{} algorithm a set of free variables with predefined bounds.
|
|
This is used for class generics see figure \ref{fig:constraints-for-classes}.
|
|
The \fjtype{} function returns a set of constraints aswell as an initial environment $\Delta$
|
|
containing the generics declared by this class.
|
|
Those type variables count as regular types and can be held by normal type placeholders.
|
|
|
|
%Why do we need a constraint generation step?
|
|
%% The problem is NP-Hard
|
|
%% a method call, does not know which type it will produce
|
|
%% depending on its type the
|
|
|
|
%NO equals constraints during the constraint generation step!
|
|
\begin{figure}[tp]
|
|
\center
|
|
\begin{tabular}{lcll}
|
|
$C $ &$::=$ &$\overline{c}$ & Constraint set \\
|
|
$c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \lessdotCC \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
|
|
$\type{T}, \type{U}, \type{L} $ & $::=$ & $\tv{a} \mid \gtype{G}$ & Type placeholder or Type \\
|
|
$\tv{a}$ & $::=$ & $\ntv{a} \mid \wtv{a}$ & Normal and wildcard type placeholder \\
|
|
$\gtype{G}$ & $::=$ & $\type{X} \mid \ntype{N}$ & Wildcard, or Class Type \\
|
|
$\ntype{N}, \ntype{S}$ & $::=$ & $\wctype{\triangle}{C}{\ol{T}} $ & Class Type \\
|
|
$\triangle$ & $::=$ & $\overline{\wtype{W}}$ & Wildcard Environment \\
|
|
$\wtype{W}$ & $::=$ & $\wildcard{X}{U}{L}$ & Wildcard \\
|
|
\end{tabular}
|
|
\caption{Syntax of types and constraints used by \fjtype{} and \unify{}}
|
|
\label{fig:syntax-constraints}
|
|
\end{figure}
|
|
|
|
\begin{figure}[tp]
|
|
\begin{gather*}
|
|
\begin{array}{@{}l@{}l}
|
|
\fjtype & ({\mtypeEnvironment }, \mathtt{class } \ \exptype{C}{\overline{\type{X} \triangleleft \type{N}}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\
|
|
& \begin{array}{ll@{}l}
|
|
\textbf{let} & \ol{\methodAssumption} =
|
|
\set{ \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \mid
|
|
\set{ \mv{m}(\ol{x}) = \expr{e} } \in \ol{M}, \, \tv{a}, \ol{\tv{a}}\ \text{fresh} } \\
|
|
& \Delta = \set{ \overline{\wildcard{X}{\type{N}}{\bot}} } \\
|
|
& C = \begin{array}[t]{l}
|
|
\set{ \typeExpr(\mtypeEnvironment \cup \ol{\methodAssumption} \cup \set{\mv{this} :
|
|
\exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}} }, \texttt{e}, \tv{a})
|
|
\\ \quad \quad \quad \quad \mid \set{ \mv{m}(\ol{x}) = \expr{e} } \in \ol{M},\, \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \in \ol{\methodAssumption}}
|
|
\end{array} \\
|
|
\textbf{in}
|
|
& (\Delta, C)
|
|
\end{array}
|
|
\end{array}
|
|
\end{gather*}
|
|
\caption{Constraint generation for classes}
|
|
\label{fig:constraints-for-classes}
|
|
\end{figure}
|
|
|
|
\begin{displaymath}
|
|
\begin{array}{@{}l@{}l}
|
|
\typeExpr{} &({\mtypeEnvironment}, \Gamma , \texttt{e}.\texttt{f}, \tv{a}) = \\
|
|
& \begin{array}{ll}
|
|
\textbf{let}
|
|
& \tv{r} \ \text{fresh} \\
|
|
& \consSet_R = \typeExpr({\mtypeEnvironment}, \Gamma, \texttt{e}, \tv{r})\\
|
|
& \constraint = \begin{array}[t]{@{}l@{}l}
|
|
\orCons\set{
|
|
\set{ &
|
|
\tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}} ,
|
|
\tv{a} \doteq [\overline{\wtv{a}}/\ol{X}]\type{T},
|
|
\ol{\wtv{a}} \lessdot [\overline{\wtv{a}}/\ol{X}]\ol{N}
|
|
} \\
|
|
& \quad \mid \mv{T}\ \mv{f} \in \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}
|
|
, \, \overline{\wtv{a}} \text{ fresh}
|
|
}\end{array}\\
|
|
{\mathbf{in}} & {
|
|
\consSet_R \cup \set{\constraint}}
|
|
\end{array}
|
|
\end{array}
|
|
\end{displaymath}
|
|
|
|
\begin{displaymath}
|
|
\begin{array}{@{}l@{}l}
|
|
\typeExpr{} &({\mtypeEnvironment}, \Gamma , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2, \tv{a}) = \\
|
|
& \begin{array}{ll}
|
|
\textbf{let}
|
|
& \tv{e}_1, \tv{e}_2, \tv{x} \ \text{fresh} \\
|
|
& \consSet_1 = \typeExpr({\mtypeEnvironment}, \Gamma, \expr{e}_1, \tv{e}_1)\\
|
|
& \consSet_2 = \typeExpr({\mtypeEnvironment } \cup \set{\expr{x} : \tv{x}}, \expr{e}_2, \tv{e}_2)\\
|
|
& \constraint =
|
|
\set{
|
|
\tv{e}_1 \lessdot \tv{x}, \tv{e}_2 \lessdot \tv{a}
|
|
}\\
|
|
{\mathbf{in}} & {
|
|
\consSet_1 \cup \consSet_2 \cup \set{\constraint}}
|
|
\end{array}
|
|
\end{array}
|
|
\end{displaymath}
|
|
|
|
\begin{displaymath}
|
|
\begin{array}{@{}l@{}l}
|
|
\typeExpr{} & ({\mtypeEnvironment}, \Gamma , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\
|
|
& \begin{array}{ll}
|
|
\textbf{let}
|
|
& \tv{r}, \ol{\tv{r}} \text{ fresh} \\
|
|
& \constraint = [\overline{\wtv{b}}/\ol{Y}]\set{
|
|
\ol{S} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a},
|
|
\ol{Y} \lessdot \ol{N} }\\
|
|
\mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T}) \\
|
|
& \mathbf{where}\ \begin{array}[t]{l}
|
|
\expr{v}, \ol{v} : \ol{S} \in \localVarAssumption \\
|
|
\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T} \in {\mtypeEnvironment }
|
|
\end{array}
|
|
|
|
\end{array}
|
|
\end{array}
|
|
\end{displaymath}
|
|
|
|
\begin{displaymath}
|
|
\begin{array}{@{}l@{}l}
|
|
\typeExpr{} &({\mtypeEnvironment}, \Gamma , e_1 \elvis{} e_2, \tv{a}) = \\
|
|
& \begin{array}{ll}
|
|
\textbf{let}
|
|
& \tv{r}_1, \tv{r}_2 \ \text{fresh} \\
|
|
& \consSet_1 = \typeExpr({\mtypeEnvironment}, \Gamma, e_1, \tv{r}_2)\\
|
|
& \consSet_2 = \typeExpr({\mtypeEnvironment}, \Gamma, e_2, \tv{r}_2)\\
|
|
{\mathbf{in}} & {
|
|
\consSet_1 \cup \consSet_2 \cup
|
|
\set{\tv{r}_1 \lessdot \tv{a}, \tv{r}_2 \lessdot \tv{a}}}
|
|
\end{array}
|
|
\end{array}
|
|
\end{displaymath}
|
|
|
|
%We could skip wfresh here:
|
|
\begin{displaymath}
|
|
\begin{array}{@{}l@{}l}
|
|
\typeExpr{} &({\mtypeEnvironment}, \Gamma , x, \tv{a}) =
|
|
\mtypeEnvironment(x)
|
|
\end{array}
|
|
\end{displaymath}
|
|
|
|
\begin{displaymath}
|
|
\begin{array}{@{}l@{}l}
|
|
\typeExpr{} &({\mtypeEnvironment}, \Gamma , \texttt{new}\ \type{C}(\overline{e}), \tv{a}) = \\
|
|
& \begin{array}{ll}
|
|
\textbf{let}
|
|
& \ol{\ntv{r}}, \ol{\ntv{a}} \ \text{fresh} \\
|
|
& \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \Gamma, \overline{e}, \ol{\ntv{r}}) \\
|
|
& C = \set{\ol{\ntv{r}} \lessdot [\ol{\ntv{a}}/\ol{X}]\ol{T}, \ol{\ntv{a}} \lessdot \ol{N} \mid \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}} \\
|
|
{\mathbf{in}} & {
|
|
\overline{\consSet} \cup
|
|
\set{\tv{a} \doteq \exptype{C}{\ol{\ntv{a}}}}}
|
|
\end{array}
|
|
\end{array}
|
|
\end{displaymath}
|
|
\\[1em]
|
|
\noindent
|
|
\begin{example}
|
|
Given the following input program missing type annotations for the \texttt{example} method:
|
|
\begin{lstlisting}[style=java]
|
|
class Class1{
|
|
<A> A head(List<X> l){ ... }
|
|
List<? extends String> get() { ... }
|
|
}
|
|
|
|
class Class2{
|
|
example(c1){
|
|
return c1.head(c1.get());
|
|
}
|
|
}
|
|
\end{lstlisting}
|
|
%This example comes with predefined type annotations.
|
|
We assume the class \texttt{Class1} has already been processed by our type inference algorithm
|
|
leading to the following type annotations:
|
|
%Now we call the $\fjtype{}$ function with the class \texttt{Class2} and the method assumptions for the preceeding class:
|
|
\begin{displaymath}
|
|
\mtypeEnvironment = \left\{\begin{array}{l}
|
|
\texttt{m}: \generics{\type{A} \triangleleft \type{Object}} \
|
|
(\type{Class1},\, \exptype{List}{\type{A}}) \to \type{X}, \\
|
|
\texttt{get}: (\type{Class1}) \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\rwildcard{A}}
|
|
\end{array} \right\}
|
|
\end{displaymath}
|
|
|
|
At first we have to convert the example method to a syntactically correct \TamedFJ{} program.
|
|
Afterwards the the \fjtype{} algorithm is able to generate constraints.
|
|
|
|
\noindent
|
|
\begin{minipage}{0.52\textwidth}
|
|
\begin{lstlisting}[style=tamedfj]
|
|
class Class2 {
|
|
example(c1) = let x = c1 in
|
|
let xp = x.get() in x.m(xp);
|
|
}
|
|
\end{lstlisting}
|
|
\end{minipage}%
|
|
\hfill
|
|
\begin{minipage}{0.46\textwidth}
|
|
\begin{lstlisting}[style=constraints]
|
|
(*@$\ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}$@*),
|
|
(*@$\ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}$@*),
|
|
(*@$\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{xp}$@*),
|
|
(*@$\tv{xp} \lessdotCC \exptype{List}{\wtv{a}}$@*)
|
|
\end{lstlisting}
|
|
\end{minipage}
|
|
|
|
Following is a possible solution for the given constraint set:
|
|
|
|
\noindent
|
|
\begin{minipage}{0.55\textwidth}
|
|
\begin{lstlisting}[style=tamedfj]
|
|
class Class2 {
|
|
example(c1) = let x :Class1 = c1 in
|
|
let xp :(*@$\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*) = x.get()
|
|
in x.m(xp);
|
|
}
|
|
\end{lstlisting}
|
|
\end{minipage}%
|
|
\hfill
|
|
\begin{minipage}{0.43\textwidth}
|
|
\begin{lstlisting}[style=constraints]
|
|
(*@$\sigma(\ntv{x}) = \type{Class1}$@*),
|
|
(*@$\sigma(\tv{xp}) = \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*)
|
|
\end{lstlisting}
|
|
\end{minipage}
|
|
|
|
For $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$ to be a correct solution for $\tv{xp}$
|
|
the constraint $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{a}}$
|
|
must be satisfied.
|
|
This is possible, because we deal with a capture constraint.
|
|
The $\lessdotCC$ constraint allows the left side to undergo a capture conversion
|
|
which leads to $\exptype{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{a}}$.
|
|
Now a substitution of the wildcard placeholder $\wtv{a}$ with $\rwildcard{A}$ leads to a satisfied constraint set.
|
|
\end{example}
|
|
|
|
The wildcard placeholders are not used as parameter or return types of methods.
|
|
Or as types for variables introduced by let statements.
|
|
They are only used for generic method parameters during a method invocation.
|
|
Type placeholders which are not flagged as wildcard placeholders ($\wtv{a}$) can never hold a free variable or a type containing free variables.
|
|
This practice hinders free variables to leave their scope.
|
|
The free variable $\rwildcard{A}$ generated by the capture conversion on the type $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$
|
|
cannot be used anywhere else then inside the constraints generated by the method call \texttt{x.m(xp)}.
|
|
|
|
\subsection{Constraint Generation}
|
|
The constraint generation is defined on a subset of Java displayed in figure \ref{fig:miniJavaSyntax}.
|
|
The input language includes only a small set of expressions like method calls, field access and a elvis operator $\elvis$
|
|
which acts as a replacement for if-else expressions.
|
|
\begin{figure}
|
|
\par\noindent\rule{\textwidth}{0.4pt}
|
|
\center
|
|
$
|
|
\begin{array}{lrcl}
|
|
%\hline
|
|
\text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
|
|
\text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
|
|
\text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
|
|
\text{Type variable contexts} & \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
|
|
\text{Class declarations} & D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\
|
|
\text{Method declarations} & \texttt{M} & ::= & \highlight{\generics{\overline{\type{X} \triangleleft \type{N}}}}\ \highlight{\type{T}}\ \texttt{m}(\overline{\highlight{\type{T}}\ \expr{x}}) \{ \texttt{return} \ \expr{e}; \} \\
|
|
\text{Terms} & \expr{e} & ::= & \expr{x} \\
|
|
& & \ \ | & \texttt{new} \ \type{C}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
|
|
& & \ \ | & \expr{e}.f\\
|
|
& & \ \ | & \expr{e}.\texttt{m}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
|
|
& & \ \ | & \expr{e} \elvis{} \expr{e}\\
|
|
\text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
|
|
\text{Method type environment} & \mathrm{\Pi} & ::= & \overline{ \texttt{m} : \generics{\ol{X \triangleleft N}}\ \ol{T} \to \type{T}}
|
|
%\hline
|
|
\end{array}
|
|
$
|
|
\par\noindent\rule{\textwidth}{0.4pt}
|
|
\caption{Input Syntax with optional type annotations}\label{fig:miniJavaSyntax}
|
|
\end{figure}
|
|
|
|
We explain the process using the following example input.
|
|
The classes \texttt{List} and \texttt{Id} are already fully typed and we want to create constraints for the class
|
|
\texttt{CExample} now.
|
|
|
|
\begin{lstlisting}{java}
|
|
class Id{
|
|
<X> X id(X x){ return x; }
|
|
}
|
|
|
|
class List<X> {
|
|
<Y extends X> List<X> concat(List<Y> l){ ... }
|
|
}
|
|
|
|
class CExample{
|
|
example(p1, p2) {
|
|
return p1.id(p2).concat(p2);
|
|
}
|
|
}
|
|
\end{lstlisting}
|
|
|
|
The first step of constraint generation is to assign type placeholders to every expression in the input program.
|
|
Type placeholders also fill in for missing type annotations in method headers.
|
|
|
|
\begin{lstlisting}{java}
|
|
class CExample{
|
|
example(p1, p2) {
|
|
return p1.id(p2).concat(p2);
|
|
}
|
|
}
|
|
\end{lstlisting}
|
|
\begin{lstlisting}{java}
|
|
class CExample{
|
|
(*@$\tv{a}$@*) example((*@$\tv{b}$@*) p1, (*@$\tv{c}$@*) p2) {
|
|
return ((p1:(*@$\tv{b}$@*)).id(p2:(*@$\tv{c}$@*)):(*@$\tv{d}$@*)).concat(p2:(*@$\tv{c}$@*)) : (*@$\tv{e}$@*);
|
|
}
|
|
}
|
|
\end{lstlisting}
|
|
|
|
The placeholders $\tv{a}-\tv{e}$ are freshly created in this example and added to every expression.
|
|
The type of local variable expressions like \expr{p1} and \expr{p2} is already known and can be assigned directly.
|
|
$\expr{p1}:\tv{b}$ and $\expr{p2}:\tv{c}$ in this case.
|
|
The method call to \texttt{id} gets the fresh type placeholder $\tv{d}$ as type and the method call to \texttt{concat} is assigned the placeholder $\tv{e}$.
|
|
|
|
Afterwards we create a method type environment $\mtypeEnvironment$ containing all method declarations.
|
|
Each entry has the form $\texttt{m} : \generics{\ol{X \triangleleft N}} \ol{T} \to \type{T}$.
|
|
The type arguments of the surrounding class and the type arguments of each method are merged together
|
|
leading to the list $\generics{\type{X}, \type{Y} \triangleleft \type{X}}$ for the \texttt{concat} method
|
|
($\triangleleft$ is short for \texttt{extends}).
|
|
Also the type of the surrounding class is added to the parameter list of the method.
|
|
This leads to the \texttt{id} method having two arguments.
|
|
One is the \texttt{Id} class itself and the second one is the actual arguemnt of the method.
|
|
|
|
$\mtypeEnvironment{} = \left\{ \begin{array}{l}
|
|
\texttt{id} : \generics{\type{X}}\type{Id},\type{X} \to \type{X}, \\
|
|
\texttt{concat} : \generics{\type{X}, \type{Y} \triangleleft \type{X}}\exptype{List}{\type{X}},\exptype{List}{\type{Y}} \to \exptype{List}{\type{X}}, \\
|
|
\texttt{example} : \type{CExample},\tv{b},\tv{c} \to \tv{a}, \\
|
|
\end{array} \right\}
|
|
$
|
|
|
|
Note: type placeholders are used for the \texttt{example} method.
|
|
|
|
Our constraint generation rules have the form:
|
|
$\mtypeEnvironment \vdash \expr{e} : \tv{a} \implies C$,
|
|
that given a method environment $\mtypeEnvironment$ and an expression $\expr{e}$ with type $\tv{a}$ generates the constraint set $C$.
|
|
|
|
%Inference-rule in the style of: https://dl.acm.org/doi/pdf/10.1145/345099.345100
|
|
\begin{mathpar}
|
|
\inferrule[Method-Cons]{
|
|
\mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C \\
|
|
\overline{\mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C} \\
|
|
\texttt{m} : \generics{\ol{Y \triangleleft N}}\type{T}_r, \overline{\type{T}} \to \type{T} \in { \mtypeEnvironment }\\
|
|
\overline{\wtv{b}}, \tv{x}, \overline{\tv{x}} \ \text{fresh} \\
|
|
C_m = \set{\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}}} \cup
|
|
[\overline{\wtv{b}}/\ol{Y}]\set{ \tv{x} \lessdotCC \type{T}_r, \overline{\tv{x} \lessdotCC \type{T}}, \type{T} \lessdot \tv{a}, \overline{Y \lessdot N} }
|
|
}{
|
|
\mtypeEnvironment \vdash \expr{e}.\texttt{m}(\overline{\expr{e}}) : \tv{a} \implies C \cup \overline{C} \cup C_m
|
|
}
|
|
\and
|
|
% \inferrule[Field-Cons]{
|
|
% \mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C \\
|
|
% C_f = \set{}
|
|
% }{
|
|
% \mtypeEnvironment \vdash \expr{e}.\texttt{f} : \tv{a} \implies C \cup C_f \\
|
|
% }
|
|
% \and
|
|
\inferrule[Var-Cons]{
|
|
}{
|
|
\mtypeEnvironment \vdash \expr{x} : \tv{a} \implies \emptyset
|
|
}
|
|
\and
|
|
\inferrule[Elvis-Cons]{
|
|
\mtypeEnvironment \vdash \expr{e}_1 : \tv{e}_1 \implies C_1 \\
|
|
\mtypeEnvironment \vdash \expr{e}_2 : \tv{e}_2 \implies C_2
|
|
}{
|
|
\mtypeEnvironment \vdash \expr{e}_1 \elvis{} \expr{e}_2 : \tv{a} \implies C_1 \cup C_2 \cup \set{\tv{e}_1 \lessdot \tv{a}, \tv{e}_2 \lessdot \tv{a}}
|
|
}
|
|
\and
|
|
\inferrule[New-Cons]{
|
|
\overline{\mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C} \\
|
|
\texttt{class} \ \exptype{D}{\ol{X \triangleleft N}} \set{ \ol{T\ f}; \ldots }
|
|
}{
|
|
\mtypeEnvironment \vdash \texttt{new}\ \type{D}(\ol{e}) : \tv{a} \implies \overline{C} \cup [\ol{\wtv{b}}/\ol{X}]\set{ \overline{\tv{e} \lessdot \type{T}}, \exptype{D}{\ol{X}} \lessdot \tv{a}, \ol{X \lessdot N} }
|
|
}
|
|
\end{mathpar}
|
|
|
|
According to the Method-Cons rule the constraints generated by the call to \texttt{id} are:
|
|
$\mtypeEnvironment \vdash (p1:\tv{b}).id(p2:\tv{c}):\tv{d} \implies \set{\tv{b} \lessdot \tv{x}_1, \tv{c} \lessdot \tv{x}_2, \tv{x}_1 \lessdotCC \type{Id},
|
|
\tv{x}_2 \lessdotCC \wtv{b}, \wtv{b} \lessdot \tv{d}}$.
|
|
|
|
\subsection{Or-Constraints}
|
|
In case the input program contains multiple method declarations holding the same name and same amount of parameters then so called Or-Constraints must be generated.
|
|
Usually Java is able to determine which method to call based on the argument's types passed to the method. %'
|
|
During the constraint generation step the argument types are unknown and we have to assume multiple methods as invocation target.
|
|
|
|
\begin{lstlisting}
|
|
class String{
|
|
bool equals(String s){ .. }
|
|
}
|
|
class Int{
|
|
bool equals(Int i){ .. }
|
|
}
|
|
class OrConsExample{
|
|
m(a, b){
|
|
return a.equals(b);
|
|
}
|
|
}
|
|
\end{lstlisting}
|
|
|
|
The method call to \texttt{equals} now has multiple possibilities.
|
|
It could either be a call to the method in the class \texttt{Int} or in \texttt{String}.
|
|
The method type environment therfore contains two versions of the \texttt{equals} method:
|
|
|
|
$\mtypeEnvironment{} = \set{ \texttt{equals}_1 : \type{String}, \type{String} \to \type{bool},
|
|
\texttt{equals}_2 : \type{Int}, \type{Int} \to \type{bool}}$
|
|
|
|
The Or-Cons rule considers multiple declarations of the same method separately and joins all of them into a Or-Constraint.
|
|
|
|
\begin{mathpar}
|
|
\inferrule[Or-Cons]{
|
|
\texttt{m}_1 \ldots \texttt{m}_n \in \text{dom}(\mtypeEnvironment{}) \\
|
|
\mtypeEnvironment \vdash \expr{e}.\texttt{m}_1(\overline{\expr{e}}) : \tv{a} \implies C_1 \quad
|
|
\ldots \quad
|
|
\mtypeEnvironment \vdash \expr{e}.\texttt{m}_n(\overline{\expr{e}}) : \tv{a} \implies C_n
|
|
}{
|
|
\mtypeEnvironment \vdash \expr{e}.\texttt{m}(\overline{\expr{e}}) : \tv{a} \implies \orCons{}(C_1, \ldots, C_n)
|
|
}
|
|
\end{mathpar}
|
|
|
|
% Problem:
|
|
% <X, A extends List<X>> void t2(List<A> l){}
|
|
|
|
% void test(List<List<?>> l){
|
|
% t2(l);
|
|
% }
|
|
% Problem:
|
|
% List<Y.List<Y>> <. List<a>, a <. List<x>
|
|
% Y.List<Y> =. a
|
|
% Z.List<Z> <. List<x>
|
|
|
|
% These constraints should fail!
|
|
|
|
% \section{Result Generation}
|
|
% If \unify{} returns atleast one type solution $(\Delta, \sigma)$
|
|
% the last step of the type inference algorithm is to generate a typed class.
|
|
|
|
% This section presents our type inference algorithm.
|
|
% The algorithm is given method assumptions $\mv\Pi$ and applied to a
|
|
% single class $\mv L$ at a time:
|
|
% \begin{gather*}
|
|
% \fjtypeinference(\mtypeEnvironment, \texttt{class}\ \exptype{C}{\ol{X}
|
|
% \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \\
|
|
% \quad \quad \begin{array}[t]{rll}
|
|
% \textbf{let}\
|
|
% (\overline{\methodAssumption}, \consSet) &= \fjtype{}(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X}
|
|
% \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \ldots \}) &
|
|
% \text{// constraint generation}\\
|
|
% {(\Delta, \sigma)} &= \unify{}(\consSet,\, \ol{X} <: \ol{N}) & \text{// constraint solving}\\
|
|
% \generics{\ol{Y} \triangleleft \ol{S}} &= \set{ \type{Y} \triangleleft \type{S} \mid \wildcard{Y}{\type{P}}{\bot} \in \Delta} \\
|
|
% \ol{M'} &= \set{ \generics{\ol{Y} \triangleleft \ol{S}}\ \sigma(\tv{a}) \ \texttt{m}(\ol{\sigma(\tv{a})\ x}) = \texttt{e} \mid (\mathtt{m}(\ol{x})\ = \mv e) \in \ol{M}, (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
|
|
% %TODO: Describe whole algorithm (Insert types, try out every unify solution by backtracking (describe it as Non Deterministic algorithm))
|
|
% \end{array}\\
|
|
% \textbf{in}\ \texttt{class}\ \exptype{C}{\ol{X}
|
|
% \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M'} \} \\
|
|
% \textbf{in}\ \mtypeEnvironment \cup
|
|
% \set{(\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \generics{\ol{Y} \triangleleft \ol{S}}\ \ol{\sigma(\tv{a})} \to \sigma(\tv{a})) \ |\ (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
|
|
% % \fjtypeInsert(\overline{\methodAssumption}, (\sigma, \unifyGenerics{}) )
|
|
% \end{gather*}
|
|
|
|
% The overall algorithm is nondeterministic. The function $\unify{}$ may
|
|
% return finitely many times as there may be multiple solutions for a constraint
|
|
% set. A local solution for class $\mv C$ may not
|
|
% be compatible with the constraints generated for a subsequent class. In this case, we have to backtrack to $\mv C$ and proceed to the next
|
|
% local solution; if thats fail we have to backtrack further to an earlier class.
|
|
|
|
% \begin{gather*}
|
|
% \textbf{ApplyTypes}(\mtypeEnvironment, \texttt{class}\ \exptype{C}{\ol{X}
|
|
% \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \\
|
|
% \quad \quad \begin{array}[t]{rl}
|
|
% \textbf{let}\
|
|
% \ol{M'} &= \set{ \generics{\ol{Y} \triangleleft \ol{S}}\ \sigma(\tv{a}) \ \texttt{m}(\ol{\sigma(\tv{a})\ x}) = \texttt{e} \mid (\mathtt{m}(\ol{x})\ = \mv e) \in \ol{M}, (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\mv{m} : \ol{\tv{a}} \to \tv{a}) \in \overline{\methodAssumption}}
|
|
% \end{array}\\
|
|
% \textbf{in}\ \texttt{class}\ \exptype{C}{\ol{X}
|
|
% \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M'} \} \\
|
|
% \end{gather*}
|
|
|
|
% %TODO: Rules to create let statements
|
|
% % Input is type solution and untyped program.
|
|
% % Output is typed program
|
|
% % describe conversion for each expression
|
|
|
|
% Given a result $(\Delta, \sigma)$ and the type placeholders generated by $\TYPE{}$
|
|
% we can construct a \wildFJ{} program.
|
|
|
|
% %TODO: show soundness by comparing constraints and type rules
|
|
% % untyped expression | constraints | typed expression (making use of constraints and sigma)
|
|
% $\begin{array}{l|c|r}
|
|
% m(x) = e & r m(p x) = e & \Delta \sigma(r) m(\sigma(p) x) = |e| \\
|
|
% e \elvis{} e' \\
|
|
% e.m(\ol{e}) & (e:a).m(\ol{e:p}) & a <. T, p <. T & let x : sigma(a) = e in e.m(x); %TODO
|
|
% \end{array}$
|
|
% \begin{displaymath}
|
|
% \begin{array}[c]{l}
|
|
% \\
|
|
% \hline
|
|
% \vspace*{-0.4cm}\\
|
|
% \wildcardEnv
|
|
% \vdash C \cup \, \set{
|
|
% \ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
|
|
% \ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} }
|
|
% \end{array}
|
|
% \end{displaymath}
|
|
%%% Local Variables:
|
|
%%% mode: latex
|
|
%%% TeX-master: "TIforWildFJ"
|
|
%%% End:
|