diff --git a/constraints.tex b/constraints.tex index a921ee4..7d2b72e 100644 --- a/constraints.tex +++ b/constraints.tex @@ -43,6 +43,9 @@ We preemptively enclose every expression in a let statement before using it as a % This behaviour emulates Java's implicit capture conversion. +%TODO: how are the challenges solved: +The \unify{} algorithm only sees the constraints with no information about the program they originated from. + \subsection{ANF transformation}\label{sec:anfTransformation} \newcommand{\anf}[1]{\ensuremath{\tau}(#1)} diff --git a/introduction.tex b/introduction.tex index c437897..02295bd 100644 --- a/introduction.tex +++ b/introduction.tex @@ -181,8 +181,44 @@ if not for the Java type system which rejects the assignment \texttt{lo = ls}. Listing \ref{lst:wildcardIntro} shows the use of wildcards rendering the assignment \texttt{lo = ls} correct. The program still does not compile, because now the addition of an Integer to \texttt{lo} is rightfully deemed incorrect by Java. -% Goal: Motivate the TamedFJ language. Why do we need it (Capture Conversion) -This behaviour is emulated by our language \TamedFJ{}, +Wildcard types are virtual types. +There is no instantiation of a \texttt{List}. +It is a placeholder type which can hold any kind of list like +\texttt{List} or \texttt{List}. +This type can also change at any given time, for example when multiple threads +are using the same field of type \texttt{List}. +A wildcard \texttt{?} must be considered a different type everytime it is accessed. +Therefore calling the method \texttt{concat} with two wildcard lists in the example in listing \ref{lst:concatError} is incorrect. +% The \texttt{concat} method does not create a new list, +% but adds all elements from the second argument to the list given as the first argument. +% This is allowed in Java, because both lists are of the polymorphic type \texttt{List}. +% As shown in listing \ref{lst:concatError} this leads to a inconsistent \texttt{List} +% if Java would treat \texttt{?} as a regular type and instantiate the type variable \texttt{X} +% of the \texttt{concat} function with \texttt{?}. + +\begin{figure} +\begin{lstlisting}[caption=Concat Example,label=lst:concatError]{java} + List concat(List l1, List l2){ + return l1.addAll(l2); +} + +List ls = new List(); + +List l1 = ls; +List l2 = new List(1); + +concat(l1, l2); +\end{lstlisting} +\begin{lstlisting}[style=TamedFJ,caption=\TamedFJ{} representation, label=lst:concatTamedFJ] +let l1' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l1 in + let l2' : (*@$\wctype{\rwildcard{Y}}{List}{\exptype{List}{\rwildcard{Y}}}$@*) = l2 in + concat(l1', l2') // Error! +\end{lstlisting} +\end{figure} + +To enable the use of wildcards in argument types of a method invocation +Java uses a process called \textit{Capture Conversion}. +This behaviour is emulated by our language \TamedFJ{}; a Featherweight Java \cite{FJ} derivative with added wildcard support and a global type inference feature (syntax definition in section \ref{sec:tifj}). %\TamedFJ{} is basically the language described by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection} with optional type annotations. @@ -246,7 +282,7 @@ add(l, "String"); \end{lstlisting} \end{minipage}\hfill \begin{minipage}{0.49\textwidth} -\begin{lstlisting}[style=letfj, caption=\letfj{} representation, label=lst:addExampleLet] +\begin{lstlisting}[style=letfj, caption=\TamedFJ{} representation, label=lst:addExampleLet] List add(List l, A v) let l2 : (*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = l @@ -255,7 +291,7 @@ let l2 : (*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcar \end{minipage} \end{figure} -The Example in listing \ref{lst:addExample} is a valid Java program. Here Java uses local type inference \cite{JavaLocalTI} +In listing \ref{lst:addExample} Java uses local type inference \cite{JavaLocalTI} to determine the type parameters to the \texttt{add} method call. A \TamedFJ{} representation including all type annotations and an explicit capture conversion via let statement is shown in listing \ref{lst:addExampleLet}. %In \letfj{} there is no local type inference and all type parameters for a method call are mandatory (see listing \ref{lst:addExampleLet}). @@ -294,7 +330,7 @@ The \texttt{shuffle} method in this case is invoked with the type $\wctype{\rwil 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] +\begin{lstlisting}[style=TamedFJ] let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in shuffle(l2d') \end{lstlisting} @@ -457,106 +493,24 @@ A problem arises when replacing type variables with wildcards. Lets have a look at a few challenges: \begin{itemize} \item -%Passing wildcard types to a polymorphic method call comes with additional challenges. -% TODO: Here the concat example! -%- Wildcards are not reflexive -%- Wildcards are opaque types. Behind a Java Wildcard is a real type. - -Wildcard types are virtual types. -There is no instantiation of a \texttt{List}. -It is a placeholder type which can hold any kind of list like -\texttt{List} or \texttt{List}. -This type can also change at any given time, for example when multiple threads -are using the same field of type \texttt{List}. -A wildcard \texttt{?} must be considered a different type everytime it is accessed. -Therefore calling the method \texttt{concat} with two wildcard lists in the example in listing \ref{lst:concatError} is incorrect. -The \texttt{concat} method does not create a new list, -but adds all elements from the second argument to the list given as the first argument. -This is allowed in Java, because both lists are of the polymorphic type \texttt{List}. -As shown in listing \ref{lst:concatError} this leads to a inconsistent \texttt{List} -if Java would treat \texttt{?} as a regular type and instantiate the type variable \texttt{X} -of the \texttt{concat} function with \texttt{?}. -To enable the use of wildcards in argument types of a method invocation -Java uses a process called \textit{Capture Conversion}. - -\begin{lstlisting}[caption=Concat Example,label=lst:concatError]{java} - List concat(List l1, List l2){ - return l1.addAll(l2); -} - -List ls = new List(); - -List l1 = ls; -List l2 = new List(1); - -concat(l1, l2); -\end{lstlisting} - - -%Existential types enable us to formalize Java's method call behavior and the so called Capture Conversion. -\begin{displaymath} -%TODO: -\begin{array}{l} - \begin{array}{@{}c} - \textit{mtype}(\texttt{concat}) = \generics{\type{X}}\ \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \to \exptype{List}{\type{X}} \\ - \texttt{l1} : \wctype{\rwildcard{A}}{List}{\rwildcard{A}}, \texttt{l2} : \wctype{\rwildcard{B}}{List}{\rwildcard{B}} \\ - \exptype{List}{\rwildcard{A}} \nless: [{\color{red}?}/\type{X}]\exptype{List}{\type{X}} \quad \quad -\exptype{List}{\rwildcard{B}} \nless: [{\color{red}?}/\type{X}]\exptype{List}{\type{X}} - \\ - \hline - \vspace*{-0.3cm}\\ - \texttt{concat}(\expr{l1}, \expr{l2}) : {\color{red}\textbf{Errror}} - \end{array} - \end{array} -\end{displaymath} - -%A method call in Java makes use of the fact that a real type is behind a wildcard type - -\item \begin{example} \label{intro-example1} -The first one is a valid Java program. -The type \texttt{List} is \textit{capture converted} to a fresh type variable $\rwildcard{X}$ -which is used as the generic method parameter \texttt{A}. - -Java uses capture conversion to replace the generic \texttt{A} by a capture converted version of the -\texttt{? super String} wildcard. -Knowing that the type \texttt{String} is a subtype of any type the wildcard \texttt{? super String} can inherit +One challenge is to design the algorithm in a way that it finds a correct solution for the program shown in listing \ref{lst:addExample} +and rejects the program in listing \ref{lst:concatError}. +The first one is a valid Java program, +because the type \texttt{List} is \textit{capture converted} to a fresh type variable $\rwildcard{X}$ +which is used as the generic method parameter for the call to \texttt{add} as shown in listing \ref{lst:addExampleLet}. +Knowing that the type \texttt{String} is a subtype of the free variable $\rwildcard{X}$ it is safe to pass \texttt{"String"} for the first parameter of the function. -\begin{verbatim} - List add(List l, A v) {} - -List list = ...; -add(list, "String"); -\end{verbatim} -\end{example} - -\item \begin{example}\label{intro-example2} -This example displays an incorrect Java program. +The second program shown in listing \ref{lst:concatError} is incorrect. 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} - List concat(List l1, List l2) { ... } -List getList() { ... } - -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}}}$. +The problem gets apparent when we try to write the \texttt{concat} method call in our \TamedFJ{} calculus (listing \ref{lst:concatTamedFJ}): +\texttt{l1'} and \texttt{l2'} are two different lists inside the body of the let statements, namely +$\exptype{List}{\rwildcard{X}}$ and $\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}}$ -\end{example} % \item % \unify{} morphs a constraint set into a correct type solution @@ -649,5 +603,3 @@ $\ntv{z}$ is a normal placeholder and is not allowed to contain free variables. \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}.