diff --git a/introduction.tex b/introduction.tex index f18516a..34fa40a 100644 --- a/introduction.tex +++ b/introduction.tex @@ -228,12 +228,32 @@ 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. +\begin{figure} +\begin{minipage}{0.48\textwidth} +\begin{lstlisting}[caption=Java Invariance Example,label=lst:invarianceExample]{java} +List ls = ...; +List lo = ...; +lo = ls; // typing error! +lo.add(new Integer(1)); +\end{lstlisting} +\end{minipage} +\hfill +\begin{minipage}{0.5\textwidth} +\begin{lstlisting}[caption=Use-Site Variance Example,label=lst:wildcardIntro]{java} +List ls = ...; +List lo = ...; +lo = ls; // correct +lo.add(new Integer(1)); // error! +\end{lstlisting} +\end{minipage} +\end{figure} + 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}. +share a reference to the same field. 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, @@ -252,70 +272,89 @@ Therefore calling the method \texttt{concat} with two wildcard lists in the exam List ls = new List(); List l1 = ls; -List l2 = new List(1); +List l2 = new List(1); // List containing Integer -concat(l1, l2); // Error! this would add an Integer to a List of Strings +concat(l1, l2); // Error! Would concat two different lists \end{lstlisting} -\begin{lstlisting}[style=TamedFJ,caption=\TamedFJ{} representation of the concat call, label=lst:concatTamedFJ] +\end{figure} + +To determine the correctness of method calls involving wildcard types Java's typecheck +makes use of a concept called \textbf{Capture Conversion}. +% was designed to make Java wildcards useful. +% - without capture conversion +% - is used to open wildcard types +% - +This process was formalized for Featherweight Java \cite{FJ} by replacing existential types with wildcards and capture conversion with let statements \cite{WildcardsNeedWitnessProtection}. +We propose our own Featherweight Java derivative called \TamedFJ{} defined in chapter \ref{sec:tifj}. +To express the example in listing \ref{lst:wildcardIntro} with our calculus we first have to translate the wildcard types: +\texttt{List} becomes $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$. +The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound, +and a type they are bound to. +In this case the name is $\rwildcard{A}$ with the upper bound $\type{Object}$ and it's bound to the the type \texttt{List}. +Before we can call the \texttt{add} method on this type we have to add a capture conversion via let statement: +\begin{lstlisting} +let v : (*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$@*) = lo in v.add(new Integer(1)); +\end{lstlisting} +\expr{lo} is assigned to a new variable \expr{v} bearing the type $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$, +but inside the let statement the variable \expr{v} will be treated as $\exptype{List}{\rwildcard{A}}$. +The idea is that every Wildcard type is backed by a concrete type. +By assigning \expr{lo} to a immutable variable \expr{v} we unpack the concrete type $\exptype{List}{\rwildcard{A}}$ +that was concealed by \expr{lo}'s existential type. +Here $\rwildcard{A}$ is a fresh variable or a captured wildcard so to say. +The only information we have about $\rwildcard{A}$ is that it is any type inbetween the bounds $\bot$ and $\type{Object}$ +It is important to give the captured wildcard type $\rwildcard{A}$ an unique name which is used nowhere else. +With this formalization it gets obvious why the method call to \texttt{concat} +in listing \ref{lst:concatError} is irregular (see \ref{lst:concatTamedFJ}). + +\begin{figure} +\begin{lstlisting}[style=TamedFJ,caption=\TamedFJ{} representation of the concat call from listing \ref{lst:concatError}, 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. -Let's have a look at a representation of the \texttt{add} call from the last line in listing \ref{lst:wildcardIntro} with our calculus \TamedFJ{}: -%The \texttt{add} call in listing \ref{lst:wildcardIntro} needs to be encased by a \texttt{let} statement in our calculus. -%This makes the capture converion explicit. -\begin{lstlisting} -let v : (*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$@*) = lo in v.add(new Integer(1)); -\end{lstlisting} -The method call is encased in a \texttt{let} statement and -\expr{lo} is assigned to a new variable \expr{v} of \linebreak[2] -\textbf{Existential Type} $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$. -Our calculus uses existential types \cite{WildFJ} to formalize wildcards: -\texttt{List} is translated to $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$ -and \texttt{List} is expressed as $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$. -The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound, -and a type they are bound to. -In this case the name is $\rwildcard{A}$ and it's bound to the the type \texttt{List}. -Inside the \texttt{let} statement the variable \expr{v} has the type -$\exptype{List}{\rwildcard{A}}$. -This is an explicit version of \linebreak[2] -\textbf{Capture Conversion}, -which makes use of the fact that a concrete type must be behind every wildcard type. -There is no instantiation of a \texttt{List}, -but there exists some unknown type $\exptype{List}{\rwildcard{A}}$, with $\rwildcard{A}$ inbetween the bounds $\bot$ (bottom type, subtype of all types) and -\texttt{Object}. -Inside the body of the let statement \expr{v} is treated as a value with the constant type $\exptype{List}{\rwildcard{A}}$. -Existential types enable us to formalize \textit{Capture Conversion}. -Polymorphic method calls need to be wrapped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}. -In Java this is done implicitly in a process called capture conversion (as proposed in Wild FJ \cite{WildFJ}). +% % TODO intro to Featherweight Java +% is a formal model of the Java programming language reduced to a core set of instructions. +% - We extend this model by existential types and let expressions. +% - We copy this from \ref{WildFJ} but make type annotations optional +% - Our calculus is called \TamedFJ{} +% - \TamedFJ{} binds every method argument with a let statement. + +% 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. +% Let's have a look at a representation of the \texttt{add} call from the last line in listing \ref{lst:wildcardIntro} with our calculus \TamedFJ{}: +% %The \texttt{add} call in listing \ref{lst:wildcardIntro} needs to be encased by a \texttt{let} statement in our calculus. +% %This makes the capture converion explicit. +% \begin{lstlisting} +% let v : (*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$@*) = lo in v.add(new Integer(1)); +% \end{lstlisting} +% The method call is encased in a \texttt{let} statement and +% \expr{lo} is assigned to a new variable \expr{v} of \linebreak[2] +% \textbf{Existential Type} $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$. +% Our calculus uses existential types \cite{WildFJ} to formalize wildcards: +% \texttt{List} is translated to $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$ +% and \texttt{List} is expressed as $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$. +% The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound, +% and a type they are bound to. +% In this case the name is $\rwildcard{A}$ and it's bound to the the type \texttt{List}. +% Inside the \texttt{let} statement the variable \expr{v} has the type +% $\exptype{List}{\rwildcard{A}}$. +% This is an explicit version of \linebreak[2] +% \textbf{Capture Conversion}, +% which makes use of the fact that a concrete type must be behind every wildcard type. +% There is no instantiation of a \texttt{List}, +% but there exists some unknown type $\exptype{List}{\rwildcard{A}}$, with $\rwildcard{A}$ inbetween the bounds $\bot$ (bottom type, subtype of all types) and +% \texttt{Object}. +% Inside the body of the let statement \expr{v} is treated as a value with the constant type $\exptype{List}{\rwildcard{A}}$. +% Existential types enable us to formalize \textit{Capture Conversion}. +% Polymorphic method calls need to be wrapped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}. +% In Java this is done implicitly in a process called capture conversion (as proposed in Wild FJ \cite{WildFJ}). -\begin{figure} -\begin{minipage}{0.4\textwidth} -\begin{lstlisting}[caption=Java Invariance Example,label=lst:invarianceExample]{java} -List ls = ...; -List lo = ...; -lo = ls; // typing error! -lo.add(new Integer(1)); -\end{lstlisting} -\end{minipage} -\hfill -\begin{minipage}{0.5\textwidth} -\begin{lstlisting}[caption=Use-Site Variance Example,label=lst:wildcardIntro]{java} -List ls = ...; -List lo = ...; -lo = ls; // correct -lo.add(new Integer(1)); // error! -\end{lstlisting} -\end{minipage} -\end{figure} \section{Global Type Inference Algorithm} @@ -450,6 +489,9 @@ exists to satisfy $\exptype{List}{\type{A}} <: \exptype{List}{\type{X}}, \exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$. +\textbf{Solution:} +Capture Conversion during Unify. + \item \unify{} morphs a constraint set into a correct type solution gradually assigning types to type placeholders during that process.