diff --git a/conclusion.tex b/conclusion.tex index 4f68eb5..63c1cc1 100644 --- a/conclusion.tex +++ b/conclusion.tex @@ -1,40 +1,14 @@ -\section{Properties of the Algorithm} -\begin{itemize} - \item Our algorithm is designed for extensibility with the final goal of full support for Java. - \unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}. - Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}. - -\end{itemize} - %TODO: how are the challenges solved: Describe this in the last chapter with examples! -\section{Soundness}\label{sec:soundness} - -\begin{theorem}\label{testenv-theorem} -Type inference produces a correctly typed program. -\begin{description} - \item[If] $\fjtypeinference(\mv{\Pi}, \texttt{class}\ \exptype{C}{\ol{X} - \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \}) = \mtypeEnvironment{}'$ - \item[Then] $\texttt{class}\ \exptype{C}{\ol{X} - \triangleleft \ol{N}} \triangleleft \type{N}\ \{ \overline{\type{T} \ f};\ \ol{M} \} \text{ok}$, - with $\ol{M} = $ -\end{description} -\end{theorem} - -To prove soundness we have to show two things. -The vital parts are method calls and field access. -The generated constraints have to resemble the \TamedFJ{}'s type system. - -\section{Completeness}\label{sec:completeness} +\section{Discussion}\label{sec:completeness} We couldn't verify it with an implementation yet, but we assume atleast the same functionality as the global type inference algorithm for Featherweight Java without Wildcards \cite{TIforFGJ}. +When it comes to wildcards there is a limitation we couldn't find a good workaround: +\begin{example} This example does not work: -\begin{example} Limitation: - -This example does not work: - -\begin{minipage}{0.35\textwidth} - \begin{verbatim} +\noindent +\begin{minipage}{0.51\textwidth} + \begin{lstlisting}[style=java] class Example{ Pair make(List l){...} bool compare(Pair p){...} @@ -43,75 +17,46 @@ class Example{ return compare(make(l)); } } -\end{verbatim} +\end{lstlisting} \end{minipage}% \hfill - \begin{minipage}{0.55\textwidth} -\begin{constraintset} - \textbf{Constraints:}\\ - $ - \wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{x}}, \\ - \exptype{Pair}{\wtv{x},\wtv{x}} \lessdot \tv{r}, \\ - \tv{r} \lessdot \exptype{Pair}{\tv{z}, \tv{z}}%,\\ - %\tv{y} \lessdot \tv{m} - $\\ -\end{constraintset} + \begin{minipage}{0.48\textwidth} +\begin{lstlisting}[style=constraints] +(*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{x}}$@*), +(*@$\exptype{Pair}{\wtv{x},\wtv{x}} \lessdot \ntv{r}$@*), +(*@$\ntv{r} \lessdot \exptype{Pair}{\wtv{z}, \wtv{z}}$@*) +\end{lstlisting} \end{minipage} \end{example} -The algorithm can find a solution to every program which the Unify by Plümicke finds -a correct solution aswell. -It will not infer intermediat type like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X},\rwildcard{X}}$. -There is propably some loss of completeness when capture constraints get deleted. -This happens because constraints of the form $\tv{a} \lessdotCC \exptype{C}{\wtv{x}}$ are kept as long as possible. -Here the variable $\tv{a}$ maybe could hold a wildcard type, -but it gets resolved to a $\generics{\type{A} \triangleleft \type{N}}$. -This combined with a constraint $\type{N} \lessdot \wtv{x}$ looses a possible solution. +%The algorithm can find a solution to every program which the Unify by Plümicke finds +%a correct solution aswell. +We will not infer intermediat types like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X},\rwildcard{X}}$ +for a normal type placeholder. +$\ntv{r}$ will get the type $\wctype{\rwildcard{X},\rwildcard{Y}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$ +which renders the constraint set unsolvable. -This is our result: -\begin{verbatim} -class List { - void addTo(List l){ - l.add(this.get()); - } -} -\end{verbatim} -$ -\tv{l} \lessdotCC \exptype{List}{\wtv{y}}, -\type{X} \lessdot \wtv{y} -$ -But the most general type would be: -\begin{verbatim} -class List { - void addTo(List l){ - l.add(this.get()); - } -} -\end{verbatim} +% This is our result: +% \begin{verbatim} +% class List { +% void addTo(List l){ +% l.add(this.get()); +% } +% } +% \end{verbatim} +% $ +% \tv{l} \lessdotCC \exptype{List}{\wtv{y}}, +% \type{X} \lessdot \wtv{y} +% $ +% But the most general type would be: +% \begin{verbatim} +% class List { +% void addTo(List l){ +% l.add(this.get()); +% } +% } +% \end{verbatim} -\subsection{Discussion Pair Example} -\begin{verbatim} - Pair make(List l){ ... } - boolean compare(Pair p) { ... } - -List l; -Pair p; - -compare(make(l)); // Valid -compare(p); // Error -\end{verbatim} - -Our type inference algorithm is not able to solve this example. -When we convert this to \TamedFJ{} and generate constraints we end up with: -\begin{lstlisting}[style=tamedfj] -let m = let x = l in make(x) in compare(m) -\end{lstlisting} -\begin{constraintset}$ -\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \ntv{x}, -\ntv{x} \lessdotCC \exptype{List}{\wtv{a}} -\exptype{Pair}{\wtv{a}, \wtv{a}} \lessdot \ntv{m}, %% TODO: Mark this constraint -\ntv{m} \lessdotCC \exptype{Pair}{\wtv{b}, \wtv{b}} -$\end{constraintset} $\ntv{x}$ will get the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and from the constraint @@ -120,63 +65,74 @@ $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}} \lessdot \ntv{m}$. Finding a supertype to $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ is the crucial part. -The correct substition for $\ntv{m}$ would be $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$. +The correct substition for $\ntv{r}$ would be $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$. But this leads to additional branching inside the \unify{} algorithm and increases runtime. %We refrain from using that type, because it is not denotable with Java syntax. %Types used for normal type placeholders should be expressable Java types. % They are not! +This also just solves this specific issue and not the problem in general. -The prefered way of dealing with this example in our opinion would be the addition of a multi-let statement to the syntax. -\begin{lstlisting}[style=letfj] -let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = l, m = make(x) in compare(make(x)) -\end{lstlisting} +% The prefered way of dealing with this example in our opinion would be the addition of a multi-let statement to the syntax. -We can make it work with a special rule in the \unify{}. -But this will only help in this specific example and not generally solve the issue. -A type $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ has atleast two immediate supertypes: -$\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ and -$\wctype{\rwildcard{X}, \rwildcard{Y}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$. -Imagine a type $\exptype{Triple}{\rwildcard{X},\rwildcard{X},\rwildcard{X}}$ already has -% TODO: how many supertypes are there? -%X.Triple <: X,Y.Triple <: -%X,Y,Z.Triple +% \begin{lstlisting}[style=letfj] +% let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = l, m = make(x) in compare(make(x)) +% \end{lstlisting} -% TODO example: -\begin{lstlisting}[style=java] - Triple sameL(List l) - Triple sameP(Pair l) - void triple(Triple tr){} +% We can make it work with a special rule in the \unify{}. +% But this will only help in this specific example and not generally solve the issue. +% A type $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ has atleast two immediate supertypes: +% $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ and +% $\wctype{\rwildcard{X}, \rwildcard{Y}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$. +% Imagine a type $\exptype{Triple}{\rwildcard{X},\rwildcard{X},\rwildcard{X}}$ already has +% % TODO: how many supertypes are there? +% %X.Triple <: X,Y.Triple <: +% %X,Y,Z.Triple -Pair p ... -List l ... +% % TODO example: +% \begin{lstlisting}[style=java] +% Triple sameL(List l) +% Triple sameP(Pair l) +% void triple(Triple tr){} -make(t) { return t; } -triple(make(sameP(p))); -triple(make(sameL(l))); -\end{lstlisting} +% Pair p ... +% List l ... -\begin{constraintset} -$ -\exptype{Triple}{\rwildcard{X}, \rwildcard{X}, \rwildcard{X}} \lessdot \ntv{t}, -\ntv{t} \lessdotCC \exptype{Triple}{\wtv{a}, \wtv{b}, \wtv{b}}, \\ -(\textit{This constraint is added later: } \exptype{Triple}{\rwildcard{X}, \rwildcard{Y}, \rwildcard{Y}} \lessdot \ntv{t}) -$ -% Triple <. t -% ( Triple <. t ) <- this constraint is added later -% t <. Triple +% make(t) { return t; } +% triple(make(sameP(p))); +% triple(make(sameL(l))); +% \end{lstlisting} -% t =. x.Triple -\end{constraintset} +% \begin{constraintset} +% $ +% \exptype{Triple}{\rwildcard{X}, \rwildcard{X}, \rwildcard{X}} \lessdot \ntv{t}, +% \ntv{t} \lessdotCC \exptype{Triple}{\wtv{a}, \wtv{b}, \wtv{b}}, \\ +% (\textit{This constraint is added later: } \exptype{Triple}{\rwildcard{X}, \rwildcard{Y}, \rwildcard{Y}} \lessdot \ntv{t}) +% $ +% % Triple <. t +% % ( Triple <. t ) <- this constraint is added later +% % t <. Triple + +% % t =. x.Triple +% \end{constraintset} \section{Conclusion and Further Work} % we solved the problems given in the introduction (see examples TODO give names to examples) -The problems introduced in the openening \ref{challenges} can be solved via our \unify{} algorithm (see examples \ref{example1} and \ref{example2}). -As you can see by the given examples our type inference algorithm can calculate -type solutions for programs involving wildcards. +The problems introduced in the openening \ref{challenges} can be solved via our \unify{} algorithm. %(see examples \ref{example1} and \ref{example2}). +Additionally we could prove that type solutions generated by our type inference algorithm are correct respective to \TamedFJ{}'s type rules. +The important parts are lemma \ref{lemma:soundness} and \ref{lemma:unifySoundness}. +They prove that the \unify{} algorithm solves a constraint set according to our subtyping rules +and that the generated constraints match \TamedFJ{}'s type system. +%As you can see by the given examples our type inference algorithm can calculate +%type solutions for programs involving wildcards. -Going further we try to prove soundness and completeness for \unify{}. +The crucial parts introduced in this paper are capture constraints, wildcard placeholders and existential types. +Those data structures allow us to solve the problems introduced in chapter \ref{challenges}. +%Going further we try to prove soundness and completeness for \unify{}. +Our algorithm is designed for extensibility with the final goal of full support for Java. +\unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}. +Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}. % The tricks are: % \begin{itemize} diff --git a/constraints.tex b/constraints.tex index e5e72fd..edee927 100644 --- a/constraints.tex +++ b/constraints.tex @@ -223,98 +223,6 @@ Those type variables count as regular types and can be held by normal type place \end{array} \end{array} \end{displaymath} -\\[1em] -\noindent -\textbf{Example:} -\begin{verbatim} -class Class1{ - A head(List l){ ... } - List get() { ... } -} - -class Class2{ - example(c1){ - return c1.head(c1.get()); - } -} -\end{verbatim} -%This example comes with predefined type annotations. -We assume the class \texttt{Class1} has already been processed by our type inference algorithm -leading to the following type annotations: -%Now we call the $\fjtype{}$ function with the class \texttt{Class2} and the method assumptions for the preceeding class: -\begin{displaymath} -\mtypeEnvironment = \left\{\begin{array}{l} - \texttt{m}: \generics{\type{A} \triangleleft \type{Object}} \ - (\type{Class1},\, \exptype{List}{\type{A}}) \to \type{X}, \\ - \texttt{get}: (\type{Class1}) \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\rwildcard{A}} -\end{array} \right\} -\end{displaymath} - -At first we have to convert the example method to a syntactically correct \TamedFJ{} program. -Afterwards the the \fjtype{} algorithm is able to generate constraints. - -\begin{minipage}{0.45\textwidth} - \begin{lstlisting}[style=tamedfj] -class Class2 { - example(c1) = let x = c1 in - let xp = x.get() in x.m(xp); -} -\end{lstlisting} - \end{minipage}% - \hfill - \begin{minipage}{0.5\textwidth} -\begin{constraintset} -$ - \begin{array}{l} - \ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}, \\ - \ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}, \\ - \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{xp}, \\ - \tv{xp} \lessdotCC \exptype{List}{\wtv{a}} - \end{array} -$ - \end{constraintset} -\end{minipage} - -Following is a possible solution for the given constraint set: - -\begin{minipage}{0.55\textwidth} - \begin{lstlisting}[style=letfj] -class Class2 { - example(c1) = let x : Class1 = c1 in - let xp : (*@$\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*) = x.get() - in x.m(xp); -} -\end{lstlisting} - \end{minipage}% - \hfill - \begin{minipage}{0.4\textwidth} -\begin{constraintset} -$ - \begin{array}{l} - \sigma(\ntv{x}) = \type{Class1} \\ - %\tv{xp} \lessdot \exptype{List}{\wtv{x}}, \\ - %\exptype{List}{\type{String}} \lessdot \tv{p1}, \\ - \sigma(\tv{xp}) = \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \\ - \end{array} -$ - \end{constraintset} -\end{minipage} - -For $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$ to be a correct solution for $\tv{xp}$ -the constraint $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{a}}$ -must be satisfied. -This is possible, because we deal with a capture constraint. -The $\lessdotCC$ constraint allows the left side to undergo a capture conversion -which leads to $\exptype{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{a}}$. -Now a substitution of the wildcard placeholder $\wtv{a}$ with $\rwildcard{A}$ leads to a satisfied constraint set. - -The wildcard placeholders are not used as parameter or return types of methods. -Or as types for variables introduced by let statements. -They are only used for generic method parameters during a method invocation. -Type placeholders which are not flagged as wildcard placeholders ($\wtv{a}$) can never hold a free variable or a type containing free variables. -This practice hinders free variables to leave their scope. -The free variable $\rwildcard{A}$ generated by the capture conversion on the type $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$ -cannot be used anywhere else then inside the constraints generated by the method call \texttt{x.m(xp)}. \begin{displaymath} \begin{array}{@{}l@{}l} @@ -353,6 +261,92 @@ cannot be used anywhere else then inside the constraints generated by the method \end{array} \end{array} \end{displaymath} +\\[1em] +\noindent +\begin{example} +Given the following input program missing type annotations for the \texttt{example} method: +\begin{lstlisting}[style=java] +class Class1{ + A head(List l){ ... } + List get() { ... } +} + +class Class2{ + example(c1){ + return c1.head(c1.get()); + } +} +\end{lstlisting} +%This example comes with predefined type annotations. +We assume the class \texttt{Class1} has already been processed by our type inference algorithm +leading to the following type annotations: +%Now we call the $\fjtype{}$ function with the class \texttt{Class2} and the method assumptions for the preceeding class: +\begin{displaymath} +\mtypeEnvironment = \left\{\begin{array}{l} + \texttt{m}: \generics{\type{A} \triangleleft \type{Object}} \ + (\type{Class1},\, \exptype{List}{\type{A}}) \to \type{X}, \\ + \texttt{get}: (\type{Class1}) \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\rwildcard{A}} +\end{array} \right\} +\end{displaymath} + +At first we have to convert the example method to a syntactically correct \TamedFJ{} program. +Afterwards the the \fjtype{} algorithm is able to generate constraints. + +\noindent +\begin{minipage}{0.52\textwidth} + \begin{lstlisting}[style=tamedfj] +class Class2 { + example(c1) = let x = c1 in + let xp = x.get() in x.m(xp); +} +\end{lstlisting} + \end{minipage}% + \hfill + \begin{minipage}{0.46\textwidth} +\begin{lstlisting}[style=constraints] +(*@$\ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}$@*), +(*@$\ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}$@*), +(*@$\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{xp}$@*), +(*@$\tv{xp} \lessdotCC \exptype{List}{\wtv{a}}$@*) +\end{lstlisting} +\end{minipage} + +Following is a possible solution for the given constraint set: + +\noindent +\begin{minipage}{0.55\textwidth} + \begin{lstlisting}[style=tamedfj] +class Class2 { + example(c1) = let x :Class1 = c1 in + let xp :(*@$\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*) = x.get() + in x.m(xp); +} +\end{lstlisting} + \end{minipage}% + \hfill + \begin{minipage}{0.43\textwidth} +\begin{lstlisting}[style=constraints] +(*@$\sigma(\ntv{x}) = \type{Class1}$@*), +(*@$\sigma(\tv{xp}) = \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*) + \end{lstlisting} +\end{minipage} + +For $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$ to be a correct solution for $\tv{xp}$ +the constraint $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{a}}$ +must be satisfied. +This is possible, because we deal with a capture constraint. +The $\lessdotCC$ constraint allows the left side to undergo a capture conversion +which leads to $\exptype{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{a}}$. +Now a substitution of the wildcard placeholder $\wtv{a}$ with $\rwildcard{A}$ leads to a satisfied constraint set. +\end{example} + +The wildcard placeholders are not used as parameter or return types of methods. +Or as types for variables introduced by let statements. +They are only used for generic method parameters during a method invocation. +Type placeholders which are not flagged as wildcard placeholders ($\wtv{a}$) can never hold a free variable or a type containing free variables. +This practice hinders free variables to leave their scope. +The free variable $\rwildcard{A}$ generated by the capture conversion on the type $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$ +cannot be used anywhere else then inside the constraints generated by the method call \texttt{x.m(xp)}. % Problem: % > void t2(List l){} diff --git a/soundness.tex b/soundness.tex index 5d0e224..7a79c12 100644 --- a/soundness.tex +++ b/soundness.tex @@ -91,7 +91,7 @@ % TODO: % \end{lemma} -\begin{lemma}{Soundness:} +\begin{lemma}{Soundness:}\label{lemma:soundness} \unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct. \begin{description} \item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = (\Delta', C)$ diff --git a/tRules.tex b/tRules.tex index f9c6e18..8cbd49f 100644 --- a/tRules.tex +++ b/tRules.tex @@ -40,7 +40,7 @@ class List { \begin{minipage}{0.49\textwidth} \begin{align*} &\mathrm{\Pi} = \set{\\ -&\texttt{add} : \generics{\ol{A \triangleleft Object}}\ \exptype{List}{\type{A}},\type{A} \to \exptype{List}{\type{X}} \\ +&\texttt{add} : \generics{\type{A} \triangleleft \type{Object}}\ \exptype{List}{\type{A}},\type{A} \to \exptype{List}{\type{A}} \\ &} \end{align*} \end{minipage} diff --git a/typeinference.tex b/typeinference.tex index 66dcc9f..ce543c5 100644 --- a/typeinference.tex +++ b/typeinference.tex @@ -342,24 +342,25 @@ decline the call to \texttt{shuffle(l)}. % 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 leave 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 program: +\item \label{challenge3} +% \textbf{Free variables cannot leave 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 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 must not contain free variables (TODO) +% \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 must not contain free variables (TODO) Take the Java program in listing \ref{lst:mapExample} for example. It uses map to apply a polymorphic method \texttt{id} to every element of a list @@ -392,7 +393,8 @@ $\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}}, \exptype{List}{\wtv{x}} \lessdot \tv{z}$ stem from the body of the lambda expression \texttt{id(x)}. -\textit{For clarification:} This method call would be represented as the following expression in \letfj{}: +\textit{For clarification:} This method call would be represented as the following expression in \TamedFJ{}: + \texttt{let x1 :$\wctype{\rwildcard{A}}{List}{\rwildcard{A}}$ = x in id(x) :$\tv{z}$} The T-Let rule prevents us from using free variables created by the method call to \expr{id} @@ -403,12 +405,12 @@ the constraints. If we naively substitute $\sigma(\tv{z}) = \exptype{List}{\rwildcard{A}}$ the return type of the \texttt{map} function would be the type $\exptype{List}{\exptype{List}{\rwildcard{A}}}$, which would be unsound. -The type of \expr{l2} is the same as the one of \expr{l}: -$\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$ -\textbf{Solution:} -We solve this issue by distinguishing between wildcard placeholders -and normal placeholders and introducing them as needed. -$\ntv{z}$ is a normal placeholder and is not allowed to contain free variables. +% The type of \expr{l2} is the same as the one of \expr{l}: +% $\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$ +% \textbf{Solution:} +% We solve this issue by distinguishing between wildcard placeholders +% and normal placeholders and introducing them as needed. +% $\ntv{z}$ is a normal placeholder and is not allowed to contain free variables. \end{enumerate} diff --git a/unify.tex b/unify.tex index b14c9d6..e4e3f92 100644 --- a/unify.tex +++ b/unify.tex @@ -732,28 +732,28 @@ After a substitution all $\tv{r}$ are replaced with this new existential type. In this example a correct solution is $\sigma(\tv{u}) = \type{Object}$ and $\sigma(\tv{l}) = \bot$. Remember that the substitution for the type placeholder $\tv{r}$ is $\wctype{\wildcard{X}{\ntv{u}}{\ntv{l}}}{List}{\rwildcard{X}}$ -leading to \texttt{List} as a return type for the \texttt{someList} method after applying $\sigma$. +leading to \texttt{List} as a return type for the \texttt{someList} method after applying $\sigma$: -\begin{lstlisting} +\begin{lstlisting}[style=tamedfj] List someList(){ return new List("String") :? new List(42); } \end{lstlisting} -\subsection{Wildcard Elimination Example} -\begin{lstlisting} - List concat(List l, List l2){ ... } - someList(){ - return new List("String") :? new List(42); - } +% \subsection{Wildcard Elimination Example} +% \begin{lstlisting} +% List concat(List l, List l2){ ... } +% someList(){ +% return new List("String") :? new List(42); +% } - concat(someList(), someList()); -\end{lstlisting} +% concat(someList(), someList()); +% \end{lstlisting} -Let's add an additional method call to the previous example. -The \texttt{concat} method takes two lists of the same generic type. -\texttt{concat} cannot be invoked with two existential lists. -%TODO: Explain capture conversion +% Let's add an additional method call to the previous example. +% The \texttt{concat} method takes two lists of the same generic type. +% \texttt{concat} cannot be invoked with two existential lists. +% %TODO: Explain capture conversion %\subsection{Description} @@ -1282,46 +1282,46 @@ $ \end{figure} -\subsection{Examples} +% \subsection{Examples} -\textit{Example} of the type reduction rules in figure \ref{fig:reductionRules} with the input -$\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$ -The first step is the \rulename{Capture} rule. -%The right side of the constraint does not contain any free variables. -$\begin{array}{c} -\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}\\ -\hline %Capture -\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdotCC \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}} -\end{array}$ +% \textit{Example} of the type reduction rules in figure \ref{fig:reductionRules} with the input +% $\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$ +% The first step is the \rulename{Capture} rule. +% %The right side of the constraint does not contain any free variables. +% $\begin{array}{c} +% \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}\\ +% \hline %Capture +% \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdotCC \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}} +% \end{array}$ -\begin{NiceTabular}{l} - $\ \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$ \\ - $\nextdeduction{ - \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdotCC \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}} - } $\\ - $\nextdeduction{ - \rwildcard{X} \vdash \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}} - } $\\ - $\nextdeduction{ - \rwildcard{X} \vdash \wctype{\rwildcard{Y}}{List}{\rwildcard{Y}} \doteq \wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X} \doteq \wtv{a} - } $\\ - $\nextdeduction{ - \wildcard{X}{Object}{\type{String}} \vdash - \type{String} \lessdot \mathcolorbox{addition}{\type{String}}, \tv{a} \doteq \rwildcard{X} - } $\\ - $\nextdeduction{ - \wildcard{X}{Object}{\type{String}} \vdash - \cancel{\type{String} \lessdot \rwildcard{X}}, \tv{a} \doteq \rwildcard{X} - } $\\ - \CodeAfter - \begin{tikzpicture} - \node [right] at (2-|last) { \colorbox{white}{\rulename{Prepare}} } ; - \node [right] at (3-|last) { \colorbox{white}{\rulename{Capture}} } ; - \node [right] at (4-|last) { \colorbox{white}{\rulename{Reduce}} } ; - \node [right] at (5-|last) { \colorbox{white}{\rulename{Equals}} } ; - \node [right] at (6-|last) { \colorbox{white}{\rulename{Erase}} } ; - \end{tikzpicture} - \end{NiceTabular} +% \begin{NiceTabular}{l} +% $\ \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$ \\ +% $\nextdeduction{ +% \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdotCC \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}} +% } $\\ +% $\nextdeduction{ +% \rwildcard{X} \vdash \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}} +% } $\\ +% $\nextdeduction{ +% \rwildcard{X} \vdash \wctype{\rwildcard{Y}}{List}{\rwildcard{Y}} \doteq \wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X} \doteq \wtv{a} +% } $\\ +% $\nextdeduction{ +% \wildcard{X}{Object}{\type{String}} \vdash +% \type{String} \lessdot \mathcolorbox{addition}{\type{String}}, \tv{a} \doteq \rwildcard{X} +% } $\\ +% $\nextdeduction{ +% \wildcard{X}{Object}{\type{String}} \vdash +% \cancel{\type{String} \lessdot \rwildcard{X}}, \tv{a} \doteq \rwildcard{X} +% } $\\ +% \CodeAfter +% \begin{tikzpicture} +% \node [right] at (2-|last) { \colorbox{white}{\rulename{Prepare}} } ; +% \node [right] at (3-|last) { \colorbox{white}{\rulename{Capture}} } ; +% \node [right] at (4-|last) { \colorbox{white}{\rulename{Reduce}} } ; +% \node [right] at (5-|last) { \colorbox{white}{\rulename{Equals}} } ; +% \node [right] at (6-|last) { \colorbox{white}{\rulename{Erase}} } ; +% \end{tikzpicture} +% \end{NiceTabular} % \subsection{Capture Conversion during Unification} % % The \unify{} algorithm applies a capture conversion when needed. @@ -1374,48 +1374,48 @@ $\begin{array}{c} % \end{itemize} -\subsection{Completeness}\label{sec:completeness} -It is not possible to create all super types of a type. -The General rule only creates the ones expressable by Java syntax, which still are infinitly many in some cases \cite{TamingWildcards}. -%thats not true. it can spawn X^T_T2.List where T and T2 are types and we need to choose one inbetween them -Otherwise the algorithm could generate more solutions, but they have to be filterd out afterwards, because they cannot be translated into Java. +% \subsection{Completeness}\label{sec:completeness} +% It is not possible to create all super types of a type. +% The General rule only creates the ones expressable by Java syntax, which still are infinitly many in some cases \cite{TamingWildcards}. +% %thats not true. it can spawn X^T_T2.List where T and T2 are types and we need to choose one inbetween them +% Otherwise the algorithm could generate more solutions, but they have to be filterd out afterwards, because they cannot be translated into Java. -\letfj{} is not able to represent all Java programs. %TODO: this makes ist impossible for our algorithm to be complete on Java +% \letfj{} is not able to represent all Java programs. %TODO: this makes ist impossible for our algorithm to be complete on Java -%Loss of completeness: -% a <. b, b +% %Loss of completeness: +% % a <. b, b -% Example -\begin{lstlisting} -m(l){ - return let x = l in x.add(1); -} -\end{lstlisting} -Here generality is lost. -Constraints: $\ntv{l} \lessdot \ntv{x}, \ntv{x} \lessdotCC \exptype{List}{\wtv{x}}$ +% % Example +% \begin{lstlisting} +% m(l){ +% return let x = l in x.add(1); +% } +% \end{lstlisting} +% Here generality is lost. +% Constraints: $\ntv{l} \lessdot \ntv{x}, \ntv{x} \lessdotCC \exptype{List}{\wtv{x}}$ -Correct solution would be: -\begin{lstlisting} -m(List l){ - return let x = l in x.add(1); -} -\end{lstlisting} +% Correct solution would be: +% \begin{lstlisting} +% m(List l){ +% return let x = l in x.add(1); +% } +% \end{lstlisting} -Our solution: -\begin{lstlisting} - m(X l){ - return let x = l in x.add(1); -} -m(List) -\end{lstlisting} -$\tv{a} \lessdotCC \type{T}$ constraints allow for existential types on the left side, -because there will be a capture conversion. -We do not cover this and only apply capture conversion when the left side is known. -So $\tv{a}$ will not be assigned a existential type, which explains our less general solution. +% Our solution: +% \begin{lstlisting} +% m(X l){ +% return let x = l in x.add(1); +% } +% m(List) +% \end{lstlisting} +% $\tv{a} \lessdotCC \type{T}$ constraints allow for existential types on the left side, +% because there will be a capture conversion. +% We do not cover this and only apply capture conversion when the left side is known. +% So $\tv{a}$ will not be assigned a existential type, which explains our less general solution. -If all of the program is given this may be not much of an issue. -The $\tv{a} \lessdotCC \type{T}$ constraint is kept until the end and if the method -is called and $\tv{a}$ gets a type, then this type can be an existential type aswell. +% If all of the program is given this may be not much of an issue. +% The $\tv{a} \lessdotCC \type{T}$ constraint is kept until the end and if the method +% is called and $\tv{a}$ gets a type, then this type can be an existential type aswell. % Problem: There are infinite subtypes to a type Pair when capture conversion is allowed