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
We define our own calculus \TamedFJ{}, which is used as input aswell as output to 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.
The syntax is shown in figure \ref{fig:syntax} with optional type annotations highlighted in yellow.
The respective type rules are defined by figure \ref{fig:expressionTyping} and \ref{fig:typing}.
\TamedFJ{} is practically a subset of the Featherweight Java calculus defined by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection}
with the exception that method argument and return type annotations are 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 (see chapter \ref{sec:soundness}).
%The language is designed to showcase type inference involving existential types.

A method assumption consists out of a method name, a list of type parameters, 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:
Here the \texttt{add} method internally is treated as a method with two arguments,
because we add \texttt{this} to its argument list.
Note that the type parameter $\type{A}$ of the surrounding class is part of the methods parameter list.
%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 still require type annotations for fields and generic class parameters.
This is a design choice by us,
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 mainly to showcase applications involving wildcard types.
\item \textit{Note:} The \texttt{new} expression is not requiring generic parameters.
\item Every method has an unique name.
The calculus does not include method overriding for simplicity reasons.
Type inference for that is described in \cite{TIforFGJ} and can be added to this algorithm accordingly.
\item The \textsc{T-Program} type rule ensures that there is one set of method assumptions used for all classes
that are part of the program.
\item The typing rules for expressions shown in figure \ref{fig:expressionTyping} refrain from restricting polymorphic recursion.
Type inference for polymorphic recursion is undecidable \cite{wells1999typability} and when proving completeness like in \cite{TIforFGJ} the calculus
needs to be restricted in that regard.
Our algorithm is not complete (see discussion in chapter \ref{sec:completeness}) and without the respective proof we can keep the \TamedFJ{} calculus as simple as possible
and as close to it's Featherweight Java correspondent as possible,
simplifying 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}$
$\begin{array}{l}
    \typerule{S-Trans}\\
    \begin{array}{@{}c}
        \Delta \vdash \type{S} <: \type{T}' \quad \quad
        \Delta \vdash \type{T}' <: \type{T}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta \vdash \type{S} <: \type{T}
    \end{array}
\end{array}$
$\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}$
$\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}$
$\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}$
$\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}$
$\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} : \type{T}_1 \quad \quad
        \triangle | \Gamma \vdash \texttt{t}_2 : \type{T}_2 \quad \quad
        \triangle \vdash \type{T}_1 <: \type{T} \quad \quad
        \triangle \vdash \type{T}_2 <: \type{T} \quad \quad
        \\
        \hline
    \vspace*{-0.3cm}\\
        \triangle | \Gamma \vdash \texttt{t}_1 \ \texttt{?:} \ \texttt{t}_2 : \type{T}
    \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}