stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

cosmetics

Browse Source
This commit is contained in:
Peter Thiemann 2024-05-29 12:07:10 +02:00
parent e42b0aaafe
commit 8b0e77cf50
3 changed files with 60 additions and 40 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
constraints.tex
View File

@ -61,7 +61,8 @@ In the special case \lstinline{let x = v in concat(x,x)} the constraints would l
$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}},
\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
and we could actually delete one of them without loosing information.
But this case will never occur in our algorithm, because the let statements for our input programs are generated by a ANF transformation (see \ref{sec:anfTransformation}).
But this case will never occur in our algorithm, because the let
statements for our input programs are generated by transformation to ANF (see \ref{sec:anfTransformation}).
@ -507,4 +508,8 @@ cannot be used anywhere else then inside the constraints generated by the method
% \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}
% \end{displaymath}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "TIforWildFJ"
%%% End:

1
introduction.tex
View File

@ -385,6 +385,7 @@ let l1' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) =
\section{Global Type Inference Algorithm}
\label{sec:glob-type-infer}
\begin{figure}[h]
\begin{minipage}{0.49\textwidth}

90
tRules.tex
View File

@ -5,24 +5,26 @@
%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.
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.
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.
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 (see chapter \ref{sec:soundness}).
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 out of a method name, a list of type parameters, a list of argument types, and a return type.
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:
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.
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}
@ -55,23 +57,25 @@ class List<A extends Object> {
\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.
\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 mainly to showcase applications involving wildcard types.
\item \textit{Note:} The \texttt{new} expression is not requiring generic parameters.
\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 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
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 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.
\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.
@ -123,18 +127,20 @@ $\begin{array}{l}
\begin{array}{@{}c}
\Delta \vdash \type{T} <: \type{T}
\end{array}
\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{T}
\Delta \vdash \type{S} <: \type{T} \quad \quad
\Delta \vdash \type{T} <: \type{U}
\\
\hline
\vspace*{-0.3cm}\\
\Delta \vdash \type{S} <: \type{T}
\Delta \vdash \type{S} <: \type{U}
\end{array}
\end{array}$
\end{array}$
\qquad
$\begin{array}{l}
\typerule{S-Upper}\\
\begin{array}{@{}c}
@ -144,7 +150,8 @@ $\begin{array}{l}
\vspace*{-0.9em}\\
\Delta \vdash \type{X} <: \type{U}
\end{array}
\end{array}$
\end{array}$
\qquad
$\begin{array}{l}
\typerule{S-Lower}\\
\begin{array}{@{}c}
@ -166,7 +173,8 @@ $\begin{array}{l}
\vspace*{-0.3cm}\\
\Delta \vdash \wctype{\Delta'}{C}{\ol{T}} <: \wcNtype{\Delta'}{[\ol{T}/\ol{X}]\type{N}}
\end{array}
\end{array}$
\end{array}$
\quad
$\begin{array}{l}
\typerule{S-Exists}\\
\begin{array}{@{}c}
@ -193,6 +201,7 @@ $\begin{array}{l}
\Delta \vdash \bot \ \ok
\end{array}
\end{array}$
\qquad
$\begin{array}{l}
\typerule{WF-Top}\\
\begin{array}{@{}c}
@ -203,6 +212,7 @@ $\begin{array}{l}
\Delta \vdash \overline{\wildcard{W}{U}{L}}.\texttt{Object}
\end{array}
\end{array}$
\qquad
$\begin{array}{l}
\typerule{WF-Var}\\
\begin{array}{@{}c}
@ -363,14 +373,14 @@ $\begin{array}{l}
$\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
\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{T}
\triangle | \Gamma \vdash \texttt{t}_1 \ \texttt{?:} \ \texttt{t}_2 : \type{U}
\end{array}
\end{array}$
\end{center}
@ -443,4 +453,8 @@ $\begin{array}{l}
\end{array}
\end{array}$
\caption{Field access}
\end{figure}
\end{figure}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "TIforWildFJ"
%%% End: