386 lines
17 KiB
TeX
386 lines
17 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}
|
|
|
|
|
|
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}{\il{T}} && \text{class type (with type variables)} \\
|
|
% Constraints
|
|
\simpleCons &::= \type{T} \lessdot \type{U} && \text{subtype constraint}\\
|
|
\orCons{} &::= \set{\set{\overline{\simpleCons_1}}, \ldots, \set{\overline{\simpleCons_n}}} && \text{or-constraint}\\
|
|
\constraint &::= \simpleCons \mid \orCons && \text{constraint}\\
|
|
\consSet &::= \set{\constraints} && \text{constraint set}\\
|
|
% Method assumptions:
|
|
\methodAssumption &::= \exptype{C}{\ol{X} \triangleleft \ol{N}}.\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}; \, K \, \overline{M} \}}) =\\
|
|
& \begin{array}{ll@{}l}
|
|
\textbf{let} & \forall \texttt{m} \in \ol{M}: \tv{a}_\texttt{m}, \ol{\tv{a}_m} \ \text{fresh} \\
|
|
& \ol{\methodAssumption} = \begin{array}[t]{l}
|
|
\set{ \mv{m'} : (\exptype{C}{\ol{X} \triangleleft \ol{N}} \to \ol{\tv{a}} \to \tv{a}) \mid
|
|
\mv{m'} \in \ol{M} \setminus \set{\mv{m}}, \, \tv{a}\, \ol{\tv{a}}\ \text{fresh} } \\
|
|
\ \cup \, \set{\mv{m} : (\exptype{C}{\ol{X} \triangleleft \ol{N}} \to \ol{\tv{a}_m} \to \tv{a}_\mv{m})}
|
|
\end{array}
|
|
\\
|
|
& C_m = \typeExpr(\mtypeEnvironment \cup \set{\mv{this} :
|
|
\exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}_m} }, \texttt{e}, \tv{a}_\texttt{m}) \\
|
|
\textbf{in}
|
|
& { ( \mtypeEnvironment \cup \ol{\methodAssumption}, \,
|
|
\bigcup_{\texttt{m} \in \ol{M}} C_m )
|
|
}
|
|
\end{array}
|
|
\end{array}
|
|
\end{gather*}
|
|
\caption{Constraint generation for classes}
|
|
\label{fig:constraints-for-classes}
|
|
\end{figure}
|
|
|
|
% \textbf{Method Assumptions}
|
|
|
|
% %$\Pi$ is a set of method assumptions used by the $\fjtype{}$ algorithm.
|
|
|
|
% % \begin{verbatim}
|
|
% % class Example<X> {
|
|
% % <Y> Y m(Example<Y> p){ ... }
|
|
% % }
|
|
% % \end{verbatim}
|
|
|
|
% In Featherweight Java a method type is bound to a specific class.
|
|
% The class \texttt{Example} shown above contains one method \texttt{m}:
|
|
|
|
% \begin{displaymath}
|
|
% \textit{mtype}({\texttt{m}, \exptype{Example}{\type{X}}}) = \generics{\type{Y}} \ \exptype{Example}{\type{Y}} \to \type{Y}
|
|
% \end{displaymath}
|
|
|
|
% $\Pi$ is a set of method assumptions used by the $\fjtype{}$ algorithm.
|
|
% It's a map of method types to method names.
|
|
% Every method name has a set of possible types,
|
|
% because there could be more than one method with the same name in a program consisting out of multiple classes.
|
|
% To simplify the syntax of method assumptions, we add the inheriting class type to the parameter list:
|
|
|
|
% \begin{displaymath}
|
|
% \Pi = \set{ \texttt{m} : \generics{\type{X}, \type{Y}} \ (\exptype{Example}{\type{X}}, \exptype{Example}{\type{Y}}) \to \type{Y}}
|
|
% \end{displaymath}
|
|
|
|
% \begin{verbatim}
|
|
% class Example<X> { }
|
|
|
|
% <X, Y> Y m(Example<X> this, Example<Y> p){ ... }
|
|
% \end{verbatim}
|
|
|
|
\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}
|
|
|
|
The set of method assumptions returned by the \textit{mtypes} function is used to generate the constraints for a method call expression:
|
|
|
|
There are two kinds of method calls.
|
|
The ones to already typed methods and calls to untyped methods.
|
|
|
|
\begin{displaymath}
|
|
\begin{array}{@{}l@{}l}
|
|
\typeExpr{} & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a} ) = \\
|
|
& \begin{array}{ll}
|
|
\textbf{let}
|
|
& \tv{r}, \ol{\tv{r}} \text{ fresh} \\
|
|
& \consSet_R = \typeExpr(({\mtypeEnvironment} ;
|
|
\overline{\localVarAssumption}), \texttt{e}, \tv{r})\\
|
|
& \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \ol{e}, \ol{\tv{r}}) \\
|
|
& \begin{array}{@{}l@{}l}
|
|
\constraint = \orCons\set{ &
|
|
\begin{array}[t]{l}
|
|
[\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdot \exptype{C}{\ol{X}},
|
|
\overline{\tv{r}} \lessdot \ol{T},
|
|
\type{T} \lessdot \tv{a},
|
|
\ol{X} \lessdot \ol{N},
|
|
\ol{Y} \lessdot \ol{N'} \}
|
|
\end{array}\\
|
|
& \ |\
|
|
(\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N'}}\overline{\type{T}} \to \type{T}) \in
|
|
{\mtypeEnvironment}
|
|
, \, \overline{\wtv{a}} \text{ fresh}, \, \overline{\wtv{b}} \text{ fresh} }
|
|
\end{array}\\
|
|
\mathbf{in} & \consSet_R \cup \overline{\consSet} \cup \constraint
|
|
\end{array}
|
|
\end{array}
|
|
\end{displaymath}
|
|
\\[1em]
|
|
\noindent
|
|
\textbf{Example:}
|
|
\begin{verbatim}
|
|
class Class1{
|
|
<X> X m(List<X> lx, List<? extends X> lt){ ... }
|
|
List<? extends String> wGet(){ ... }
|
|
List<String> get() { ... }
|
|
}
|
|
|
|
class Class2{
|
|
example(c1){
|
|
return c1.m(c1.get(), c1.wGet());
|
|
}
|
|
}
|
|
\end{verbatim}
|
|
%This example comes with predefined type annotations.
|
|
We assume the class \texttt{Class1} has already been processed by our type inference algorithm,
|
|
which has lead to the given type annotations for \texttt{Class1}.
|
|
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}
|
|
\type{Class1}.\texttt{m}: \generics{\type{X} \triangleleft \type{Object}} \
|
|
(\exptype{List}{\type{X}}, \, \wctype{\wildcard{A}{\type{X}}{\bot}}{List}{\wildcard{A}{\type{X}}{\bot}}) \to \type{X}, \\
|
|
\type{Class1}.\texttt{wGet}: () \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\wildcard{A}{\type{Object}}{\type{String}}}, \\
|
|
\type{Class1}.\texttt{get}: () \to \exptype{List}{\type{String}}
|
|
\end{array} \right\}
|
|
\end{displaymath}
|
|
|
|
The result of the $\typeExpr{}$ function is the constraint set
|
|
\begin{displaymath}
|
|
C = \left\{ \begin{array}{l}
|
|
\tv{c1} \lessdot \type{Class1}, \\
|
|
\tv{p1} \lessdot \exptype{List}{\wtv{x}}, \\
|
|
\exptype{List}{\type{String}} \lessdot \tv{p1}, \\
|
|
\tv{p2} \lessdot \wctype{\wildcard{A}{\wtv{x}}{\bot}}{List}{\rwildcard{A}}, \\
|
|
\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{p2}
|
|
\end{array} \right\}
|
|
\end{displaymath}
|
|
|
|
|
|
The first parameter of a method assumption is the receiver type $\type{T}_r$.
|
|
\texttt{Class1} for this example.
|
|
Therefore the $(\tv{c1} \lessdot \type{Class1})$ constraint.
|
|
The type variable $\tv{c1}$ is assigned to the parameter \texttt{c1} of the \texttt{example} method.
|
|
|
|
or a simplified version:
|
|
|
|
\begin{displaymath}
|
|
C = \left\{ \begin{array}{l}
|
|
\tv{c1} \lessdot \type{Class1}, \\
|
|
\exptype{List}{\type{String}}
|
|
\lessdot \exptype{List}{\wtv{x}}, \\
|
|
\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}
|
|
\lessdot \wctype{\wildcard{A}{\wtv{x}}{\bot}}{List}{\rwildcard{A}}
|
|
\end{array} \right\}
|
|
\end{displaymath}
|
|
|
|
|
|
$\wtv{x}$ is a type variable we use for the generic $\type{X}$. It is flagged as a free type variable.
|
|
%TODO: Do an example where wildcards are inserted and we need capture conversion
|
|
|
|
\unify{} returns the solution $(\sigma = \set{ \tv{x} \to \type{String} })$
|
|
|
|
% \\[1em]
|
|
% \noindent
|
|
% \textbf{Example:}
|
|
% \begin{verbatim}
|
|
% class Class1 {
|
|
% <X> Pair<X, X> make(List<X> l){ ... }
|
|
% <Y> boolean compare(Pair<Y,Y> p) { ... }
|
|
|
|
% example(l){
|
|
% return compare(make(l));
|
|
% }
|
|
% }
|
|
% \end{verbatim}
|
|
|
|
% The method call \texttt{make(l)} generates the constraints
|
|
% \begin{displaymath}
|
|
% \tv{l} \lessdot \exptype{List}{\tv{x}}, \exptype{Pair}{\tv{x}, \tv{x}} \lessdot \tv{m}
|
|
% \end{displaymath}
|
|
% with $\tv{l}$ being the type placeholder for the variable \texttt{l}
|
|
% and $\tv{m}$ is the type variable for the return type of the method call.
|
|
% $\tv{m}$ is then used as the parameter for the \texttt{compare} method:
|
|
% \begin{displaymath}
|
|
% \tv{m} \lessdot \exptype{Pair}{\tv{y}, \tv{y}}
|
|
% \end{displaymath}
|
|
% Note the conversion of the generic parameters \texttt{X} and \texttt{Y} to type variables $\tv{x}$ and $\tv{y}$.
|
|
|
|
|
|
|
|
% Step 3 of the \unify{} algorithm has to look for every possible supertype of $\exptype{Pair}{\tv{x}, \tv{x}}$,
|
|
% when processing the $\exptype{Pair}{\tv{x}, \tv{x}} \lessdot \tv{m}$ constraint.
|
|
|
|
\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} |