From 8b0e77cf506bb37fbde8901956df9c563ab3730c Mon Sep 17 00:00:00 2001 From: Peter Thiemann Date: Wed, 29 May 2024 12:07:10 +0200 Subject: [PATCH] cosmetics --- constraints.tex | 9 +++-- introduction.tex | 1 + tRules.tex | 90 ++++++++++++++++++++++++++++-------------------- 3 files changed, 60 insertions(+), 40 deletions(-) diff --git a/constraints.tex b/constraints.tex index 69bafd4..2d05df5 100644 --- a/constraints.tex +++ b/constraints.tex @@ -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} \ No newline at end of file +% \end{displaymath} +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "TIforWildFJ" +%%% End: diff --git a/introduction.tex b/introduction.tex index a6666fb..38d06e8 100644 --- a/introduction.tex +++ b/introduction.tex @@ -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} diff --git a/tRules.tex b/tRules.tex index 79795fd..3e2e014 100644 --- a/tRules.tex +++ b/tRules.tex @@ -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 { \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} \ No newline at end of file +\end{figure} +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "TIforWildFJ" +%%% End: