diff --git a/introduction.tex b/introduction.tex index e68140c..a6666fb 100644 --- a/introduction.tex +++ b/introduction.tex @@ -550,12 +550,31 @@ is solved by removing the wildcard $\rwildcard{X}$ if possible. this problem is solved by ANF transformation -\item \textbf{Wildcards as Existential 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} -can emerge, which have no equivalent in the Java syntax. +\item +% This problem is solved by assuming everything is a wildcard and lateron erasing excessive wildcards +% this is solved by having wildcards bound to a type. But this makes it necessary to remove wildcards lateron otherwise Unify would have to backtrack +The program in listing \ref{shuffleExample} shows a challenge involving wildcards and subtyping. +The method call \texttt{shuffle(l)} is incorrect, because \texttt{l} has the type +$\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ representing a list of unknown lists. +Whereas $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ is a subtype of +$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ representing a list of lists, all of the same type $\rwildcard{X}$, +and can savely be passed to \texttt{shuffle}. +This behavior can also be explained by looking at the types and their capture converted versions: +\begin{center} +\begin{tabular}{l | l | l} +Java type & \TamedFJ{} representation & Capture Conversion \\ +\hline +$\exptype{List}{\exptype{List}{\texttt{?}}}$ & $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ & $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ \\ +$\exptype{List2D}{\texttt{?}}$ & $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$ & $\exptype{List2D}{\rwildcard{X}}$ \\ +%Supertype of $\exptype{List2D}{\texttt{?}}$ & $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ & $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$ \\ +\end{tabular} +\end{center} +%The direct supertype of $\exptype{List2D}{\rwildcard{X}}$ is $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$. +%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} +%can emerge, which have no equivalent in the Java syntax. \begin{lstlisting}[style=java,label=shuffleExample,caption=Intermediate Types Example] class List extends Object {...} @@ -569,45 +588,64 @@ 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=TamedFJ] -let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in shuffle(l2d') -\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=TamedFJ] +% let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in shuffle(l2d') +% \end{lstlisting} -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} +% 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}}}$ +Given such a program our type inference algorithm has to allow the call \texttt{shuffle(l2d)} and +decline the call to \texttt{shuffle(l)}. + +% 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}}}$ \item \label{challenge3} \textbf{Free Variables cannot leaver their scope}: +Let's assume we have a variable \texttt{ls} with type $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$ +%When calling the \texttt{id} function with an element of this list we have to apply capture conversion. +and the following input program: + +\noindent +\begin{minipage}{0.62\textwidth} +\begin{lstlisting} +let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = ls.get(0) in id(x) : (*@$\ntv{z}$@*) +\end{lstlisting}\end{minipage} + \hfill +\begin{minipage}{0.36\textwidth} + \begin{lstlisting}[style=constraints] +(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$@*), +(*@$\exptype{List}{\wtv{x}} \lessdot \ntv{z},$@*) + \end{lstlisting} +\end{minipage} +% the variable z has to -\begin{example} Take the Java program in listing \ref{lst:mapExample} for example. It maps every element of a list $\expr{l} : \exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$ @@ -655,8 +693,6 @@ $\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$ We solve this by distinguishing between wildcard placeholders and normal placeholders. $\ntv{z}$ is a normal placeholder and is not allowed to contain free variables. -\end{example} - \end{enumerate} %TODO: Move this part. or move the third challenge some underneath.