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

Change principal type problem in introduction

Browse Source
This commit is contained in:
JanUlrich 2024-04-08 21:45:29 +02:00
parent 2b41b56498
commit 5718c42e28
3 changed files with 38 additions and 75 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

109
introduction.tex
View File

@ -509,11 +509,23 @@ The method call to \texttt{concat} with two wildcard lists is unsound.
Each list could be of a different kind and therefore the \texttt{concat} cannot succeed.
\begin{verbatim}
<A> List<A> concat(List<A> l1, List<A> l2) { ... }
List<?> getList() { ... }
List<?> list = ... ;
concat(list, list);
concat(getList(), getList());
\end{verbatim}
The \letfj{} representation in listing \ref{letfjConcatFail} clarifies this.
Inside the let statement the variables hold the types
$\set{ \texttt{x1} : \exptype{List}{\rwildcard{X}}, \texttt{x2} : \exptype{List}{\rwildcard{Y}}}$.
For the method call \texttt{concat(x1, x2)} no replacement for the generic \texttt{A}
exists to satisfy
$\exptype{List}{\type{A}} <: \exptype{List}{\type{X}},
\exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$.
\begin{lstlisting}[style=letfj,caption=Incorrect method call,label=letfjConcatFail]
let x1 : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = getList() in
let x2 : (*@$\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}$@*) = getList() in
concat(x1, x2)
\end{lstlisting}
% $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}, \\
% \wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
@ -536,79 +548,30 @@ 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 SpecialPair<X, Y extends X> extends Pair<X,Y>{}
\item \textbf{Capture Conversion during \unify{}:}
The return type of a generic method call depends on its argument types.
A method like \texttt{String trim(String s)} will always return a \type{String} type.
However the return type of \texttt{<A> A head(List<A> l)} is a generic variable \texttt{A} and only shows
its actual type when the type of the argument list \texttt{l} is known.
The same goes for capture conversion, which can only be applied for a method call
when the argument types are given.
At the start of our global type inference algorithm no types are assigned yet.
During the course of the \unify{} algorithm more and more types emerge.
As soon as enough type information is given \unify{} can conduct a capture conversion if needed.
The constraints where this is possible are marked as capture constraints.
Type information flows top down.
Argument types of a method invocation impact its return type.
But knowing the return type does not imply distinct argument types.
The code in listing \ref{principalTypeExample} shows a nested method call
\texttt{receive(copy(lSpecial))}.
We know from the argument types of \texttt{receive} -which are given- that the \texttt{copy} method
needs to return a type of the form $\exptype{Pair}{\type{X}, \type{Y}}$
where \type{X} and \type{Y} can be any types as long as \type{Y} is a subtype of \type{X}.
Without wildcards this would leave us with a clue what the type should look like.
<X,Y> Pair<X,Y> id(Pair<X,Y> in){
return in;
}
<X, Y extends X> void receive(Pair<X,Y> 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<X> <. a as a =. X.C<X>
% A method has infinte possibilities of being called and there is no most general type.
% P<X,Y> m(C<X> c, C<Y> c2)
% depending on
% A.P<A,A> <. A,B.P<A,B>
% % During the method call it is not sure what kind of return type is needed from the method.
% % The method P<A,B> make(A a, B b)
% % The type A,B.P<A,B> cannot be a subtype of P<X,X>
% % But if A^X_X and B^X_X
% % Could a constraint C<X> <. a? be expanded to a? = X^u?_l?.C<X>
%TODO: simplify this example. lSpeial <. List<x> and List<x> <. id is sufficient
% The unify algorithm needs to resolve l <c List<x?> to l <. X.List<X>, X.List<X> <c List<x?>
\end{itemize}

2
prolog.tex
View File

@ -97,7 +97,7 @@
\newcommand{\constraints}{\ensuremath{\mathit{\overline{c}}}}
\newcommand{\itype}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\il}[1]{\ensuremath{\overline{\itype{#1}}}}
\newcommand{\type}[1]{\mathtt{#1}}
\newcommand{\type}[1]{\ensuremath{\mathtt{#1}}}
\newcommand{\anyType}[1]{\mathit{#1}}
\newcommand{\gType}[1]{\texttt{#1}}
\newcommand{\mtypeEnvironment}{\ensuremath{\Pi}}

2
tRules.tex
View File

@ -132,7 +132,7 @@ $
% \caption{Input Syntax}\label{fig:syntax}
% \end{figure}
\subsection{ANF transformation}\ref{sec:anfTransformation}
\subsection{ANF transformation}\label{sec:anfTransformation}
\newcommand{\anf}[1]{\ensuremath{\tau}(#1)}
%https://en.wikipedia.org/wiki/A-normal_form)
Featherweight Java's syntax involves no \texttt{let} statement