Ecoop2024_TIforWildFJ/tRules.tex

\section{\TamedFJ{}}\label{sec:tifj}
%LetFJ -> Output language!
%TamedFJ -> ANF transformed input langauge
%Input language only described here. It is standard Featherweight Java
% we use the transformation to proof soundness. this could also be moved to the end. 
% the constraint generation step assumes every method argument to be encapsulated in a let statement. This is the way Java is doing capture conversion
This section defines the calculus \TamedFJ{}, which is used as input and output of our global type inference algorithm.
%We assume that the input to our algorithm is a program, which carries none of the optional type annotations.
%After calculating a type solution we can insert all missing types and generate a correct program.
%The input to our algorithm is a typeless version of Featherweight Java.
Figure~\ref{fig:syntax} contains the syntax with optional type annotations highlighted in yellow.
The respective typing rules are defined in Figures~\ref{fig:expressionTyping} and~\ref{fig:typing}.
\TamedFJ{} is a subset of the calculus defined by Bierhoff
\cite{WildcardsNeedWitnessProtection}, but in addition we make the types for
method arguments and return types optional. 
The point is that a correct and fully typed \TamedFJ{} program is also a correct Featherweight Java program,
which is vital for our soundness proof (chapter \ref{sec:soundness}).
%The language is designed to showcase type inference involving existential types.

A method assumption consists of a method name, a list of type variables, a list of argument types, and a return type.
The first type in the list of argument types is the type of the surrounding class also known as the \texttt{this} parameter.
See Figure~\ref{fig:methodTypeExample} for an example, where the
\texttt{add} method is treated internally as a method with two
arguments, because we add \texttt{this} to its argument list.
The type variable $\type{A}$ of the surrounding class is part of the
method's list of type parameters.
%For example the \texttt{add} method in listing \ref{lst:tamedfjSample} is represented by the assumption
%$\texttt{add} : \generics{\ol{X \triangleleft Object}}\ \type{X} \to \exptype{List}{\type{X}}$.
\begin{figure}
\center
\begin{minipage}{0.49\textwidth}
    %[style=java,caption=\TamedFJ{} sample, label=lst:tamedfjSample]
\begin{lstlisting}
class List<A extends Object> {
    List<A> add(A v){..,}
}
\end{lstlisting}
\end{minipage}
\begin{minipage}{0.49\textwidth}
\begin{align*}
&\mathrm{\Pi} = \set{\\
&\texttt{add} : \generics{\ol{A \triangleleft Object}}\ \exptype{List}{\type{A}},\type{A} \to \exptype{List}{\type{X}} \\
&}
\end{align*}
\end{minipage}
% \begin{minipage}{0.49\textwidth}
% \begin{lstlisting}[style=java,caption=\TamedFJ{} sample, label=lst:tamedfjSample]
% class List<A extends Object> {}
% <A extends Object> List<A>
%     add(List<A> this, A v){..,}
% \end{lstlisting}
% \end{minipage}
\caption{\TamedFJ{} class and its corresponding method type environment}\label{fig:methodTypeExample}
\end{figure}

\textit{Additional Notes:}%
\begin{itemize}
%\item Method parameters and return types are optional.
\item We require type annotations for fields and generic class parameters,
  as we consider them as data declarations which are given by the programmer.
% They are inferred in for example \cite{plue14_3b}
\item We add the elvis operator ($\elvis{}$) to the syntax to easily showcase applications involving wildcard types.
\item The \texttt{new} expression does not require generic parameters.
\item Every method has an unique name.
The calculus does not include method overriding for simplicity.
Type inference with method overriding is described elsewhere
\cite{TIforFGJ} and can be added to our algorithm in a similar way.
\item The \textsc{T-Program} typing rule ensures that there is one set of method assumptions used for all classes
that are part of the program.
\item Unlike previous work \cite{TIforFGJ},  the typing rules for expressions shown in
  Figure~\ref{fig:expressionTyping} allow for polymorphic recursion.
  Type inference for polymorphic recursion is undecidable
  \cite{wells1999typability} and when proving completeness the calculus needs to be restricted in that regard (cf.\
  \cite{TIforFGJ}).
  Our algorithm is not complete (see discussion in section
  \ref{sec:completeness}), so we keep the \TamedFJ{} calculus as simple as possible
  and close to Featherweight Java to simplify the soundness proof. 
\end{itemize}

%Additional features like overriding methods and method overloading can be added by copying the respective parts from there.
%Additional features can be easily added by generating the respective constraints (Plümicke hier zitieren)

% The type system in \cite{WildcardsNeedWitnessProtection} allows a method to \textit{override} an existing method declaration in one of its super classes,
% but only by a method with the exact same type.
% The type system presented here does not allow the \textit{overriding} of methods.
% Our type inference algorithm consumes the input classes in succession and could only do a type check instead of type inference
% on overriding methods, because their type is already determined.
% Allowing overriding therefore has no implication on our type inference algorithm.

% The output is a valid Featherweight Java program.
% We use the syntax of the version introduced in \cite{WildcardsNeedWitnessProtection}
% calling it \letfj{} for that it is a Featherweight Java variant including \texttt{let} statements.

\newcommand{\highlight}[1]{\begingroup\fboxsep=0pt\colorbox{yellow}{$\displaystyle #1$}\endgroup}
\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}})\\
& & \ \ | & \texttt{let}\ \expr{x} \highlight{: \wcNtype{\Delta}{N}} = \expr{e} \ \texttt{in} \ \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:syntax}
\end{figure}

\begin{figure}[tp]
\begin{center}
$\begin{array}{l}
    \typerule{S-Refl}\\
    \begin{array}{@{}c}
        \Delta \vdash \type{T} <: \type{T}
    \end{array}
 \end{array}$
 \qquad
$\begin{array}{l}
    \typerule{S-Trans}\\
    \begin{array}{@{}c}
        \Delta \vdash \type{S} <: \type{T} \quad \quad
        \Delta \vdash \type{T} <: \type{U}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta \vdash \type{S} <: \type{U}
    \end{array}
 \end{array}$
 \qquad
$\begin{array}{l}
    \typerule{S-Upper}\\
    \begin{array}{@{}c}
        \wildcard{X}{U}{L} \in \Delta \\
    \vspace*{-0.9em}\\
        \hline
    \vspace*{-0.9em}\\
        \Delta \vdash \type{X} <: \type{U}
    \end{array}
 \end{array}$
 \qquad
$\begin{array}{l}
    \typerule{S-Lower}\\
    \begin{array}{@{}c}
        \wildcard{X}{U}{L} \in \Delta \\
    \vspace*{-0.9em}\\
        \hline
    \vspace*{-0.9em}\\
        \Delta \vdash \type{L} <: \type{X}
    \end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
    \typerule{S-Extends}\\
    \begin{array}{@{}c}
        \texttt{class}\ \exptype{C}{\overline{\type{X} \triangleleft \type{U}}} \triangleleft \type{N} \ \{ \ldots \} \\
        \ol{X} \cap \text{dom}(\Delta) = \emptyset
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta \vdash \wctype{\Delta'}{C}{\ol{T}} <: \wcNtype{\Delta'}{[\ol{T}/\ol{X}]\type{N}}
    \end{array}
 \end{array}$
 \quad
$\begin{array}{l}
    \typerule{S-Exists}\\
    \begin{array}{@{}c}
        \Delta', \Delta \vdash [\ol{T}/\ol{\type{X}}]\ol{L} <: \ol{T} \quad \quad
        \Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\
        \text{fv}(\ol{T}) \subseteq \text{dom}(\Delta, \Delta') \quad
        \text{dom}(\Delta') \cap \text{fv}(\wcNtype{\ol{\wildcard{X}{U}{L}}}{N}) = \emptyset
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta \vdash \wcNtype{\Delta'}{[\ol{T}/\ol{X}]\type{N}} <:
        \wcNtype{\ol{\wildcard{X}{U}{L}}}{N}
    \end{array}
\end{array}$
\end{center}
\caption{Subtyping}\label{fig:subtyping}
\end{figure}

\begin{figure}[tp]
\begin{center}
$\begin{array}{l}
    \typerule{WF-Bot}\\
    \begin{array}{@{}c}
        \Delta \vdash \bot \ \ok
    \end{array}
\end{array}$
\qquad
$\begin{array}{l}
    \typerule{WF-Top}\\
    \begin{array}{@{}c}
        \Delta \vdash \ol{L}, \ol{U} \ \ok
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta \vdash \overline{\wildcard{W}{U}{L}}.\texttt{Object}
    \end{array}
\end{array}$
\qquad
$\begin{array}{l}
    \typerule{WF-Var}\\
    \begin{array}{@{}c}
        \wildcard{W}{U}{L} \in \Delta \quad \quad 
        \Delta \vdash \ol{L}, \ol{U} \ \ok
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta \vdash \wildcard{W}{U}{L} \ \ok
    \end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
    \typerule{WF-Class}\\
    \begin{array}{@{}c}
        \Delta' = \ol{\wildcard{W}{U}{L}} \quad \quad
        \Delta, \Delta' \vdash \ol{T}, \ol{L}, \ol{U} \ \ok \quad \quad
        \Delta, \Delta' \vdash \ol{L} <: \ol{U} \\
        \Delta, \Delta' \vdash \ol{T} <: [\ol{T}/\ol{X}] \ol{U'} \quad \quad 
        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U'}} \triangleleft \type{N} \ \{ \ldots \}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta \vdash \wctype{\ol{\wildcard{W}{U}{L}}}{C}{\ol{T}} \ \ok
    \end{array}
\end{array}$
\end{center}
\caption{Well-formedness}\label{fig:well-formedness}
\end{figure}

\begin{figure}[tp]
\begin{center}
$\begin{array}{l}
    \typerule{T-Var}\\
    \begin{array}{@{}c}
        \texttt{x} : \type{T} \in \Gamma
        \\
        \hline
    \vspace*{-0.3cm}\\
        \triangle | \Gamma \vdash \texttt{x} : \type{T}
    \end{array}
\end{array}$ \hfill
$\begin{array}{l}
    \typerule{T-Field}\\
    \begin{array}{@{}c}
        \Delta | \Gamma \vdash \expr{v} : \type{T} \quad \quad 
        \Delta \vdash \type{T} <: \wcNtype{}{N} \quad \quad
        \textit{fields}(\type{N}) = \ol{U\ f} \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta | \Gamma \vdash \expr{v}.\texttt{f}_i : \type{U}_i
    \end{array}
\end{array}$
\\[1em]
% $\begin{array}{l}
%     \typerule{T-Field}\\
%     \begin{array}{@{}c}
%         \Delta | \Gamma \vdash \texttt{e} : \type{T} \quad \quad 
%         \Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
%         \textit{fields}(\type{N}) = \ol{U\ f} \\
% \Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
% \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
% \Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
%         \\
%         \hline
%     \vspace*{-0.3cm}\\
%         \Delta | \Gamma \vdash \texttt{e}.\texttt{f}_i : \type{S}
%     \end{array}
% \end{array}$
% \\[1em]
% $\begin{array}{l}
%     \typerule{T-New}\\
%     \begin{array}{@{}c}
%         \Delta, \overline{\Delta} \vdash  \exptype{C}{\ol{T}} \ \ok \quad \quad
%         \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
%         \Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
%         \Delta \vdash  \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
%         \Delta, \overline{\Delta} \vdash  \overline{\type{N}} <: \overline{\type{U}} \quad \quad
%         \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
%         \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
%         \Delta \vdash \type{T},  \overline{\wcNtype{\Delta}{N}} \ \ok
%         \\
%         \hline
%     \vspace*{-0.3cm}\\
%         \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}}
%     \end{array}
% \end{array}$
% \\[1em] 
$\begin{array}{l}
    \typerule{T-New}\\
    \begin{array}{@{}c}
        \Delta, \overline{\Delta} \vdash  \exptype{C}{\ol{T}} \ \ok \quad \quad
        \Delta \vdash  \overline{\type{S}} <: \overline{\type{U}} \\
        \Delta | \Gamma \vdash \overline{\expr{v} : \type{S}} \quad \quad
        \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} 
        \\
        \hline
    \vspace*{-0.3cm}\\
        \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{v}) : \exptype{C}{\ol{T}}
    \end{array}
\end{array}$
\hfill
% $\begin{array}{l}
%     \typerule{T-Call}\\
%     \begin{array}{@{}c}
%         \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
%         \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
%         \\
%         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
%         \Delta | \Gamma \vdash  \texttt{e}, \ol{e} : \ol{T} \quad \quad
%         \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
%         \\
%         \Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
%         \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
%         \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
%         \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
%         \\
%         \hline
%     \vspace*{-0.3cm}\\
%         \Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T}
%     \end{array}
% \end{array}$
% \\[1em]
$\begin{array}{l}
    \typerule{T-Call}\\
    \begin{array}{@{}c}
        \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
        \Delta \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
        \\
        \Delta \vdash \ol{S} \ \ok \quad \quad
        \Delta | \Gamma \vdash  \expr{v}, \ol{v} : \ol{T} \quad \quad
        \Delta \vdash \ol{T} <: [\ol{S}/\ol{X}]\ol{U} 
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta | \Gamma \vdash \expr{v}.\texttt{m}(\ol{v}) : \type{T}
    \end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
    \typerule{T-Let}\\
    \begin{array}{@{}c}
        \Delta | \Gamma \vdash \expr{t}_1 : \type{T}_1 \quad \quad
        \Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}
        \\
        \Delta, \Delta' | \Gamma, \expr{x} : \wcNtype{}{N} \vdash \expr{t}_2 : \type{T}_2 \quad \quad
        \Delta, \Delta' \vdash  \type{T}_2 <: \type{T} \quad \quad
        \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta | \Gamma \vdash \texttt{let}\ \expr{x} = \expr{t}_1 \ \texttt{in} \ \expr{t}_2 : \type{T}
    \end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
    \typerule{T-Elvis}\\
    \begin{array}{@{}c}
        \triangle | \Gamma \vdash \texttt{t}_1 : \type{S} \quad \quad
        \triangle | \Gamma \vdash \texttt{t}_2 : \type{T} \quad \quad
        \triangle \vdash \type{S} <: \type{U} \quad \quad
        \triangle \vdash \type{T} <: \type{U} \quad \quad
        \\
        \hline
    \vspace*{-0.3cm}\\
        \triangle | \Gamma \vdash \texttt{t}_1 \ \texttt{?:} \ \texttt{t}_2 : \type{U}
    \end{array}
\end{array}$
\end{center}
\caption{Expression Typing}\label{fig:expressionTyping}
\end{figure}

\begin{figure}
\begin{center}
$\begin{array}{l}
    \typerule{T-Method}\\
    \begin{array}{@{}c}
        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\ldots} \quad \quad 
        \generics{\ol{Y \triangleleft \type{N}}}(\exptype{C}{\ol{X}},\ol{T}) \to \type{T} \in \mathtt{\Pi}(\texttt{m}) \quad \quad
        \triangle' =  \overline{\type{Y} : \bot .. \type{P}} \\
        \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \quad \quad
        \text{dom}(\triangle) = \ol{X} \quad \quad
        %\texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \ \{ \ldots \} \\
        \mathtt{\Pi} | \triangle, \triangle' | \ol{x : T}, \texttt{this} : \exptype{C}{\ol{X}} \vdash \texttt{e} : \type{S} \quad \quad 
        \triangle \vdash \type{S} <: \type{T}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) \set{ \texttt{return}\ \texttt{e}; } \ \ok \ \text{in C}
    \end{array}
\end{array}$
\\[1em]
$\begin{array}{l}
    \typerule{T-Class}\\
    \begin{array}{@{}c}
        %\forall \texttt{m} \in \ol{M} : \mathtt{\Pi}(\texttt{m}) = \generics{\ol{X \triangleleft \type{N}}}(\exptype{C}{\ol{X}},\ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \\
        \triangle = \overline{\type{X} : \bot .. \type{U}} \quad \quad
        \triangle \vdash \ol{U}, \ol{T}, \type{N} \ \ok \quad \quad
        \mathtt{\Pi} | \triangle \vdash \ol{M} \ \ok \text{ in C}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \mathtt{\Pi} \vdash \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \} 
    \end{array}
\end{array}$
%\\[1em]
\hfill
$\begin{array}{l}
    \typerule{T-Program}\\
    \begin{array}{@{}c}
        \mathtt{\Pi} = \overline{\texttt{m} : \generics{\ol{X \triangleleft \type{N}}}\ol{T} \to \type{T}}
        \\
        \hline
    \vspace*{-0.3cm}\\
    \mathtt{\Pi} \vdash \overline{D}
    \end{array}
\end{array}$
\end{center}
\caption{Class and Method Typing rules}\label{fig:typing}
\end{figure}



\begin{figure}
    $\text{fields}(\exptype{Object}{}) = \emptyset$
    \quad \quad
    $\begin{array}{l}
    \typerule{F-Class}\\
    \begin{array}{@{}c}
        \texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \set{\ol{S\ f}; \ol{M}} \quad \quad 
        \text{fields}([\ol{T}/\ol{X}]\type{N}) = \ol{U\ g}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \text{fields}(\exptype{C}{\ol{T}}) = \ol{U\ g}, [\ol{T}/\ol{X}]\ol{S\ f}
    \end{array}
\end{array}$
\caption{Field access}
\end{figure}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "TIforWildFJ"
%%% End: