Ecoop2024_TIforWildFJ/constraints.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}

Constraint generation step is the same as in \cite{TIforFGJ} except for field access and method invocation.
Here \fjtype{} generates capture constraints instead of normal subtype constraints.

Subtype constraints are created according to the type rules defined in section \ref{sec:tifj}.
The \typeExpr{} function creates constraints for a given expression.

$\begin{array}{c}
\typeExpr(\texttt{t}_1, \ntv{b}) = C_l \quad \quad \typeExpr(\texttt{t}_2, \ntv{c}) = C_l \quad \quad \ntv{b}, \ntv{c} \ \text{fresh}
\\
\hline
\typeExpr(\texttt{t}_1 \texttt{?:} \texttt{t}_2, \tv{a}) = C_l \cup C_r \cup \set{\ntv{b} \lessdot \tv{a}, \ntv{c} \lessdot \tv{a}}
\end{array}
$

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.

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}{\il{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}; \, 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{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2) = \\
                & \begin{array}{ll}
                    \textbf{let} 
                    & \tv{e}, \tv{x} \ \text{fresh} \\
                    & \consSet_R = \typeExpr({\mtypeEnvironment}, \expr{e}_1, \tv{e})\\
                    & \constraint =
                      \set{
                      \tv{e} \lessdot \tv{x} 
                      }\\
                    {\mathbf{in}} & {
                    \consSet_R \cup \set{\constraint}} \cup \typeExpr(\mtypeEnvironment \cup \set{\expr{x} : \tv{x}})
                  \end{array} 
  \end{array}
\end{displaymath}

\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} , \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} , \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} \lessdotCC \exptype{C}{\ol{X}},
                    \overline{\tv{r}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a}, 
                    \ol{Y} \lessdot \ol{N} \}
                  \end{array}\\
            & \ |\ 
            (\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T}) \in 
                {\mtypeEnvironment} %, \, |\ol{T}| = |\ol{e}|
            , \, \overline{\wtv{a}} \text{ fresh}}
        \end{array}\\
      \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T})
      \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}