Introduce new challenge (principal type). Restructure and remove some parts.
This commit is contained in:
Andreas Stadelmeier
parent
9a7195d261
commit
c7212cd7c6
335
introduction.tex
335
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<X> extends Object {...}
|
||||
class List2D<X> extends List<List<X>> {...}
|
||||
|
||||
<X> void shuffle(List<List<X>> 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 <X>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}
|
||||
<X> List<X> concat(List<X> 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<Object>(), 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<A,B extends A> extends List<B>{
|
||||
void addAll(List<B> 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<String>} is a subtype of \texttt{List<? extend Object>}.
|
||||
|
||||
\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{<X>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<X> extends Object {...}
|
||||
class List2D<X> extends List<List<X>> {...}
|
||||
|
||||
<X> void shuffle(List<List<X>> 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 <X>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}
|
||||
<A> List<A> id(List<A> 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}
|
||||
% <A> List<A> id(List<A> a) = a
|
||||
|
||||
m() = new List<String>() :? new List<Integer>() :? 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<String>() :? new List<Integer>() :? 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<String>() :? new List<Integer>() :? 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<String>() :? new List<Integer>() :? 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<X, Y extends X> extends Pair<X,Y>{}
|
||||
|
||||
|
||||
<X,Y> Pair<X,Y> id(Pair<X,Y> in){
|
||||
return ...;
|
||||
}
|
||||
|
||||
<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>
|
||||
|
||||
|
||||
\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]
|
||||
<X> List<X> clone(List<X> l);
|
||||
example(p){
|
||||
|
||||
@ -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}
|
||||
}
|
||||
|
||||
|
||||
@ -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}
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user