Rephrase TamedFJ intro

This commit is contained in:
Andreas Stadelmeier 2024-05-27 18:22:17 +02:00
parent 42d8afce35
commit e5f577f577

View File

@ -7,36 +7,48 @@
% 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 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. The input to our algorithm is a typeless version of Featherweight Java.
The syntax is shown in figure \ref{fig:syntax} The syntax is shown in figure \ref{fig:syntax} with optional type annotations highlighted in yellow.
and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}. The respective type rules are defined by figure \ref{fig:expressionTyping} and \ref{fig:typing}.
Method parameters and return types are optional. \TamedFJ{} is a subset of the calculus defined by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection}.
We still require type annotations for fields and generic class parameters. 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]
class List<A extends Object> {
List<A> add(A v){..,}
}
\end{lstlisting}
TODO
\\[1em]
\noindent
\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, This is a design choice by us,
as we consider them as data declarations which are given by the programmer. as we consider them as data declarations which are given by the programmer.
% They are inferred in for example \cite{plue14_3b} % They are inferred in for example \cite{plue14_3b}
Note the \texttt{new} expression not requiring generic parameters, \item We add the elvis operator ($\elvis{}$) to the syntax mainly to showcase applications involving wildcard types.
which are also inferred by our algorithm. \item \textit{Note:} The \texttt{new} expression is not requiring generic parameters.
The method call naturally has type inferred generic parameters aswell. \item Every method has an unique name.
We add the elvis operator ($\elvis{}$) to the syntax mainly to showcase applications involving wildcard types. The calculus does not include method overriding for simplicity reasons.
The syntax is described in figure \ref{fig:syntax} with optional type annotations highlighted in yellow.
It is possible to exclude all optional types.
\TamedFJ{} is a subset of the calculus defined by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection}.
%The language is designed to showcase type inference involving existential types.
The idea is for our type inference algorithm to calculate all missing types and output a fully and correctly typed \TamedFJ{} program,
which by default is also a correct Featherweight Java program (see chapter \ref{sec:soundness}).
\noindent
\textit{Notes:}
\begin{itemize}
\item 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. Type inference for that is described in \cite{TIforFGJ} and can be added to this algorithm accordingly.
%\textit{Note:} \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. \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 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. 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 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 \cite{WildcardsNeedWitnessProtection} as possible. and as close to it's Featherweight Java correspondent as possible,
Our soundness proof works either way. simplifying the soundness proof.
\end{itemize} \end{itemize}
%Additional features like overriding methods and method overloading can be added by copying the respective parts from there. %Additional features like overriding methods and method overloading can be added by copying the respective parts from there.