diff --git a/constraints.tex b/constraints.tex index 99ec65b..d137dd8 100644 --- a/constraints.tex +++ b/constraints.tex @@ -9,19 +9,22 @@ %\subsection{Well-Formedness} -Constraint generation step is the same as in \cite{TIforFGJ} except for field access and method invocation. -Here \fjtype{} generates capture constraints instead of normal subtype constraints. -Subtype constraints are created according to the type rules defined in section \ref{sec:tifj}. -The \typeExpr{} function creates constraints for a given expression. +% But it can be easily adapted to Featherweight Java or Java. +% We add T <. a for every return of an expression anyway. If anything returns a Generic like X it is not directly used in a method call like X { -% % Y m(Example p){ ... } -% % } -% % \end{verbatim} - -% In Featherweight Java a method type is bound to a specific class. -% The class \texttt{Example} shown above contains one method \texttt{m}: - -% \begin{displaymath} -% \textit{mtype}({\texttt{m}, \exptype{Example}{\type{X}}}) = \generics{\type{Y}} \ \exptype{Example}{\type{Y}} \to \type{Y} -% \end{displaymath} - -% $\Pi$ is a set of method assumptions used by the $\fjtype{}$ algorithm. -% It's a map of method types to method names. -% Every method name has a set of possible types, -% because there could be more than one method with the same name in a program consisting out of multiple classes. -% To simplify the syntax of method assumptions, we add the inheriting class type to the parameter list: - -% \begin{displaymath} -% \Pi = \set{ \texttt{m} : \generics{\type{X}, \type{Y}} \ (\exptype{Example}{\type{X}}, \exptype{Example}{\type{Y}}) \to \type{Y}} -% \end{displaymath} - -% \begin{verbatim} -% class Example { } - -% Y m(Example this, Example p){ ... } -% \end{verbatim} - -\begin{displaymath} - \begin{array}{@{}l@{}l} - \typeExpr{} &({\mtypeEnvironment} , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2) = \\ - & \begin{array}{ll} - \textbf{let} - & \tv{e}, \tv{x} \ \text{fresh} \\ - & \consSet_R = \typeExpr({\mtypeEnvironment}, \expr{e}_1, \tv{e})\\ - & \constraint = - \set{ - \tv{e} \lessdot \tv{x} - }\\ - {\mathbf{in}} & { - \consSet_R \cup \set{\constraint}} \cup \typeExpr(\mtypeEnvironment \cup \set{\expr{x} : \tv{x}}) - \end{array} - \end{array} -\end{displaymath} - \begin{displaymath} \begin{array}{@{}l@{}l} \typeExpr{} &({\mtypeEnvironment} , \texttt{e}.\texttt{f}, \tv{a}) = \\ @@ -185,13 +134,27 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi \end{array} \end{displaymath} -The set of method assumptions returned by the \textit{mtypes} function is used to generate the constraints for a method call expression: - -There are two kinds of method calls. -The ones to already typed methods and calls to untyped methods. \begin{displaymath} \begin{array}{@{}l@{}l} - \typeExpr{}' & ({\mtypeEnvironment} , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\ + \typeExpr{} &({\mtypeEnvironment} , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2, \tv{a}) = \\ + & \begin{array}{ll} + \textbf{let} + & \tv{e}_1, \tv{e}_2, \tv{x} \ \text{fresh} \\ + & \consSet_1 = \typeExpr({\mtypeEnvironment}, \expr{e}_1, \tv{e}_1)\\ + & \consSet_2 = \typeExpr({\mtypeEnvironment} \cup \set{\expr{x} : \tv{x}}, \expr{e}_2, \tv{e}_2)\\ + & \constraint = + \set{ + \tv{e}_1 \lessdot \tv{x}, \tv{e}_2 \lessdot \tv{a} + }\\ + {\mathbf{in}} & { + \consSet_1 \cup \consSet_2 \cup \set{\constraint}} + \end{array} + \end{array} +\end{displaymath} + +\begin{displaymath} + \begin{array}{@{}l@{}l} + \typeExpr{} & ({\mtypeEnvironment} , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\ & \begin{array}{ll} \textbf{let} & \tv{r}, \ol{\tv{r}} \text{ fresh} \\ @@ -207,126 +170,98 @@ The ones to already typed methods and calls to untyped methods. \end{array} \end{array} \end{displaymath} - -\begin{displaymath} - \begin{array}{@{}l@{}l} - \typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a}) = \\ - & \begin{array}{ll} - \textbf{let} - & \tv{r}, \ol{\tv{r}} \text{ fresh} \\ - & \consSet_R = \typeExpr(({\mtypeEnvironment} ; - \overline{\localVarAssumption}), \texttt{e}, \tv{r})\\ - & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \ol{e}, \ol{\tv{r}}) \\ - & \begin{array}{@{}l@{}l} - \constraint = \orCons\set{ & - \begin{array}[t]{l} - [\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdotCC \exptype{C}{\ol{X}}, - \overline{\tv{r}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a}, - \ol{Y} \lessdot \ol{N} \} - \end{array}\\ - & \ |\ - (\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T}) \in - {\mtypeEnvironment} %, \, |\ol{T}| = |\ol{e}| - , \, \overline{\wtv{a}} \text{ fresh}} - \end{array}\\ - \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T}) - \end{array} - \end{array} - \end{displaymath} \\[1em] \noindent \textbf{Example:} \begin{verbatim} class Class1{ - X m(List lx, List lt){ ... } - List wGet(){ ... } - List get() { ... } + A head(List l){ ... } + List get() { ... } } class Class2{ example(c1){ - return c1.m(c1.get(), c1.wGet()); + 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, -which has lead to the given type annotations for \texttt{Class1}. -Now we call the $\fjtype{}$ function with the class \texttt{Class2} and the method assumptions for the preceeding class: +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} - \type{Class1}.\texttt{m}: \generics{\type{X} \triangleleft \type{Object}} \ - (\exptype{List}{\type{X}}, \, \wctype{\wildcard{A}{\type{X}}{\bot}}{List}{\wildcard{A}{\type{X}}{\bot}}) \to \type{X}, \\ - \type{Class1}.\texttt{wGet}: () \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\wildcard{A}{\type{Object}}{\type{String}}}, \\ - \type{Class1}.\texttt{get}: () \to \exptype{List}{\type{String}} + \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} -The result of the $\typeExpr{}$ function is the constraint set -\begin{displaymath} -C = \left\{ \begin{array}{l} -\tv{c1} \lessdot \type{Class1}, \\ -\tv{p1} \lessdot \exptype{List}{\wtv{x}}, \\ -\exptype{List}{\type{String}} \lessdot \tv{p1}, \\ -\tv{p2} \lessdot \wctype{\wildcard{A}{\wtv{x}}{\bot}}{List}{\rwildcard{A}}, \\ -\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{p2} -\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} -The first parameter of a method assumption is the receiver type $\type{T}_r$. -\texttt{Class1} for this example. -Therefore the $(\tv{c1} \lessdot \type{Class1})$ constraint. -The type variable $\tv{c1}$ is assigned to the parameter \texttt{c1} of the \texttt{example} method. +Following is a possible solution for the given constraint set: -or a simplified version: +\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} -\begin{displaymath} -C = \left\{ \begin{array}{l} -\tv{c1} \lessdot \type{Class1}, \\ -\exptype{List}{\type{String}} - \lessdot \exptype{List}{\wtv{x}}, \\ -\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} - \lessdot \wctype{\wildcard{A}{\wtv{x}}{\bot}}{List}{\rwildcard{A}} -\end{array} \right\} -\end{displaymath} +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. - -$\wtv{x}$ is a type variable we use for the generic $\type{X}$. It is flagged as a free type variable. -%TODO: Do an example where wildcards are inserted and we need capture conversion - -\unify{} returns the solution $(\sigma = \set{ \tv{x} \to \type{String} })$ - -% \\[1em] -% \noindent -% \textbf{Example:} -% \begin{verbatim} -% class Class1 { -% Pair make(List l){ ... } -% boolean compare(Pair p) { ... } - -% example(l){ -% return compare(make(l)); -% } -% } -% \end{verbatim} - -% The method call \texttt{make(l)} generates the constraints -% \begin{displaymath} -% \tv{l} \lessdot \exptype{List}{\tv{x}}, \exptype{Pair}{\tv{x}, \tv{x}} \lessdot \tv{m} -% \end{displaymath} -% with $\tv{l}$ being the type placeholder for the variable \texttt{l} -% and $\tv{m}$ is the type variable for the return type of the method call. -% $\tv{m}$ is then used as the parameter for the \texttt{compare} method: -% \begin{displaymath} -% \tv{m} \lessdot \exptype{Pair}{\tv{y}, \tv{y}} -% \end{displaymath} -% Note the conversion of the generic parameters \texttt{X} and \texttt{Y} to type variables $\tv{x}$ and $\tv{y}$. - - - -% Step 3 of the \unify{} algorithm has to look for every possible supertype of $\exptype{Pair}{\tv{x}, \tv{x}}$, -% when processing the $\exptype{Pair}{\tv{x}, \tv{x}} \lessdot \tv{m}$ constraint. +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} diff --git a/introduction.tex b/introduction.tex index 3a3d887..706e925 100644 --- a/introduction.tex +++ b/introduction.tex @@ -382,6 +382,91 @@ $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype % List m() = new List() :? new List() :? id(m()); % \end{verbatim} +\subsection{\TamedFJ{} and \letfj{}} +%LetFJ -> Output language! +%TamedFJ -> ANF transformed input langauge +%Input language only described here. It is standard Featherweight Java +% we use the transformation to proof soundness. this could also be moved to the end. +% the constraint generation step assumes every method argument to be encapsulated in a let statement. This is the way Java is doing capture conversion + +The input to our algorithm is a typeless version of Featherweight Java. +Methods are declared without parameter or return types. +We still keep type annotations for fields and generic class parameters. +This is a design choice by us, +as we consider them as data declarations which are given by the programmer. +% They are inferred in for example \cite{plue14_3b} +Note the \texttt{new} expression not requiring generic parameters, +which are also inferred by our algorithm. +The method call naturally has no generic parameters aswell. +We add the elvis operator ($\elvis{}$) to the syntax mainly to showcase applications involving wildcard types. +The syntax is described in figure \ref{fig:inputSyntax}. + + +\begin{figure} +$ +\begin{array}{lrcl} +\hline +\text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\ +\text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\ +\text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\ +\text{Type variable contexts} & \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\ +\text{Class declarations} & D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\ +\text{Method declarations} & \texttt{M} & ::= & \texttt{m}(\overline{x}) \{ \texttt{return}\ t; \} \\ +\text{Terms} & t & ::= & x \\ +& & \ \ | & \texttt{new} \ \type{C}(\overline{t})\\ +& & \ \ | & t.f\\ +& & \ \ | & t.\texttt{m}(\overline{t})\\ +& & \ \ | & t \elvis{} t\\ +\text{Variable contexts} & \Gamma & ::= & \overline{x:\type{T}}\\ +\hline +\end{array} +$ +\caption{Input Syntax}\label{fig:inputSyntax} +\end{figure} + +The output is a valid Featherweight Java program. +We use the syntax of the version introduced in \cite{WildcardsNeedWitnessProtection} +calling it \letfj{} for that it is a Featherweight Java variant including \texttt{let} statements. +Our output syntax is shown in figure \ref{fig:outputSyntax} +which is actually a subset of \letfj{}, because we omit \texttt{null} types. + +\begin{figure} +$ +\begin{array}{lrcl} +\hline +\text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\ +\text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\ +\text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\ +\text{Type variable contexts} & \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\ +\text{Class declarations} & D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\ +\text{Method declarations} & \texttt{M} & ::= & \generics{\overline{\type{X} \triangleleft \type{N}}}\type{T}\ \texttt{m}(\overline{\type{T}\ \expr{x}}) = \expr{e} \\ +\text{Terms} & \expr{e} & ::= & \expr{x} \\ +& & \ \ | & \texttt{new} \ \exptype{C}{\ol{T}}(\overline{\expr{e}})\\ +& & \ \ | & \expr{e}.f\\ +& & \ \ | & \expr{e}.\texttt{m}\generics{\ol{T}}(\overline{\expr{e}})\\ +& & \ \ | & \texttt{let}\ \expr{x} : \wcNtype{\Delta}{N} = \expr{e} \ \texttt{in} \ \expr{e}\\ +& & \ \ | & \expr{e} \elvis{} \expr{e}\\ +\text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\ +\hline +\end{array} +$ +\caption{Output Syntax}\label{fig:outputSyntax} +\end{figure} + + +The output of our type inference algorithm is a valid \letfj{} program. +Before generating constraints the input is transformed to \TamedFJ{}. +After adding the missing type annotations the resulting program is a valid \letfj{} program. +%This is shown in chapter \ref{sec:soundness} +Capture conversion is only needed for wildcard types, +but we don't know which expressions will spawn wildcard types because there are no type annotations yet. +We preemptively enclose every expression in a let statement before using it as a method argument. + +We need the let statements to deal with possible Wildcard types. + + +The syntax used in our examples is the standard Featherweight Java syntax. + \subsection{Challenges}\label{challenges} %TODO: Wildcard subtyping is infinite see \cite{TamingWildcards} @@ -414,7 +499,7 @@ it is safe to pass \texttt{"String"} for the first parameter of the function. List add(List l, A v) {} List list = ...; -add("String", list); +add(list, "String"); \end{verbatim} \end{example} @@ -460,7 +545,7 @@ class SpecialPair extends Pair{} Pair id(Pair in){ - return ...; + return in; } void receive(Pair in){} @@ -531,154 +616,121 @@ $ 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}. -\section{\TamedFJ{} and \letfj{}} -The input to our type inference algorithm is a \TamedFJ{} program. -The output is a valid \letfj{} program. -\letfj{} is defined in \cite{WildcardsNeedWitnessProtection}. -It is an extension to Featherweight Java which adds Wildcard types and let statements. -The let statements are used to explicitly apply capture conversion. - %TODO % The goal is to proof soundness in respect to the type rules introduced by \cite{aModelForJavaWithWildcards} % and \cite{WildcardsNeedWitnessProtection}. -\subsection{Capture Conversion} -The input to our type inference algorithm does not contain let statements. -Those are added after computing a type solution. -Let statements act as capture conversion and only have to be applied in method calls involving wildcard types. +% \subsection{Capture Conversion} +% The \texttt{let} statements in \TamedFJ{} act as capture conversion for wildcard types. -\begin{figure} -\begin{minipage}{0.45\textwidth} -\begin{lstlisting}[style=fgj] - List clone(List l); -example(p){ - return clone(p); -} -\end{lstlisting} - \end{minipage}% - \hfill - \begin{minipage}{0.5\textwidth} -\begin{lstlisting}[style=tfgj] -(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){ - return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in - clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*); -} -\end{lstlisting} - \end{minipage} -\caption{Type inference adding capture conversion}\label{fig:addingLetExample} - \end{figure} +% \begin{figure} +% \begin{minipage}{0.45\textwidth} +% \begin{lstlisting}[style=tfgj] +% List clone(List l); +% example(p){ +% return clone(p); +% } +% \end{lstlisting} +% \end{minipage}% +% \hfill +% \begin{minipage}{0.5\textwidth} +% \begin{lstlisting}[style=letfj] +% List clone(List l); +% (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p) = +% let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in +% clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*); +% \end{lstlisting} +% \end{minipage} +% \caption{Type inference adding capture conversion}\label{fig:addingLetExample} +% \end{figure} -Figure \ref{fig:addingLetExample} shows a let statement getting added to the typed output. -The method \texttt{clone} cannot be called with the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$. -After a capture conversion \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$ with $\rwildcard{X}$ being a free variable. -Afterwards we have to find a supertype of $\exptype{List}{\rwildcard{X}}$, which does not contain free variables -($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in this case). +% Figure \ref{fig:addingLetExample} shows a let statement getting added to the typed output. +% The method \texttt{clone} cannot be called with the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$. +% After a capture conversion \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$ with $\rwildcard{X}$ being a free variable. +% Afterwards we have to find a supertype of $\exptype{List}{\rwildcard{X}}$, which does not contain free variables +% ($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in this case). -During the constraint generation step most types are not known yet and are represented by a type placeholder. -During a methodcall like the one in the \texttt{example} method in figure \ref{fig:ccExample} the type of the parameter \texttt{p} -is not known yet. -The type \texttt{List} would be one possibility as a parameter type for \texttt{p}. -To make wildcards work for our type inference algorithm \unify{} has to apply capture conversions if necessary. +% During the constraint generation step most types are not known yet and are represented by a type placeholder. +% During a methodcall like the one in the \texttt{example} method in figure \ref{fig:ccExample} the type of the parameter \texttt{p} +% is not known yet. +% The type \texttt{List} would be one possibility as a parameter type for \texttt{p}. +% To make wildcards work for our type inference algorithm \unify{} has to apply capture conversions if necessary. -The type placeholder $\tv{r}$ is the return type of the \texttt{example} method. -One possible type solution is $\tv{p} \doteq \tv{r} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$, -which leads to: -\begin{verbatim} -List example(List p){ - return clone(p); -} -\end{verbatim} +% The type placeholder $\tv{r}$ is the return type of the \texttt{example} method. +% One possible type solution is $\tv{p} \doteq \tv{r} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$, +% which leads to: +% \begin{verbatim} +% List example(List p){ +% return clone(p); +% } +% \end{verbatim} -But by substituting $\tv{p} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in the constraint -$\tv{p} \lessdotCC \exptype{List}{\wtv{x}}$ leads to -$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$. +% But by substituting $\tv{p} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in the constraint +% $\tv{p} \lessdotCC \exptype{List}{\wtv{x}}$ leads to +% $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{x}}$. -To make this typing possible we have to introduce a capture conversion via a let statement: -$\texttt{return}\ (\texttt{let}\ \texttt{x} : \wctype{\rwildcard{X}}{List}{\rwildcard{X}} = \texttt{p}\ \texttt{in} \ -\texttt{clone}\generics{\rwildcard{X}}(x) : \wctype{\rwildcard{X}}{List}{\rwildcard{X}})$ +% To make this typing possible we have to introduce a capture conversion via a let statement: +% $\texttt{return}\ (\texttt{let}\ \texttt{x} : \wctype{\rwildcard{X}}{List}{\rwildcard{X}} = \texttt{p}\ \texttt{in} \ +% \texttt{clone}\generics{\rwildcard{X}}(x) : \wctype{\rwildcard{X}}{List}{\rwildcard{X}})$ -Inside the let statement the variable \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$ +% Inside the let statement the variable \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$ -This spawns additional problems. +% This spawns additional problems. -\begin{figure} -\begin{minipage}{0.45\textwidth} -\begin{verbatim} - List clone(List l){...} +% \begin{figure} +% \begin{minipage}{0.45\textwidth} +% \begin{verbatim} +% List clone(List l){...} -example(p){ - return clone(p); -} -\end{verbatim} - \end{minipage}% - \hfill - \begin{minipage}{0.35\textwidth} -\begin{constraintset} - \textbf{Constraints:}\\ - $ - \tv{p} \lessdotCC \exptype{List}{\wtv{x}}, \\ -\tv{p} \lessdot \tv{r}, \\ -\tv{p} \lessdot \type{Object}, -\tv{r} \lessdot \type{Object} - $ -\end{constraintset} - \end{minipage} +% example(p){ +% return clone(p); +% } +% \end{verbatim} +% \end{minipage}% +% \hfill +% \begin{minipage}{0.35\textwidth} +% \begin{constraintset} +% \textbf{Constraints:}\\ +% $ +% \tv{p} \lessdotCC \exptype{List}{\wtv{x}}, \\ +% \tv{p} \lessdot \tv{r}, \\ +% \tv{p} \lessdot \type{Object}, +% \tv{r} \lessdot \type{Object} +% $ +% \end{constraintset} +% \end{minipage} -\caption{Type inference example}\label{fig:ccExample} -\end{figure} +% \caption{Type inference example}\label{fig:ccExample} +% \end{figure} -In addition with free variables this leads to unwanted behaviour. -Take the constraint -$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ for example. -After a capture conversion from $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ to $\exptype{List}{\rwildcard{Y}}$ and a substitution $\wtv{a} \doteq \rwildcard{Y}$ -we get -$\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$. -Which is correct if we apply capture conversion to the left side: -$\exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$ -If the input constraints did not intend for this constraint to undergo a capture conversion then \unify{} would produce an invalid -type solution due to: -$\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \nless: \exptype{List}{\rwildcard{X}}$ -The reason for this is the \texttt{S-Exists} rule's premise -$\text{dom}(\Delta') \cap \text{fv}(\exptype{List}{\rwildcard{X}}) = \emptyset$. +% In addition with free variables this leads to unwanted behaviour. +% Take the constraint +% $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ for example. +% After a capture conversion from $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ to $\exptype{List}{\rwildcard{Y}}$ and a substitution $\wtv{a} \doteq \rwildcard{Y}$ +% we get +% $\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$. +% Which is correct if we apply capture conversion to the left side: +% $\exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$ +% If the input constraints did not intend for this constraint to undergo a capture conversion then \unify{} would produce an invalid +% type solution due to: +% $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \nless: \exptype{List}{\rwildcard{X}}$ +% The reason for this is the \texttt{S-Exists} rule's premise +% $\text{dom}(\Delta') \cap \text{fv}(\exptype{List}{\rwildcard{X}}) = \emptyset$. -Additionally free variables are not allowed to leave the scope of a capture conversion -introduced by a let statement. -%TODO we combat both of this with wildcard type placeholders (? flag) - -Type placeholders which are not flagged as possible free variables ($\wtv{a}$) can never hold a free variable or a type containing free variables. -Constraint generation places these standard place holders at method return types and parameter types. -\begin{lstlisting}[style=fgj] - List clone(List l); -(*@$\red{\tv{r}}$@*) example((*@$\red{\tv{p}}$@*) p){ - return clone(p); -} -\end{lstlisting} -This prevents type solutions that contain free variables in parameter and return types. -When calling a method which already has a type annotation we have to consider adding a capture conversion in form of a let statement. -The constraint $\tv{p} \lessdot \exptype{List}{\wtv{x}}$ signals the \unify{} algorithm that here a capture conversion is possible. -$\sigma(\tv{p}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, \sigma(\tv{r}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, $ is a possible solution. -But only when adding a capture conversion: -\begin{lstlisting}[style=fgj] - List clone(List l); -(*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){ - return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*); -} -\end{lstlisting} - -Capture constraints cannot be stored in a set. -$\wtv{a} \lessdotCC \wtv{b}$ is not the same as $\wtv{a} \lessdotCC \wtv{b}$. -Both constraints will end up the same after a substitution for both placeholders $\tv{a}$ and $\tv{b}$. -But afterwards a capture conversion is applied, which can generate different types on the left sides. -\begin{itemize} - \item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Y}}$ - \item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Z}}$ -\end{itemize} - -Wildcards are not reflexive. A box of type $\wctype{\rwildcard{X}}{Box}{\rwildcard{X}}$ -is able to hold a value of any type. It could be a $\exptype{Box}{String}$ or a $\exptype{Box}{Integer}$ etc. -Also two of those boxes do not necessarily contain the same type. -But there are situations where it is possible to assume that. -For example the type $\wctype{\rwildcard{X}}{Pair}{\exptype{Box}{\rwildcard{X}}, \exptype{Box}{\rwildcard{X}}}$ -is a pair of two boxes, which always contain the same type. -Inside the scope of the \texttt{Pair} type, the wildcard $\rwildcard{X}$ stays the same. \ No newline at end of file +% Capture constraints cannot be stored in a set. +% $\wtv{a} \lessdotCC \wtv{b}$ is not the same as $\wtv{a} \lessdotCC \wtv{b}$. +% Both constraints will end up the same after a substitution for both placeholders $\tv{a}$ and $\tv{b}$. +% But afterwards a capture conversion is applied, which can generate different types on the left sides. +% \begin{itemize} +% \item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Y}}$ +% \item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Z}}$ +% \end{itemize} +% +% Wildcards are not reflexive. A box of type $\wctype{\rwildcard{X}}{Box}{\rwildcard{X}}$ +% is able to hold a value of any type. It could be a $\exptype{Box}{String}$ or a $\exptype{Box}{Integer}$ etc. +% Also two of those boxes do not necessarily contain the same type. +% But there are situations where it is possible to assume that. +% For example the type $\wctype{\rwildcard{X}}{Pair}{\exptype{Box}{\rwildcard{X}}, \exptype{Box}{\rwildcard{X}}}$ +% is a pair of two boxes, which always contain the same type. +% Inside the scope of the \texttt{Pair} type, the wildcard $\rwildcard{X}$ stays the same. \ No newline at end of file diff --git a/prolog.tex b/prolog.tex index a32883c..af553a4 100755 --- a/prolog.tex +++ b/prolog.tex @@ -13,7 +13,8 @@ } \lstdefinestyle{fgj}{backgroundcolor=\color{lime!20}} \lstdefinestyle{tfgj}{backgroundcolor=\color{lightgray!20}} -\lstdefinestyle{letfj}{backgroundcolor=\color{lightgray!20}} +\lstdefinestyle{letfj}{backgroundcolor=\color{lime!20}} +\lstdefinestyle{tamedfj}{backgroundcolor=\color{yellow!20}} \lstdefinestyle{java}{backgroundcolor=\color{lightgray!20}} \newtheorem{recap}[note]{Recap} diff --git a/tRules.tex b/tRules.tex index b92f002..ff727c8 100644 --- a/tRules.tex +++ b/tRules.tex @@ -61,7 +61,7 @@ $ \hline \end{array} $ -\caption{Input Syntax}\label{fig:syntax} +\caption{\TamedFJ{} Syntax}\label{fig:syntax} \end{figure} % \begin{figure} @@ -139,15 +139,16 @@ Featherweight Java's syntax involves no \texttt{let} statement and terms can be nested freely. This is similar to Java's syntax. To convert it to \TamedFJ{} additional let statements have to be added. -This is done by a \textit{A-Normal Form} \cite{aNormalForm} transformation. - +This is done by a \textit{A-Normal Form} \cite{aNormalForm} transformation shown in figure \ref{fig:anfTransformation}. +The input of this transformation is a Featherweight Java program in the syntax given \ref{fig:inputSyntax} +and the output is a \TamedFJ{} program. \textit{Example:}\\ \noindent \begin{minipage}{0.45\textwidth} \begin{lstlisting}[style=fgj,caption=Featherweight Java] m(l, v){ - return id(l).add(v); + return l.add(v); } \end{lstlisting} \end{minipage}% @@ -155,42 +156,48 @@ m(l, v){ \begin{minipage}{0.5\textwidth} \begin{lstlisting}[style=tfgj,caption=\TamedFJ{} representation] m(l, v) = - let x = id(l) in x.add(v) - + let x1 = l in + let x2 = v in x1.add(x2) \end{lstlisting} \end{minipage} -$ -\begin{array}{|lrcl|l} -\hline -& & & \textbf{Featherweight Java Terms}\\ -\text{Terms} & t & ::= -& \expr{x} -\\ -& & \ \ | -& \texttt{new} \ \type{C}(\overline{t}) -\\ -& & \ \ | -& t.f -\\ -& & \ \ | -& t.\texttt{m}(\overline{t}) -\\ -& & \ \ | -& t \elvis{} t\\ -% -\hline -\end{array} -$ +% $ +% \begin{array}{|lrcl|l} +% \hline +% & & & \textbf{Featherweight Java Terms}\\ +% \text{Terms} & t & ::= +% & \expr{x} +% \\ +% & & \ \ | +% & \texttt{new} \ \type{C}(\overline{t}) +% \\ +% & & \ \ | +% & t.f +% \\ +% & & \ \ | +% & t.\texttt{m}(\overline{t}) +% \\ +% & & \ \ | +% & t \elvis{} t\\ +% % +% \hline +% \end{array} +% $ +\begin{figure} + \begin{center} $\begin{array}{lrcl} -\text{ANF} & \anf{\expr{x}} & = & \expr{x} \\ +%\text{ANF} +& \anf{\expr{x}} & = & \expr{x} \\ & \anf{\texttt{new} \ \type{C}(\overline{t})} & = & \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}}) \\ & \anf{t.f} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \expr{x}.f \\ & \anf{t.\texttt{m}(\overline{t})} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \expr{x}.\texttt{m}(\overline{\expr{x}}) \\ & \anf{t_1 \elvis{} t_2} & = & \anf{t_1} \elvis{} \anf{t_2} \end{array}$ +\end{center} +\caption{ANF Transformation}\label{fig:anfTransformation} +\end{figure} % $ % \begin{array}{lrcl|l} @@ -455,7 +462,7 @@ $\begin{array}{l} $\begin{array}{l} \typerule{T-Let}\\ \begin{array}{@{}c} - \Delta | \Gamma \vdash \expr{e}_1 : \type{T}_1 \quad \quad + \Delta | \Gamma \vdash \expr{t}_1 : \type{T}_1 \quad \quad \Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N} \\ \Delta, \Delta' | \Gamma, \expr{x} : \wcNtype{}{N} \vdash \expr{t}_2 : \type{T}_2 \quad \quad @@ -465,7 +472,7 @@ $\begin{array}{l} \\ \hline \vspace*{-0.3cm}\\ - \Delta | \Gamma \vdash \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2 : \type{T} + \Delta | \Gamma \vdash \texttt{let}\ \expr{x} = \expr{t}_1 \ \texttt{in} \ \expr{t}_2 : \type{T} \end{array} \end{array}$ \\[1em] @@ -508,8 +515,7 @@ $\begin{array}{l} $\begin{array}{l} \typerule{T-Class}\\ \begin{array}{@{}c} - \mathtt{\Pi}' = \mathtt{\Pi} \cup \set{ \texttt{m} : (\type{T'_m}, \ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M}} \quad \quad - \forall \texttt{m} \in \ol{M}: \Delta \vdash \exptype{C}{\ol{X}} <: \type{T'_m}\\ + \mathtt{\Pi}' = \mathtt{\Pi} \cup \set{ \texttt{m} : (\exptype{C}{\ol{X}}, \ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M}} \\ \mathtt{\Pi}'' = \mathtt{\Pi} \cup \set{ \texttt{m} : \generics{\ol{X \triangleleft \type{N}}, \ol{Y \triangleleft P}}(\exptype{C}{\ol{X}},\ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M} } \\ \triangle = \overline{\type{X} : \bot .. \type{U}} \quad \quad