diff --git a/introduction.tex b/introduction.tex index 23aae89..3f357a0 100644 --- a/introduction.tex +++ b/introduction.tex @@ -282,6 +282,40 @@ lo.add(new Integer(1)); // error! \section{Global Type Inference Algorithm} +\begin{figure}[h] +\begin{minipage}{0.49\textwidth} +\begin{lstlisting}[style=tfgj, caption=Valid Java program, label=lst:addExample] + List add(List l, A v) + +List l = ...; +add(l, "String"); +\end{lstlisting} +\end{minipage}\hfill +\begin{minipage}{0.49\textwidth} +\begin{lstlisting}[style=tamedfj, caption=\TamedFJ{} representation, label=lst:addExampleLet] + List add(List l, A v) +List l = ...; +let v:(*@$\tv{v}$@*) = l + in add(v, "String"); +\end{lstlisting} +\end{minipage}\\ +\begin{minipage}{0.49\textwidth} +\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:addExampleCons] +(*@$\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}} \lessdot \tv{v}$@*) +(*@$\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$@*) +(*@$\type{String} \lessdot \wtv{a}$@*) +\end{lstlisting} +\end{minipage}\hfill +\begin{minipage}{0.49\textwidth} +\begin{lstlisting}[style=letfj, caption=Type solution, label=lst:addExampleSolution] + List add(List l, A v) +List l = ...; +let l2:(*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = l + in add(l2, "String"); +\end{lstlisting} +\end{minipage} +\end{figure} + % \begin{description} % \item[input] \tifj{} program % \item[output] type solution @@ -298,11 +332,32 @@ which introduces a let statement defining a new variable \texttt{v}. Afterwards constraints are generated \ref{lst:addExampleCons}. During the constraint generation step the type of the variable \texttt{v} is unknown and given the type placeholder $\tv{v}$. -Due to the call to the method \texttt{add} it is clear that \texttt{v} has to be a subtype of -any kind of \texttt{List} resulting in the constraint $\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$. +The methodcall to \texttt{add} spawns the constraint $\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$. Here we introduce a capture constraint ($\lessdotCC$) %a new type of subtype constraint expressing that the left side of the constraint is subject to a capture conversion. -%Additionally we use a wildcard placeholder $\wtv{a}$ as a type parameter for \texttt{List}. +At the start of our global type inference algorithm no types are assigned yet. +During the course of \unify{} - our unification algorithm used to solve the generated constraint set (see chapter \ref{sec:unify})- more and more types emerge. +As soon as a concrete type for $\tv{v}$ is given \unify{} can conduct a capture conversion if needed. +%The constraints where this is possible are marked as capture constraints. +In this example $\tv{v}$ will be set to $\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$ leaving us with the following constraints: + +\begin{displaymath} +\prftree[r]{Capture}{ +\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}, \, \type{String} \lessdotCC \wtv{a} +}{ +\wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a} +} +\end{displaymath} + +%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})$ +The constraint $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$ +allows \unify{} to do a capture conversion to $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$. +The captured wildcard $\rwildcard{X}$ gets a fresh name and is stored in the wildcard environment of the \unify{} algorithm. +Leaving us with the solution $\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$, $\type{String} \lessdot \rwildcard{Y}$ +The constraint $\type{String} \lessdot \rwildcard{Y}$ is satisfied +because $\rwildcard{Y}$ has $\type{String}$ as lower bound. + A correct Featherweight Java program including all type annotations and an explicit capture conversion via let statement is shown in listing \ref{lst:addExampleSolution}. This program can be deducted from the type solution of our \unify{} algorithm presented in chapter \ref{sec:unify}. @@ -326,43 +381,6 @@ a type parameter to method call \texttt{add(v, "String")}. % There are no informal parts in our \unify{} algorithm. % It solely consist out of transformation rules which are bound to simple checks. - -%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] -\begin{minipage}{0.49\textwidth} -\begin{lstlisting}[style=tfgj, caption=Valid Java program, label=lst:addExample] - List add(List l, A v) - -List l = ...; -add(l, "String"); -\end{lstlisting} -\end{minipage}\hfill -\begin{minipage}{0.49\textwidth} -\begin{lstlisting}[style=tamedfj, caption=\TamedFJ{} representation, label=lst:addExampleLet] - List add(List l, A v) -List l = ...; -let v:(*@$\tv{v}$@*) = l - in add(v, "String"); -\end{lstlisting} -\end{minipage}\\ -\begin{minipage}{0.49\textwidth} -\begin{lstlisting}[style=constraints, caption=Constraints, label=lst:addExampleCons] -(*@$\tv{v} \lessdot \wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$@*) -(*@$\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$@*) -(*@$\type{String} \lessdot \wtv{a}$@*) -\end{lstlisting} -\end{minipage}\hfill -\begin{minipage}{0.49\textwidth} -\begin{lstlisting}[style=letfj, caption=Type solution, label=lst:addExampleSolution] - List add(List l, A v) -List l = ...; -let l2:(*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = l - in add(l2, "String"); -\end{lstlisting} -\end{minipage} -\end{figure} - 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}}}$. @@ -409,36 +427,6 @@ 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} -$\begin{array}{c} -\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}, \, \type{String} \lessdotCC \wtv{a} -\\ -\hline -\textit{Capture Conversion:}\ \wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a} -\\ -\hline -\textit{Solution:}\ \wtv{a} \doteq \rwildcard{Y} \implies \wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}, \, \type{String} \lessdot \rwildcard{Y} -\end{array} -$ -\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}}$. -The captured wildcard $\rwildcard{X}$ gets a fresh name and is stored in the wildcard environment of the \unify{} algorithm. - - -\textit{Note:} The constraint $\type{String} \lessdot \rwildcard{Y}$ is satisfied -because $\rwildcard{Y}$ 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} @@ -516,17 +504,10 @@ $\exptype{List}{\type{A}} <: \exptype{List}{\type{X}}, % is solved by removing the wildcard $\rwildcard{X}$ if possible. \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 head(List 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. - +The example in \ref{lst:addExample} needs to be solvable. +Here a capture conversion during the unification step of our algorithm has to be conducted. +Otherwise the \texttt{add} method is not callable with the existential type +$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$. \item \textbf{Free Variables cannot leaver their scope}: