386 lines
18 KiB
TeX
386 lines
18 KiB
TeX
\section{Constraint generation}\label{chapter:constraintGeneration}
|
|
% Our type inference algorithm is split into two parts.
|
|
% A constraint generation step \textbf{TYPE} and a \unify{} step.
|
|
|
|
% 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 same as in \cite{TIforFGJ} except for field access and method invocation.
|
|
We will focus on those parts.
|
|
Here the new capture constraints and wildcard type placeholders are introduced.
|
|
|
|
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.
|
|
\begin{verbatim}
|
|
m(l, v){
|
|
let x = x in x.add(v)
|
|
}
|
|
\end{verbatim}
|
|
|
|
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.
|
|
|
|
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}}}$.
|
|
|
|
Type variables declared in the class header are passed to \unify{}.
|
|
Those type variables count as regular types and can be held by normal type placeholders.
|
|
|
|
|
|
There are two different types of constraints:
|
|
\begin{description}
|
|
\item[$\lessdot$] \textit{Example:}
|
|
|
|
$\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}$
|
|
|
|
\noindent
|
|
Those two constraints imply that we have to find a type replacement for type variable $\tv{a}$,
|
|
which is a supertype of $\exptype{List}{String}$ aswell as $\exptype{List}{Integer}$.
|
|
This paper describes a \unify{} algorithm to solve these constraints and calculate a type solution $\sigma$.
|
|
For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
|
|
\item[$\lessdotCC$] TODO
|
|
% The \fjtype{} algorithm assumes capture conversions for every method parameter.
|
|
\end{description}
|
|
|
|
%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]
|
|
\begin{align*}
|
|
% Type
|
|
\type{T}, \type{U} &::= \tv{a} \mid \wtv{a} \mid \mv{X} \mid {\wcNtype{\Delta}{N}} && \text{types and type placeholders}\\
|
|
\type{N} &::= \exptype{C}{\ol{T}} && \text{class type (with type variables)} \\
|
|
% Constraints
|
|
\constraint &::= \type{T} \lessdot \type{U} \mid \type{T} \lessdotCC \type{U} && \text{Constraint}\\
|
|
\consSet &::= \set{\constraints} && \text{constraint set}\\
|
|
% Method assumptions:
|
|
\methodAssumption &::= \texttt{m} : \exptype{}{\ol{Y}
|
|
\triangleleft \ol{P}}\ \ol{\type{T}} \to \type{T} &&
|
|
\text{method
|
|
type assumption}\\
|
|
\localVarAssumption &::= \texttt{x} : \itype{T} && \text{parameter
|
|
assumption}\\
|
|
\mtypeEnvironment & ::= \overline{\methodAssumption} &
|
|
& \text{method type environment} \\
|
|
\typeAssumptionsSymbol &::= ({\mtypeEnvironment} ; \overline{\localVarAssumption})
|
|
\end{align*}
|
|
\caption{Syntax of constraints and type assumptions}
|
|
\label{fig:syntax-constraints}
|
|
\end{figure}
|
|
|
|
\begin{figure}[tp]
|
|
\begin{gather*}
|
|
\begin{array}{@{}l@{}l}
|
|
\fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\ol{X} \triangleleft \ol{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} } \\
|
|
\textbf{in}
|
|
& \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}
|
|
\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} , \texttt{e}.\texttt{f}, \tv{a}) = \\
|
|
& \begin{array}{ll}
|
|
\textbf{let}
|
|
& \tv{r} \ \text{fresh} \\
|
|
& \consSet_R = \typeExpr({\mtypeEnvironment}, \texttt{e}, \tv{r})\\
|
|
& \constraint = \begin{array}[t]{@{}l@{}l}
|
|
\orCons\set{
|
|
\set{ &
|
|
\tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}} ,
|
|
[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} ,
|
|
\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} , \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}, \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} , \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}
|
|
\\[1em]
|
|
\noindent
|
|
\textbf{Example:}
|
|
\begin{verbatim}
|
|
class Class1{
|
|
<A> A head(List<X> l){ ... }
|
|
List<? extends String> get() { ... }
|
|
}
|
|
|
|
class Class2{
|
|
example(c1){
|
|
return c1.head(c1.get());
|
|
}
|
|
}
|
|
\end{verbatim}
|
|
%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.
|
|
|
|
\begin{minipage}{0.45\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.5\textwidth}
|
|
\begin{constraintset}
|
|
$
|
|
\begin{array}{l}
|
|
\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{array}
|
|
$
|
|
\end{constraintset}
|
|
\end{minipage}
|
|
|
|
Following is a possible solution for the given constraint set:
|
|
|
|
\begin{minipage}{0.55\textwidth}
|
|
\begin{lstlisting}[style=letfj]
|
|
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.4\textwidth}
|
|
\begin{constraintset}
|
|
$
|
|
\begin{array}{l}
|
|
\sigma(\ntv{x}) = \type{Class1} \\
|
|
%\tv{xp} \lessdot \exptype{List}{\wtv{x}}, \\
|
|
%\exptype{List}{\type{String}} \lessdot \tv{p1}, \\
|
|
\sigma(\tv{xp}) = \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \\
|
|
\end{array}
|
|
$
|
|
\end{constraintset}
|
|
\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.
|
|
|
|
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)}.
|
|
|
|
\begin{displaymath}
|
|
\begin{array}{@{}l@{}l}
|
|
\typeExpr{} &({\mtypeEnvironment} , e_1 \elvis{} e_2, \tv{a}) = \\
|
|
& \begin{array}{ll}
|
|
\textbf{let}
|
|
& \tv{r}_1, \tv{r}_2 \ \text{fresh} \\
|
|
& \consSet_1 = \typeExpr({\mtypeEnvironment}, e_1, \tv{r}_2)\\
|
|
& \consSet_2 = \typeExpr({\mtypeEnvironment}, 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} , x, \tv{a}) =
|
|
\mtypeEnvironment(x)
|
|
\end{array}
|
|
\end{displaymath}
|
|
|
|
\begin{displaymath}
|
|
\begin{array}{@{}l@{}l}
|
|
\typeExpr{} &({\mtypeEnvironment} , \texttt{new}\ \type{C}(\overline{e}), \tv{a}) = \\
|
|
& \begin{array}{ll}
|
|
\textbf{let}
|
|
& \ol{\tv{r}} \ \text{fresh} \\
|
|
& \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \overline{e}, \ol{\tv{r}}) \\
|
|
& C = \set{\ol{\tv{r}} \lessdot [\ol{\tv{a}}/\ol{X}]\ol{T}, \ol{\tv{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{a}}}}
|
|
\end{array}
|
|
\end{array}
|
|
\end{displaymath}
|
|
|
|
% 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} |