Ecoop2024_TIforWildFJ/constraints.tex
Andreas Stadelmeier 813b256e4d Intro to type rules
2024-02-10 08:19:24 +01:00

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}