From c7212cd7c6fcb27b2866a636e74cf729cb806f04 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Wed, 13 Mar 2024 00:30:16 +0100 Subject: [PATCH] Introduce new challenge (principal type). Restructure and remove some parts. --- introduction.tex | 335 +++++++++++++++++++++++++---------------------- martin.bib | 8 ++ prolog.tex | 1 + 3 files changed, 190 insertions(+), 154 deletions(-) diff --git a/introduction.tex b/introduction.tex index 62ba736..f3328e6 100644 --- a/introduction.tex +++ b/introduction.tex @@ -182,138 +182,6 @@ Those properties are needed to formalize capture conversion. Polymorphic method calls need to be wraped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}. In Java this is done implicitly in a process called capture conversion. -One problem is the divergence between denotable and expressable types in Java \cite{semanticWildcardModel}. -A wildcard in the Java syntax has no name and is bound to its enclosing type. -$\exptype{List}{\exptype{List}{\type{?}}}$ equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$. -During type checking \emph{intermediate types} -%like $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ -%or $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ -can emerge, which have no equivalent in the Java syntax. -%Our type inference algorithm uses existential types internally but spawns type solutions compatible with Java. - -Example: % This program is not typable with the Type Inference algorithm from Plümicke -\begin{verbatim} -class List extends Object {...} -class List2D extends List> {...} - - void shuffle(List> list) {...} - -List> l = ...; -List2D l2d = ...; - -shuffle(l); // Error -shuffle(l2d); // Valid -\end{verbatim} -Java is using local type inference to allow method invocations which are not describable with regular Java types. -The \texttt{shuffle} method in this case is invoked with the type $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ -which is a subtype of $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$. -After capture conversion \texttt{l2d'} has the type $\exptype{List}{\exptype{List}{\rwildcard{X}}}$ -and \texttt{shuffle} can be invoked with the type parameter $\rwildcard{X}$: -\begin{lstlisting}[style=letfj] -let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in shuffle(l2d') -\end{lstlisting} - -The respective constraints are: -\begin{constraintset} -\begin{center} - $ - \begin{array}{l} - \wctype{\rwildcard{X}}{List2D}{\rwildcard{X}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}} - \\ - \hline - \wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}} - \\ - \hline - \textit{Capture Conversion:}\ - \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\wtv{x}}} - \\ - \hline - \textit{Solution:} \wtv{x} \doteq \rwildcard{X} \implies \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\rwildcard{X}}} - \end{array} - $ -\end{center} -\end{constraintset} - -\texttt{l} however has the type -$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$. -The method call \texttt{shuffle(l)} is not correct, because there is no solution for the subtype constraint: - -$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$ - -\section{Type Inference for Capture Conversion} -why do we need a lessdotCC constraint -\dbox{Eine dashbox!} -input is e.m(e); - -\begin{verbatim} - List concat(List a, X b){} -\end{verbatim} - -\begin{recap}\textbf{TI for FGJ without Wildcards:} -The type inference algorithm for Featherweight Generic Java \cite{TIforFGJ} (called \TFGJ{}) is complete and sound: -It is able to find a type solution for a Featherweight Generic Java program, which has no type annotations at all, -if there is any. -It's only restriction is that no polymorphic recursion is allowed. -\TFGJ{} generates subtype constraints $(\type{T} \lessdot \type{T})$ consisting of named types and type placeholders. -For example the method invocation \texttt{concat(new List(), new Object())} generates the constraints -$\exptype{List}{\tv{l}} \lessdot \exptype{List}{\tv{a}}, \type{Object} \lessdot \tv{a}$. -Subtyping without the use of wildcards is invariant \cite{FJ}: -Therefore the only possible solution for the type placeholders $\tv{l}$ and $\tv{a}$ is $\tv{l} \doteq \type{Object}$ and $\tv{a} \doteq \type{Object}$. % in Java and Featherweight Java. -Solution: \texttt{concat(new List(), new Object())} -%- usually the type of e must be subtypes of the method parameters -%- in case of a polymorphic method: type placeholders resemble type parameters -\end{recap} -In \letfj{} the \texttt{concat} method has infinitely many possibilities of argument types. -It can be called with a $\exptype{List}{\type{String}}$ or $\wctype{\wildcard{X}{\type{String}}{\type{Object}}}{List}{\rwildcard{X}}$ -or $\wctype{\rwildcard{X}, \wildcard{Y}{\bot}{\rwildcard{X}}}{List}{\rwildcard{X}}$ -\begin{lstlisting} -class List2 extends List{ - void addAll(List l){ ... } -} - - -\end{lstlisting} - -% TODO: Change example: Assuming String is a final type. - -involving wildcards: -- depending on the type of e a capture conversion must be applied first -- the captured type N must be a subtype of the method parameters -- type parameters: can be set to free variables! - - but must afterwards be closed again - - the free variables can only be used inside the let statement -- we align the let statements in a way thate mimics Java capture conversion: - - -% $\exptype{List}{String} <: \wctype{\wildcard{X}{\bot}{\type{Object}}}{List}{\rwildcard{X}}$ -% means \texttt{List} is a subtype of \texttt{List}. - -\subsection{Global Type Inference} -% A global type inference algorithm works on an input with no type annotations at all. -% \begin{verbatim} -% m(l) { -% return l.add(l); -% } -% \end{verbatim} - -% $\tv{l} \lessdotCC \exptype{List}{\wtv{x}}, \tv{l} \lessdotCC \wtv{x}$ - -\begin{description} - \item[input] \tifj{} program - \item[output] type solution - \item[postcondition] the type solution applied to the input must yield a valid \letfj{} program -\end{description} - -The input to our type inference algorithm is a modified version of the \letfj{}\cite{WildcardsNeedWitnessProtection} calculus (see chapter \ref{sec:tifj}). -First \fjtype{} generates constraints -and afterwards \unify{} computes a solution for the given constraint set. -Constraints consist out of subtype constraints $(\type{T} \lessdot \type{T})$ and capture constraints $(\type{T} \lessdotCC \type{T})$. -\textit{Note:} a type $\type{T}$ can also be a type placeholders $\ntv{a}$ or a wildcard type placeholder $\wtv{a}$. -A subtype constraint is satisfied if the left side is a subtype of the right side according to the rules in figure \ref{fig:subtyping}. -\textit{Example:} $\exptype{List}{\ntv{a}} \lessdot \exptype{List}{\type{String}}$ is fulfilled by replacing type placeholder $\ntv{a}$ with the type $\type{String}$. -Subtype constraints and type placeholders act the same as the ones used in \emph{Type Inference for Featherweight Generic Java} \cite{TIforFGJ}. -The novel capture constraints and wildcard placeholders are needed for method invocations involving wildcards. - %show input and a correct letFJ representation %TODO: first show local type inference and explain lessdotCC constraints. then show example with global TI \begin{figure}[h] @@ -347,8 +215,71 @@ becomes $\exptype{List}{\rwildcard{X}}$ and the wildcard $\wildcard{X}{\type{Obj a type parameter to \texttt{add(...)}. %This is a valid Java program where the type parameters for the polymorphic method \texttt{add} %are determined by local type inference. -Our type inference algorithm has to add let statements if necessary, including the capture types. +One problem is the divergence between denotable and expressable types in Java \cite{semanticWildcardModel}. +A wildcard in the Java syntax has no name and is bound to its enclosing type: +$\exptype{List}{\exptype{List}{\type{?}}}$ equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$. +During type checking \emph{intermediate types} +%like $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ +%or $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ +can emerge, which have no equivalent in the Java syntax. +%Our type inference algorithm uses existential types internally but spawns type solutions compatible with Java. + +Example: % This program is not typable with the Type Inference algorithm from Plümicke +\begin{lstlisting}[style=java,label=shuffleExample,caption=Intermediate Types Example] +class List extends Object {...} +class List2D extends List> {...} + + void shuffle(List> list) {...} + +List> l = ...; +List2D l2d = ...; + +shuffle(l); // Error +shuffle(l2d); // Valid +\end{lstlisting} +Java is using local type inference to allow method invocations which are not describable with regular Java types. +The \texttt{shuffle} method in this case is invoked with the type $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ +which is a subtype of $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$. +After capture conversion \texttt{l2d'} has the type $\exptype{List}{\exptype{List}{\rwildcard{X}}}$ +and \texttt{shuffle} can be invoked with the type parameter $\rwildcard{X}$: +\begin{lstlisting}[style=letfj] +let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in shuffle(l2d') +\end{lstlisting} + +\subsection{Global Type Inference} + +\begin{description} + \item[input] \tifj{} program + \item[output] type solution + \item[postcondition] the type solution applied to the input must yield a valid \letfj{} program +\end{description} + +The input to our type inference algorithm is a modified version of the \letfj{}\cite{WildcardsNeedWitnessProtection} calculus (see chapter \ref{sec:tifj}). +First \fjtype{} generates constraints +and afterwards \unify{} computes a solution for the given constraint set. +Constraints consist out of subtype constraints $(\type{T} \lessdot \type{T})$ and capture constraints $(\type{T} \lessdotCC \type{T})$. +\textit{Note:} a type $\type{T}$ can either be a named type, a type placeholder $\ntv{a}$ or a wildcard type placeholder $\wtv{a}$. +A subtype constraint is satisfied if the left side is a subtype of the right side according to the rules in figure \ref{fig:subtyping}. +\textit{Example:} $\exptype{List}{\ntv{a}} \lessdot \exptype{List}{\type{String}}$ is fulfilled by replacing type placeholder $\ntv{a}$ with the type $\type{String}$. +Subtype constraints and type placeholders act the same as the ones used in \emph{Type Inference for Featherweight Generic Java} \cite{TIforFGJ}. +The novel capture constraints and wildcard placeholders are needed for method invocations involving wildcards. + +\begin{recap}\textbf{TI for FGJ without Wildcards:} +\TFGJ{} generates subtype constraints $(\type{T} \lessdot \type{T})$ consisting of named types and type placeholders. +For example the method invocation \texttt{concat(l, new Object())} generates the constraints +$\tv{l} \lessdot \exptype{List}{\tv{a}}, \type{Object} \lessdot \tv{a}$. +Subtyping without the use of wildcards is invariant \cite{FJ}: +Therefore the only possible solution for the type placeholder $\tv{a}$ is $\tv{a} \doteq \type{Object}$. % in Java and Featherweight Java. +The correct type for the variable \texttt{l} is $\exptype{List}{\type{Object}}$ (or a direct subtype). +%- usually the type of e must be subtypes of the method parameters +%- in case of a polymorphic method: type placeholders resemble type parameters +The type inference algorithm for Featherweight Generic Java \cite{TIforFGJ} (called \TFGJ{}) is complete and sound: +It is able to find a type solution for a Featherweight Generic Java program, which has no type annotations at all, +if there is any. +It's only restriction is that no polymorphic recursion is allowed. +\end{recap} +% Lets have a look at the constraints generated by \fjtype{} for the example in listing \ref{lst:addExample}: \begin{constraintset} \begin{center} @@ -364,12 +295,45 @@ $\begin{array}{c} $ \end{center} \end{constraintset} +% +Capture Constraints $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ allow for a capture conversion, +which converts a constraint of the form $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ to $(\exptype{C}{\rwildcard{X}} \lessdot \type{T})$ +%These constraints are used at places where a capture conversion via let statement can be added. + %Why do we need the lessdotCC constraints here? The type of \texttt{l} can be capture converted by a let statement if needed (see listing \ref{lst:addExampleLet}). Therefore we assign the constraint $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$ which allows \unify{} to do a capture conversion to $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$. \textit{Note:} The constraint $\type{String} \lessdot \rwildcard{X}$ is satisfied because $\rwildcard{X}$ has $\type{String}$ as lower bound. + +For the example shown in listing \ref{shuffleExample} the method call \texttt{shuffle(l2d)} creates the constraints: +\begin{constraintset} +\begin{center} + $ + \begin{array}{l} + \wctype{\rwildcard{X}}{List2D}{\rwildcard{X}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}} + \\ + \hline + \wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}} + \\ + \hline + \textit{Capture Conversion:}\ + \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\wtv{x}}} + \\ + \hline + \textit{Solution:} \wtv{x} \doteq \rwildcard{X} \implies \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\rwildcard{X}}} + \end{array} + $ +\end{center} +\end{constraintset} + +The method call \texttt{shuffle(l)} is invalid however, +because \texttt{l} has the type +$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$. +There is no solution for the subtype constraint: +$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$ + % No capture conversion for methods in the same class: % Given two methods without type annotations like % \begin{verbatim} @@ -395,28 +359,28 @@ which allows \unify{} to do a capture conversion to $\exptype{List}{\rwildcard{X % List id(List a) = a % \end{verbatim} -The following example has the \texttt{id} method already typed and the method \texttt{m} -extended by a recursive call \texttt{id(m())}: -\begin{verbatim} - List id(List a) = a +% The following example has the \texttt{id} method already typed and the method \texttt{m} +% extended by a recursive call \texttt{id(m())}: +% \begin{verbatim} +% List id(List a) = a -m() = new List() :? new List() :? id(m()); -\end{verbatim} -Now the constraints make use of a $\lessdotCC$ constraint: -$\exptype{List}{\type{String}} \lessdot \ntv{r}, -\exptype{List}{\type{Integer}} \lessdot \ntv{r}, -\ntv{r} \lessdotCC \exptype{List}{\wtv{a}}$ +% m() = new List() :? new List() :? id(m()); +% \end{verbatim} +% Now the constraints make use of a $\lessdotCC$ constraint: +% $\exptype{List}{\type{String}} \lessdot \ntv{r}, +% \exptype{List}{\type{Integer}} \lessdot \ntv{r}, +% \ntv{r} \lessdotCC \exptype{List}{\wtv{a}}$ -After substituting $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\ntv{r}$ like in the example before -we get the constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$. -Due to the $\lessdotCC$ \unify{} is allowed to perform a capture conversion yielding -$\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$. -\textit{Note:} The wildcard placeholder $\wtv{a}$ is allowed to hold free variables whereas a normal placeholder like $\ntv{r}$ -is never assigned a type containing free variables. -Therefore \unify{} sets $\wtv{a} \doteq \rwildcard{X}$, completing the constraint set and resulting in the type solution: -\begin{verbatim} -List m() = new List() :? new List() :? id(m()); -\end{verbatim} +% After substituting $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\ntv{r}$ like in the example before +% we get the constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$. +% Due to the $\lessdotCC$ \unify{} is allowed to perform a capture conversion yielding +% $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$. +% \textit{Note:} The wildcard placeholder $\wtv{a}$ is allowed to hold free variables whereas a normal placeholder like $\ntv{r}$ +% is never assigned a type containing free variables. +% Therefore \unify{} sets $\wtv{a} \doteq \rwildcard{X}$, completing the constraint set and resulting in the type solution: +% \begin{verbatim} +% List m() = new List() :? new List() :? id(m()); +% \end{verbatim} \subsection{Challenges}\label{challenges} @@ -487,9 +451,72 @@ concat(list, list); % An additional constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ % is solved by removing the wildcard $\rwildcard{X}$ if possible. +\item \textbf{No principal method type:} +We tried to skip capture conversion and the capture constraints entirely. +But \letfj{}'s type system does not imply a principal typing for methods \cite{principalTypes}. +The problem is that a principal type of a method should have the most general parameter types and the most specific return type. +\begin{lstlisting}[caption=Return type depends on argument types,label=principalTypeExample] +class SpecialPair2 extends Pair{} + + + Pair id(Pair in){ + return ...; +} + + void receive(Pair in){} + +Pair l; +SpecialPair lSpecial; + +id(l); // this has to work +receive(id(lSpecial)); // and this too +\end{lstlisting} + +By means of subtyping we are able to create types like +$\wctype{\rwildcard{X}, \wildcard{Y}{\rwildcard{X}}{\bot}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$ +as a direct supertype of \texttt{SpecialPair}, +which is now compatible with the \texttt{receive} method. +The call \texttt{receive(id(lSpecial))} is correct whereas the return type of the \texttt{id} method +does not imply so. + +If we look at this in the context of global type inference and assume that there are no type annotations for \texttt{l} and \texttt{lSpecial}. +We can neither apply capture conversion during the constraint generation step, because the parameter types are not known yet +and we also can't assume a most generic type for the parameter types, because the the needed return type is not known either. +Take the example in figure \ref{fig:principalTI}. +As soon as the type of $\tv{lSpecial}$ is resolved \unify{} can determine the type of $\tv{id}$ +and then solve the constraints $\tv{id} \lessdotCC \exptype{Pair}{\wtv{e}, \wtv{f}}, \wtv{f} \lessdot \wtv{e}$. +%TODO: explain how type variables are named after their respective variables and methods +Capture Conversion cannot be applied before the argument type ($\tv{lSpecial}$ in this case) is known. +Trying to give $\tv{lSpecial}$ a most general type like \texttt{Pair} won't work either (see listing \ref{principalTypeExample}). + +\begin{figure} +\begin{minipage}{0.40\textwidth} +\begin{lstlisting}[style=tfgj] +// l and lSpecial are untyped +id(l); +receive(id(lSpecial)); +\end{lstlisting} +\end{minipage}% +\hfill +\begin{minipage}{0.59\textwidth} +\begin{constraintset} +$ +\tv{l} \lessdotCC \exptype{Pair}{\wtv{a}, \wtv{b}}, \\ +\tv{lSpecial} \lessdotCC \exptype{Pair}{\wtv{c}, \wtv{d}}, +\exptype{Pair}{\wtv{c}, \wtv{d}} \lessdot \tv{id}, \\ +\tv{id} \lessdotCC \exptype{Pair}{\wtv{e}, \wtv{f}}, +\wtv{f} \lessdot \wtv{e} +$ +\end{constraintset} +\end{minipage} +\caption{Principal Type problem}\label{fig:principalTI} +\end{figure} +% TODO: make Unify to resolve C <. a as a =. X.C + \end{itemize} +%TODO: Move this part. or move the third challenge some underneath. The \unify{} algorithm only sees the constraints with no information about the program they originated from. The main challenge was to find an algorithm which computes $\sigma(\wtv{a}) = \rwildcard{X}$ for example \ref{intro-example1} but not for example \ref{intro-example2}. @@ -499,7 +526,7 @@ Those are added after computing a type solution. Let statements act as capture conversion and only have to be applied in method calls involving wildcard types. \begin{figure} - \begin{minipage}{0.45\textwidth} +\begin{minipage}{0.45\textwidth} \begin{lstlisting}[style=fgj] List clone(List l); example(p){ diff --git a/martin.bib b/martin.bib index 2c0ef11..eea0ad2 100644 --- a/martin.bib +++ b/martin.bib @@ -448,3 +448,11 @@ numpages = {55}, keywords = {Compilation, Java, generic classes, language design, language semantics} } +@inproceedings{principalTypes, + title={What are principal typings and what are they good for?}, + author={Jim, Trevor}, + booktitle={Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, + pages={42--53}, + year={1996} +} + diff --git a/prolog.tex b/prolog.tex index f86f1e7..a60607e 100755 --- a/prolog.tex +++ b/prolog.tex @@ -14,6 +14,7 @@ \lstdefinestyle{fgj}{backgroundcolor=\color{lime!20}} \lstdefinestyle{tfgj}{backgroundcolor=\color{lightgray!20}} \lstdefinestyle{letfj}{backgroundcolor=\color{lightgray!20}} +\lstdefinestyle{java}{backgroundcolor=\color{lightgray!20}} \newtheorem{recap}[note]{Recap}