Fix TamedFJ introduction

This commit is contained in:
Andreas Stadelmeier 2024-05-27 23:22:38 +02:00
parent 49368e0d0e
commit 3dbdce8e29

View File

@ -5,33 +5,56 @@
%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
The input to our algorithm is a typeless version of Featherweight Java.
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 a subset of the calculus defined by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection}.
\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.
This calculus 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.
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 argument type is the type of the surrounding class or the \texttt{this} parameter one could say.
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{lstlisting}[style=java,caption=\TamedFJ{} sample, label=lst:tamedfjSample]
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}
TODO
\\[1em]
\noindent
\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 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.
@ -85,6 +108,7 @@ $
& & \ \ | & \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}
$