From a98c4b04862fda442e0a78f466b9554e80dd88af Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Wed, 24 Jul 2024 21:24:11 +0200 Subject: [PATCH 01/11] Soundness e.f WIP --- constraints.tex | 2 +- soundness.tex | 37 ++++++++++++++++++++++--------------- 2 files changed, 23 insertions(+), 16 deletions(-) diff --git a/constraints.tex b/constraints.tex index edee927..75a7e43 100644 --- a/constraints.tex +++ b/constraints.tex @@ -175,7 +175,7 @@ Those type variables count as regular types and can be held by normal type place \orCons\set{ \set{ & \tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}} , - [\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} , + \tv{a} \doteq [\overline{\wtv{a}}/\ol{X}]\type{T}, \ol{\wtv{a}} \lessdot [\overline{\wtv{a}}/\ol{X}]\ol{N} } \\ & \quad \mid \mv{T}\ \mv{f} \in \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots} diff --git a/soundness.tex b/soundness.tex index c076b44..24b3581 100644 --- a/soundness.tex +++ b/soundness.tex @@ -141,27 +141,34 @@ that suffices the T-Let and T-Field type rules. The case where no capture conversion is needed, because $\Delta' = \emptyset$, is trivial. Here the Let statement can be skipped entirely. We investigate the case $\sigma(\tv{x}) = \wcNtype{\Delta}{N}$. %Constraints t1 <. x, x <. C, T <. t2 -Let $\type{T}_1 = \wcNtype{\Delta'}{N} = \sigma(\tv{x})$, $\sigma(\tv{t_1}) = \type{T}_1$ then +Let $\type{T}_1 = \wcNtype{\Delta'}{N} = \sigma(\tv{x})$, $\sigma(\tv{t_1}) = \type{T}_1$, +$\sigma(\tv{a}) = \type{T}_2$ then \begin{itemize} \item $\Delta | \Gamma \vdash t_1 : \type{T}_1$ by assumption \item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ by constraint $\tv{t_1} \lessdot \tv{x}$ and lemma \ref{lemma:unifySoundness} \item $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_2$ -$\Delta | \Gamma \vdash \expr{x} : \type{N}$ by T-Var, -$\Delta, \Delta', \overline{\Delta} \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$ -and lemma \ref{lemma:unifySoundness}. -The environment $\overline{\Delta}$ is not needed, because of lemma \ref{lemma:unifyNoFreeVariablesInSupertype}: -$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ - -% The constraint a =. [a?/X]T finishes this case - -%TODO: WIP - -We know $\type{T}_2 f \in \text{fields}(\type{N})$ because - - -\item $\Delta, \Delta' | \Gamma \vdash t_1 : \type{T}_1$ by lemma \ref{lemma:unifySoundness} and the constraint $\tv{t_1} \lessdot \tv{x}$ +First we can say $\Delta | \Gamma \vdash \expr{x} : \type{N}$ by T-Var. +%$\Delta, \Delta', \overline{\Delta} \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$ +%and lemma \ref{lemma:unifySoundness}. +%The environment $\overline{\Delta}$ is not needed, because of lemma \ref{lemma:unifyNoFreeVariablesInSupertype}: +%$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ +%by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$ +%and lemmas \ref{lemma:unifySoundness} and \ref{lemma:unifyNoFreeVariablesInSupertype}. +By lemma \ref{lemma:unifyWellFormedness} and WF-Var we can deduct +$\text{fv}(\wcNtype{\Delta'}{N}) \subseteq \Delta$ +and by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$ +and lemmas \ref{lemma:unifySoundness} and \ref{lemma:unifyNoFreeVariablesInSupertype} +we can finally say +$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$. +With the constraint $\tv{a} \doteq [\ol{\wtv{a}}/\ol{X}]\type{T}$ +and $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) \in \text{fields}(\sigma(\exptype{C}{\ol{\wtv{a}}}))$ by F-Class +we proof $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_2$. +\item $\Delta, \Delta' \vdash \type{T}_2 <: \type{T}$ by constraint %TODO: Rename constraints \end{itemize} +% method call: a1 , a2 , a3 Date: Thu, 25 Jul 2024 10:36:53 +0200 Subject: [PATCH 02/11] Soundness --- soundness.tex | 27 ++++++++++++++++++++++----- 1 file changed, 22 insertions(+), 5 deletions(-) diff --git a/soundness.tex b/soundness.tex index 24b3581..d4577dc 100644 --- a/soundness.tex +++ b/soundness.tex @@ -1,5 +1,14 @@ \section{Soundness} +The differenciation of wildcard placeholders and normal type placeholders is vital for the soundness proof. +During a let statement the environment $\Delta$ is extended by capture converted wildcards, +but only for the scope of the body of the let statement. +The capture converted wildcards must not be used outside of the let statement. +This is ensured by two things: +The first is lemma \ref{lemma:freeVariablesOnlyTravelOneHop} which ensures that free variables only +travel one hop at the time through a constraint set. +And the second one is the fact that normal type placeholders never contain free variables. + % \begin{lemma} % A sound TypelessFJ program is also sound under LetFJ type rules. % \begin{description} @@ -150,14 +159,14 @@ $\sigma(\tv{a}) = \type{T}_2$ then First we can say $\Delta | \Gamma \vdash \expr{x} : \type{N}$ by T-Var. %$\Delta, \Delta', \overline{\Delta} \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$ %and lemma \ref{lemma:unifySoundness}. -%The environment $\overline{\Delta}$ is not needed, because of lemma \ref{lemma:unifyNoFreeVariablesInSupertype}: +%The environment $\overline{\Delta}$ is not needed, because of lemma \ref{lemma:freeVariablesOnlyTravelOneHop}: %$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ %by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$ -%and lemmas \ref{lemma:unifySoundness} and \ref{lemma:unifyNoFreeVariablesInSupertype}. +%and lemmas \ref{lemma:unifySoundness} and \ref{lemma:freeVariablesOnlyTravelOneHop}. By lemma \ref{lemma:unifyWellFormedness} and WF-Var we can deduct $\text{fv}(\wcNtype{\Delta'}{N}) \subseteq \Delta$ and by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$ -and lemmas \ref{lemma:unifySoundness} and \ref{lemma:unifyNoFreeVariablesInSupertype} +and lemmas \ref{lemma:unifySoundness} and \ref{lemma:freeVariablesOnlyTravelOneHop} we can finally say $\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$. With the constraint $\tv{a} \doteq [\ol{\wtv{a}}/\ol{X}]\type{T}$ @@ -167,7 +176,7 @@ we proof $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_ \end{itemize} % method call: a1 , a2 , a3 Date: Fri, 26 Jul 2024 01:31:15 +0200 Subject: [PATCH 03/11] Big Cleanup (delete comments in soundness proof --- soundness.tex | 188 +++----------------------------------------------- 1 file changed, 11 insertions(+), 177 deletions(-) diff --git a/soundness.tex b/soundness.tex index d4577dc..32ef3b7 100644 --- a/soundness.tex +++ b/soundness.tex @@ -9,97 +9,6 @@ The first is lemma \ref{lemma:freeVariablesOnlyTravelOneHop} which ensures that travel one hop at the time through a constraint set. And the second one is the fact that normal type placeholders never contain free variables. -% \begin{lemma} -% A sound TypelessFJ program is also sound under LetFJ type rules. -% \begin{description} -% \item[if:] -% $\Gamma | \Delta \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \ \text{in}\ C \text{with} \ \generics{\ol{Y \triangleleft P}}$ -% \end{description} -% \end{lemma} - -% TODO: Beforehand we have to show that $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$ -% Here $\Delta$ does not contain every $\overline{\Delta}$ ever created. -% %what prevents a free variable to emerge in \Delta.N example Y^Object |- C <: X^Y.C -% % if the Y is later needed for an equals: same(id(x), x2) -% Free wildcards do not move inwards. We can show that every new type is either well-formed and therefore does not contain any free variables. -% Or it is a generic method call: is it possible to use any free wildcards here? -% let empty - -% Box empty() -% same(Box, empty()) -% let p1 : X.Box = Box in let -% X.Box <. Box -% Box <. Box - -% boxin(empty()), Box2 - -% Where can a problem arise? When we use free wildcards before they are freed. -% But we can always CC them first. Exception two types: X.Pair and Y.Pair -% Here y = Y and x = X but - -% void same(Pair a, Pair b){} -% Pair left() { return null; } -% Pair right() { return null; } - -% Box id(Box> x) -% here it could be beneficial to use a free wildcard as the parameter X to have it later -% Box x = ... -% same(id(x), id(x)) <- this will be accepted by TI - -% let left : X,Y.Pair = left() in -% let right : Pair = right() in - -% Compromise: -% - Generate constraints so that they comply with LetFJ -% - Propose a version which is close to Java - -% Version for LetFJ: -% Is it still possible to do the capture conversion in form of constraints? -% X.C <. C -% T <. X.C -% how to proof: X.C ok - - -% If $\Delta \cup \overline{\Delta} | \Theta \vdash \texttt{e} : \type{T} \mid \overline{\Delta}$ -% then there exists a $|\texttt{e}|$ with $\Delta | \Theta \vdash |\texttt{e}| : \wcNtype{\Delta'}{N}$ in LetFJ. -% This is possible by starting with the parameter types as the base case $\overline{\Delta} = \emptyset$. - - -% Each type $\wcNtype{\Delta'}{N}$ can only use wildcards already freed. - -% \textit{Proof} by structural induction. -% \begin{description} -% \item[$\texttt{e} = \texttt{x}$] $\Delta | \Theta \vdash \texttt{e} : \type{T} \mid \emptyset$ -% $\Delta \vdash \type{T} \ \ok$ by \rulename{T-Method} -% and therefore $\Delta | \Theta \vdash \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$. - -% $|\texttt{x}, \texttt{e}| = \texttt{let}\ \texttt{e} : \type{T} = \texttt{x in } \texttt{e}$ - -% \item[$\texttt{e} = \texttt{e}.\texttt{m}(\ol{e})$] there must be atleast one value in $\texttt{e}$ or $\ol{e}$ -% \item[$\texttt{e}.f$] given let x : T = e' in x -% let x : T = e' in let xf = x.f in xf - -% Required: -% $ \Delta | \Theta \vdash e' : \type{T}_1$ -% $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ -% $\Delta, \Delta' | \Theta, x : \type{N} \vdash let xf = x.f in xf : \type{T}_2$ - -% \end{description} - - -% \textbf{Proof:} Every program complying with our type rules can be converted to a correct LetFJ program. -% First we convert the program so that every wildcards used in an expression are in the $\Delta$ environment: -% m(p) = e => let xp = p in [xp/p]e -% x1.m(x2) => let xm = x1.m(x2=) in xm -% x.f => let xf = x.f in xf -% Then we have to proof there is never a wildcard used before it is declared. -% Wildcards are introduced by the capture conversions and nothing else. - - -% \begin{lemma}{Well-formedness:} -% TODO: -% \end{lemma} - \unify{} calculates solutions for all normal type placeholders. Those are used for all untyped method's argument and return type. A correct typing for method calls can be deducted from those type informations. @@ -108,28 +17,9 @@ A correct typing for method calls can be deducted from those type informations. \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)$ - and $(\Delta_u, \sigma) = \unify{}(\Delta', C)$ % and let $\Delta= \Delta_u \cup \Delta'$ -% $\Delta, \Delta' \vdash $ -% , with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } }$ -% and $\vdash \ol{L} : \mtypeEnvironment{}$ -% and $\Gamma \subseteq \mtypeEnvironment{}$ -% \item[given] a $(\Delta, \sigma)$ with $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$ -% and there exists a $\Delta'$ with $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T'})}$ - %\item[then] there is a completion $|\texttt{e}|$ with $\Delta|\Gamma \vdash |\texttt{e}| : \sigma(\tv{a})$ \item[then] $\Delta|\Gamma \vdash \texttt{e} : \sigma(\tv{a})$ where $\Delta = \Delta_u \cup \Delta'$ \end{description} \end{lemma} -% Regular type placeholders represent type annotations. -% These are the only types a \wildFJ{} program needs to be correctly typed. -% The type placeholders flagged as wildcard placeholders are intermediate types -% used in let statements and as type parameters for generic method calls. - -%Unify needs to return S aswell and guarantee that the \Delta' environment are the wildcards -% only used inside the constraint the wildcard variable occurs -% should Unify also return the \Delta' environment? Otherwise the bounds of free wildcard variables are lost - -% Or is it possible to deduct the right \ol{S} directly from the types in the normal TPHs? - \textit{Proof:} By structural induction over the expression $\texttt{e}$. \begin{description} @@ -175,14 +65,6 @@ we proof $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_ \item $\Delta, \Delta' \vdash \type{T}_2 <: \type{T}$ by constraint %TODO: Rename constraints \end{itemize} -% method call: a1 , a2 , a3 <. List - % $\sigma(\ol{\tv{r}}) = \overline{\wcNtype{\Delta}{N}}$, - % $\ol{N} <: [\ol{S}/\ol{X}]\ol{U}$, - % TODO: S ok? We could proof $\Delta, \Delta' \overline{\Delta} \vdash \ol{S} \ \ok$ - % by proving every substitution in Unify is ok aslong as every type in the inputs is ok - % S ok when all variables are in the environment and every L <: U and U <: Class-bound - % This can be given by the constraints generated. We can proof if T ok and S <: T and T <: S' then S ok and S' ok - - % If S ok and T <. S , then Unify generates a T ok - - % S typeinference: - % T <: [S/Y]U - % We apply the following lemma - % Lemma - % if T ok and T <: S then S ok - - % until - % T = [S/Y]U - - % and then we can say by - % Lemma: - % If [S/Y]U ok then S ok (TODO: proof!) - - % So we do not have to proof S ok (but T) - - % % T_r <: C (S is in T) - % % Is C ok? - % % if every type environment \Delta supplied to Unify is ok (L <: U), then \sigma(a) = \Delta'.N implies \Delta' conforms to (L <: U) - % % this together with the X <. N constraints proofs T_r ok - - % $\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{N} \ \ok$ %TODO - % %Easy, because unify only generates substitutions for normal type placeholders which are OK \item[$\text{let}\ \expr{x} = \expr{e} \ \text{in}\ \text{let}\ \overline{\expr{x} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x})$] generates constraints $\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}}, \tv{r} \lessdot \tv{a}, \ol{\tv{x}} \lessdotCC \ol{T}, \type{T} \lessdot \tv{r}, \ol{\wtv{b}} \lessdot \ol{N}$. -We need to proof $\text{let}\ \expr{x} : \wcNtype{\Delta'}{N} = \expr{e}, \, -\overline{\expr{x} : \wcNtype{\Delta'}{N} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x}) : \type{T}_2$ -where $\sigma(\tv{x}) = \wcNtype{\Delta'}{N}$, $\sigma(\ol{\tv{x}}) = \ol{\wcNtype{\Delta'}{N}}$, $\sigma(\tv{a}) = \type{T}_2$. - +%We need to proof $\text{let}\ \expr{x} : \wcNtype{\Delta'}{N} = \expr{e}, \, +%\overline{\expr{x} : \wcNtype{\Delta'}{N} = \expr{e}} \ \text{in}\ \texttt{x}.\texttt{m}(\ol{x}) : \type{T}_2$ +%where $\sigma(\tv{x}) = \wcNtype{\Delta'}{N}$, $\sigma(\ol{\tv{x}}) = \ol{\wcNtype{\Delta'}{N}}$, $\sigma(\tv{a}) = \type{T}_2$. +We omit the case where a capture conversion is not needed and +assume $\sigma(\tv{x}) = \wcNtype{\Delta'}{N}$, $\sigma(\ol{\tv{x}}) = \ol{\wcNtype{\Delta'}{N}}$. +We have to show T-Let and T-Call which leaves us with: +\begin{itemize} + \item $\Delta | \Gamma \vdash \expr{e} : \sigma(\tv{e})$ and $\Delta | \Gamma \vdash \overline{\expr{e} : \sigma(\tv{e})}$ by assumption + \item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ and $\Delta \vdash \overline{\type{T}_1 <: \wcNtype{\Delta'}{N}}$ by constraints $\tv{e} \lessdot \tv{x}$, $\overline{\tv{e} \lessdot \tv{x}}$ and lemma \ref{lemma:unifySoundness} + \item $\Delta, \Delta', \ol{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash $ +\end{itemize} \item[$\texttt{v}.\texttt{m}(\ol{v})$] Proof is analog to field access, except the $\Delta \vdash \ol{S}\ \ok$ premise. We know that $\unify{}(\Delta, [\overline{\wtv{b}}/\ol{Y}]\set{ From c75f0c1ace1cd6461fdedd052e50393f574e9438 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Mon, 29 Jul 2024 14:09:22 +0200 Subject: [PATCH 04/11] Rebuttal --- rebuttal.md | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 rebuttal.md diff --git a/rebuttal.md b/rebuttal.md new file mode 100644 index 0000000..9c04b7e --- /dev/null +++ b/rebuttal.md @@ -0,0 +1,11 @@ +Thank you very much for your in depth reviews. We submitted the paper in an early stage to get early feedback and we'd appreciate the chance to submit a revised version. We are already working on the shortcomings you exposed in your reviews. + +A prototype implementation of the type inference algorithm is currently in development. We expect to use the prototype to explore the boundaries of what the algorithm is capable of. In the next revision of the paper we will report positive and negative examples as well as measurements of the algorithm's runtime. + +We plan to address the following points before submitting the revision: +* Implementation of the algorithm and a showcase of working use cases. +* Reworked and detailed soundness proof. +* Provide better explanations and examples on constraint generation. +* Fix typos, errors, ambiguous explanations, etc.. +* Discussion of the algorithm's complexity, our minimal aim is NP-Hardness, but we will try to draw comparisons to similar algorithms like the ones from Plümicke or Stadelmeier already mentioned in the paper. +* A discussion on completeness and why a complete type inference algorithm for Java is not possible. From 550bc384e519bd2ca01e67c172aca89905937e55 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Tue, 30 Jul 2024 12:03:37 +0200 Subject: [PATCH 05/11] Work on Soundness --- soundness.tex | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/soundness.tex b/soundness.tex index 32ef3b7..23160c5 100644 --- a/soundness.tex +++ b/soundness.tex @@ -86,7 +86,12 @@ We have to show T-Let and T-Call which leaves us with: \begin{itemize} \item $\Delta | \Gamma \vdash \expr{e} : \sigma(\tv{e})$ and $\Delta | \Gamma \vdash \overline{\expr{e} : \sigma(\tv{e})}$ by assumption \item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ and $\Delta \vdash \overline{\type{T}_1 <: \wcNtype{\Delta'}{N}}$ by constraints $\tv{e} \lessdot \tv{x}$, $\overline{\tv{e} \lessdot \tv{x}}$ and lemma \ref{lemma:unifySoundness} - \item $\Delta, \Delta', \ol{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash $ + \item $\Delta, \Delta', \ol{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash \expr{x}.\texttt{m}(\ol{x}) : \sigma(\tv{r})$ by T-Call, because the following promises are satisfied + \begin{itemize} + \item $\generics{\ol{X} \triangleleft \ol{U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m})$ is given, otherwise the program fails at the constraint generation step. + \item $\Delta \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$ by constraints $\ol{\wtv{b}} \lessdot \ol{N}$ and lemma \ref{lemma:unifySoundness} + TODO: does not work because left side is a wildcard variable (maybe just change lemma soundness a bit) + \end{itemize} \end{itemize} \item[$\texttt{v}.\texttt{m}(\ol{v})$] Proof is analog to field access, except the $\Delta \vdash \ol{S}\ \ok$ premise. From 454cbab6db5ee2685542a79df0806d4e1fd0e536 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Fri, 2 Aug 2024 01:10:46 +0200 Subject: [PATCH 06/11] Start variables keep in scope lemma --- soundness.tex | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/soundness.tex b/soundness.tex index 23160c5..3192f93 100644 --- a/soundness.tex +++ b/soundness.tex @@ -156,6 +156,12 @@ We have to show T-Let and T-Call which leaves us with: \end{description} +\begin{lemma} + Free variables never leave their scope. + If $\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}}, + \tv{r} \lessdot \tv{a}$ % TODO +\end{lemma} + % \begin{lemma} Unify does add free variables to types not containing free variables (or wildcard placeholders) % \begin{description} % \item[If] $(\sigma, \Delta) = \unify{}( \Delta', C )$ From eb05d04ae851e5d7eedb9684c37074e7d2cefa67 Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Sun, 4 Aug 2024 22:06:02 +0200 Subject: [PATCH 07/11] Fix --- soundness.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/soundness.tex b/soundness.tex index 3192f93..d4811d8 100644 --- a/soundness.tex +++ b/soundness.tex @@ -86,10 +86,10 @@ We have to show T-Let and T-Call which leaves us with: \begin{itemize} \item $\Delta | \Gamma \vdash \expr{e} : \sigma(\tv{e})$ and $\Delta | \Gamma \vdash \overline{\expr{e} : \sigma(\tv{e})}$ by assumption \item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ and $\Delta \vdash \overline{\type{T}_1 <: \wcNtype{\Delta'}{N}}$ by constraints $\tv{e} \lessdot \tv{x}$, $\overline{\tv{e} \lessdot \tv{x}}$ and lemma \ref{lemma:unifySoundness} - \item $\Delta, \Delta', \ol{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash \expr{x}.\texttt{m}(\ol{x}) : \sigma(\tv{r})$ by T-Call, because the following promises are satisfied + \item $\Delta, \Delta', \overline{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash \expr{x}.\texttt{m}(\ol{x}) : \sigma(\tv{r})$ by T-Call, because the following promises are satisfied \begin{itemize} \item $\generics{\ol{X} \triangleleft \ol{U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m})$ is given, otherwise the program fails at the constraint generation step. - \item $\Delta \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$ by constraints $\ol{\wtv{b}} \lessdot \ol{N}$ and lemma \ref{lemma:unifySoundness} + \item $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$ by constraints $\ol{\wtv{b}} \lessdot [\ol{\wtv{b}}/\ol{X}]\ol{N}$ and lemma \ref{lemma:unifySoundness} TODO: does not work because left side is a wildcard variable (maybe just change lemma soundness a bit) \end{itemize} \end{itemize} From 563690dcedf1fdde6b203953f030eb2e1ee8d92b Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Thu, 8 Aug 2024 22:46:19 +0200 Subject: [PATCH 08/11] Start Constraint generation using implication rules --- constraints.tex | 107 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 107 insertions(+) diff --git a/constraints.tex b/constraints.tex index 75a7e43..489db36 100644 --- a/constraints.tex +++ b/constraints.tex @@ -348,6 +348,113 @@ 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)}. +\subsection{Examples} + + +% v.m(v, v.f, this.id(v)); + +% let x1 = v, x2 = v, x3 = v.f, x4 = |this.id(v)| in x1.m(x2, x3, x4) + +\begin{lstlisting}{java} +class Id{ + X id(X x){ return x; } +} + +class List { + List concat(List l){ ... } +} + +class CExample{ + example(p1, p2) { + return p1.id(p2).concat(p2); + } +} +\end{lstlisting} + +At first we assign a type placeholder to every expression in the input program. +Type placeholders also fill in for missing type annotations in method headers. + +\begin{lstlisting}{java} +class CExample{ + example(p1, p2) { + return p1.id(p2).concat(p2); + } +} +\end{lstlisting} +\begin{lstlisting}{java} +class CExample{ + (*@$\tv{a}$@*) example((*@$\tv{b}$@*) p1, (*@$\tv{c}$@*) p2) { + return ((p1:(*@$\tv{b}$@*)).id(p2:(*@$\tv{c}$@*)):(*@$\tv{d}$@*)).concat(p2:(*@$\tv{c}$@*)) : (*@$\tv{e}$@*); + } +} +\end{lstlisting} + +The placeholders $\tv{a}-\tv{e}$ are freshly created in this example and added to every expression. +The type of local variable expressions like \expr{p1} and \expr{p2} is already known and can be assigned directly. +$\expr{p1}:\tv{b}$ and $\expr{p2}:\tv{c}$ in this case. +The method call to \texttt{id} gets the fresh type placeholder $\tv{d}$ as type and the method call to \texttt{concat} is assigned the placeholder $\tv{e}$. + +Afterwards a method type environment $\mtypeEnvironment$ containing all method declarations is created. +Note how type placeholders are used for the \texttt{example} method: + +$\mtypeEnvironment{} = \left\{ \begin{array}{l} +\texttt{id} : \generics{\type{X}}\type{Id},\type{X} \to \type{X}, \\ +\texttt{concat} : \generics{\type{X}}\exptype{List}{\type{X}},\exptype{List}{\type{X}} \to \exptype{List}{\type{X}}, \\ +\texttt{example} : \type{CExample},\tv{b},\tv{c} \to \tv{a}, \\ +\end{array} \right\} +$ + +\begin{mathpar} + \inferrule[Method-Cons]{ + \mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C \\ + \overline{\mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C} \\ + \texttt{m} : \generics{\ol{Y \triangleleft N}}\type{T}_r, \overline{\type{T}} \to \type{T} \in { \mtypeEnvironment }\\ + \overline{\wtv{b}}, \tv{x}, \overline{\tv{x}} \ \text{fresh} \\ + C_m = \set{\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}}} \cup + [\overline{\wtv{b}}/\ol{Y}]\set{ \tv{x} \lessdotCC \type{T}_r, \overline{\tv{x} \lessdotCC \type{T}}, \type{T} \lessdot \tv{a}, \overline{Y \lessdot N} } + }{ + \mtypeEnvironment \vdash \expr{e}.\texttt{m}(\overline{\expr{e}}) : \tv{a} \implies C \cup \overline{C} \cup C_m + } +\end{mathpar} + +In case the input program contains multiple method declarations holding the same name and same amount of parameters then so called Or-Constraints must be generated. +Usually Java is able to determine which method to call based on the argument's types passed to the method. %' +During the constraint generation step the argument types are unknown and we have to assume multiple methods as invocation target. + +\begin{lstlisting} +class String{ + bool equals(String s){ .. } +} +class Int{ + bool equals(Int i){ .. } +} +class OrConsExample{ + m(a, b){ + return a.equals(b); + } +} +\end{lstlisting} + +The method call to \texttt{equals} now has multiple possibilities. +It could either be a call to the method in the class \texttt{Int} or in \texttt{String}. +The method type environment therfore contains two versions of the \texttt{equals} method: + +$\mtypeEnvironment{} = \set{ \texttt{equals}_1 : \type{String}, \type{String} \to \type{bool}, +\texttt{equals}_2 : \type{Int}, \type{Int} \to \type{bool}}$ + +The Or-Cons rule considers multiple declarations of the same method separately and joins all of them into a Or-Constraint. + +\begin{mathpar} + \inferrule[Or-Cons]{ + \texttt{m}_1 \ldots \texttt{m}_n \in \text{dom}(\mtypeEnvironment{}) \\ + \mtypeEnvironment \vdash \expr{e}.\texttt{m}_1(\overline{\expr{e}}) : \tv{a} \implies C_1 \quad + \ldots \quad + \mtypeEnvironment \vdash \expr{e}.\texttt{m}_n(\overline{\expr{e}}) : \tv{a} \implies C_n + }{ + \mtypeEnvironment \vdash \expr{e}.\texttt{m}(\overline{\expr{e}}) : \tv{a} \implies \orCons{}(C_1, \ldots, C_n) + } +\end{mathpar} + % Problem: % > void t2(List l){} From a41b2985663d78a9c3822792cfc9d4311fb5ba02 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Fri, 9 Aug 2024 16:20:09 +0200 Subject: [PATCH 09/11] Add New-Cons --- constraints.tex | 90 +++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 80 insertions(+), 10 deletions(-) diff --git a/constraints.tex b/constraints.tex index 489db36..5bece6f 100644 --- a/constraints.tex +++ b/constraints.tex @@ -348,12 +348,39 @@ 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)}. -\subsection{Examples} +\subsection{Constraint Generation} +The constraint generation is defined on a subset of Java displayed in figure \ref{fig:miniJavaSyntax}. +The input language includes only a small set of expressions like method calls, field access and a elvis operator $\elvis$ +which acts as a replacement for if-else expressions. +\begin{figure} +\par\noindent\rule{\textwidth}{0.4pt} +\center +$ +\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} & ::= & \highlight{\generics{\overline{\type{X} \triangleleft \type{N}}}}\ \highlight{\type{T}}\ \texttt{m}(\overline{\highlight{\type{T}}\ \expr{x}}) \{ \texttt{return} \ \expr{e}; \} \\ +\text{Terms} & \expr{e} & ::= & \expr{x} \\ +& & \ \ | & \texttt{new} \ \type{C}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\ +& & \ \ | & \expr{e}.f\\ +& & \ \ | & \expr{e}.\texttt{m}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\ +& & \ \ | & \expr{e} \elvis{} \expr{e}\\ +\text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\ +\text{Method type environment} & \mathrm{\Pi} & ::= & \overline{ \texttt{m} : \generics{\ol{X \triangleleft N}}\ \ol{T} \to \type{T}} +%\hline +\end{array} +$ +\par\noindent\rule{\textwidth}{0.4pt} +\caption{Input Syntax with optional type annotations}\label{fig:miniJavaSyntax} +\end{figure} - -% v.m(v, v.f, this.id(v)); - -% let x1 = v, x2 = v, x3 = v.f, x4 = |this.id(v)| in x1.m(x2, x3, x4) +We explain the process using the following example input. +The classes \texttt{List} and \texttt{Id} are already fully typed and we want to create constraints for the class +\texttt{CExample} now. \begin{lstlisting}{java} class Id{ @@ -361,7 +388,7 @@ class Id{ } class List { - List concat(List l){ ... } + List concat(List l){ ... } } class CExample{ @@ -371,7 +398,7 @@ class CExample{ } \end{lstlisting} -At first we assign a type placeholder to every expression in the input program. +The first step of constraint generation is to assign type placeholders to every expression in the input program. Type placeholders also fill in for missing type annotations in method headers. \begin{lstlisting}{java} @@ -394,16 +421,28 @@ The type of local variable expressions like \expr{p1} and \expr{p2} is already k $\expr{p1}:\tv{b}$ and $\expr{p2}:\tv{c}$ in this case. The method call to \texttt{id} gets the fresh type placeholder $\tv{d}$ as type and the method call to \texttt{concat} is assigned the placeholder $\tv{e}$. -Afterwards a method type environment $\mtypeEnvironment$ containing all method declarations is created. -Note how type placeholders are used for the \texttt{example} method: +Afterwards we create a method type environment $\mtypeEnvironment$ containing all method declarations. +Each entry has the form $\texttt{m} : \generics{\ol{X \triangleleft N}} \ol{T} \to \type{T}$. +The type arguments of the surrounding class and the type arguments of each method are merged together +leading to the list $\generics{\type{X}, \type{Y} \triangleleft \type{X}}$ for the \texttt{concat} method +($\triangleleft$ is short for \texttt{extends}). +Also the type of the surrounding class is added to the parameter list of the method. +This leads to the \texttt{id} method having two arguments. +One is the \texttt{Id} class itself and the second one is the actual arguemnt of the method. $\mtypeEnvironment{} = \left\{ \begin{array}{l} \texttt{id} : \generics{\type{X}}\type{Id},\type{X} \to \type{X}, \\ -\texttt{concat} : \generics{\type{X}}\exptype{List}{\type{X}},\exptype{List}{\type{X}} \to \exptype{List}{\type{X}}, \\ +\texttt{concat} : \generics{\type{X}, \type{Y} \triangleleft \type{X}}\exptype{List}{\type{X}},\exptype{List}{\type{Y}} \to \exptype{List}{\type{X}}, \\ \texttt{example} : \type{CExample},\tv{b},\tv{c} \to \tv{a}, \\ \end{array} \right\} $ +Note: type placeholders are used for the \texttt{example} method. + +Our constraint generation rules have the form: +$\mtypeEnvironment \vdash \expr{e} : \tv{a} \implies C$, +that given a method environment $\mtypeEnvironment$ and an expression $\expr{e}$ with type $\tv{a}$ generates the constraint set $C$. + \begin{mathpar} \inferrule[Method-Cons]{ \mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C \\ @@ -415,8 +454,39 @@ $ }{ \mtypeEnvironment \vdash \expr{e}.\texttt{m}(\overline{\expr{e}}) : \tv{a} \implies C \cup \overline{C} \cup C_m } + \and +% \inferrule[Field-Cons]{ +% \mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C \\ +% C_f = \set{} +% }{ +% \mtypeEnvironment \vdash \expr{e}.\texttt{f} : \tv{a} \implies C \cup C_f \\ +% } +% \and + \inferrule[Var-Cons]{ + }{ + \mtypeEnvironment \vdash \expr{x} : \tv{a} \implies \emptyset + } + \and + \inferrule[Elvis-Cons]{ + \mtypeEnvironment \vdash \expr{e}_1 : \tv{e}_1 \implies C_1 \\ + \mtypeEnvironment \vdash \expr{e}_2 : \tv{e}_2 \implies C_2 + }{ + \mtypeEnvironment \vdash \expr{e}_1 \elvis{} \expr{e}_2 : \tv{a} \implies C_1 \cup C_2 \cup \set{\tv{e}_1 \lessdot \tv{a}, \tv{e}_2 \lessdot \tv{a}} + } + \and + \inferrule[New-Cons]{ + \overline{\mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C} \\ + \texttt{class} \ \exptype{D}{\ol{X \triangleleft N}} \set{ \ol{T\ f}; \ldots } + }{ + \mtypeEnvironment \vdash \texttt{new}\ \type{D}(\ol{e}) : \tv{a} \implies \overline{C} \cup [\ol{\wtv{b}}/\ol{X}]\set{ \overline{\tv{e} \lessdot \type{T}}, \exptype{D}{\ol{X}} \lessdot \tv{a}, \ol{X \lessdot N} } + } \end{mathpar} +According to the Method-Cons rule the constraints generated by the call to \texttt{id} are: +$\mtypeEnvironment \vdash (p1:\tv{b}).id(p2:\tv{c}):\tv{d} \implies \set{\tv{b} \lessdot \tv{x}_1, \tv{c} \lessdot \tv{x}_2, \tv{x}_1 \lessdotCC \type{Id}, +\tv{x}_2 \lessdotCC \wtv{b}, \wtv{b} \lessdot \tv{d}}$. + +\subsection{Or-Constraints} In case the input program contains multiple method declarations holding the same name and same amount of parameters then so called Or-Constraints must be generated. Usually Java is able to determine which method to call based on the argument's types passed to the method. %' During the constraint generation step the argument types are unknown and we have to assume multiple methods as invocation target. From b50a6a93a23193ed0014c42267779db5c69c9bf3 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Fri, 9 Aug 2024 23:35:36 +0200 Subject: [PATCH 10/11] Adding to Soundness proof: Adding the old Unify-Soundness. Start writing lemmas to proof free variables cannot travel out of the scope of a let statement. They can only travel one hop at a time -> cant go through normal type placeholders --- soundness.tex | 75 ++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 69 insertions(+), 6 deletions(-) diff --git a/soundness.tex b/soundness.tex index d4811d8..d4b17c8 100644 --- a/soundness.tex +++ b/soundness.tex @@ -86,11 +86,17 @@ We have to show T-Let and T-Call which leaves us with: \begin{itemize} \item $\Delta | \Gamma \vdash \expr{e} : \sigma(\tv{e})$ and $\Delta | \Gamma \vdash \overline{\expr{e} : \sigma(\tv{e})}$ by assumption \item $\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}$ and $\Delta \vdash \overline{\type{T}_1 <: \wcNtype{\Delta'}{N}}$ by constraints $\tv{e} \lessdot \tv{x}$, $\overline{\tv{e} \lessdot \tv{x}}$ and lemma \ref{lemma:unifySoundness} - \item $\Delta, \Delta', \overline{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash \expr{x}.\texttt{m}(\ol{x}) : \sigma(\tv{r})$ by T-Call, because the following promises are satisfied + \item $\Delta, \Delta', \overline{\Delta'} | \Gamma, \expr{x} : \type{N}, \overline{\expr{x} : \type{N}} \vdash \expr{x}.\texttt{m}(\ol{x}) : \sigma(\tv{r})$ by T-Call and lemma \ref{lemma:freeVariableScope}, because the following promises are satisfied. + Note: The lemma \ref{lemma:freeVariableScope} and the fact that the wildcard placeholders $\overline{\wtv{b}}$ are + solely used here guarantees that no other than the variables declared in $\Delta, \Delta', \overline{\Delta}$ appear in $\sigma'(\overline{\wtv{b}})$. \begin{itemize} \item $\generics{\ol{X} \triangleleft \ol{U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m})$ is given, otherwise the program fails at the constraint generation step. \item $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$ by constraints $\ol{\wtv{b}} \lessdot [\ol{\wtv{b}}/\ol{X}]\ol{N}$ and lemma \ref{lemma:unifySoundness} - TODO: does not work because left side is a wildcard variable (maybe just change lemma soundness a bit) + there must be some $\ol{S}$ satisfying this premise. + + % what about we apply Unify again. With the known types. TODO: proof that unify can be applied again, with the capture converted versions of the constraints + %TODO: does not work because left side is a wildcard variable (maybe just change lemma soundness a bit) + \item \end{itemize} \end{itemize} \item[$\texttt{v}.\texttt{m}(\ol{v})$] @@ -156,12 +162,56 @@ We have to show T-Let and T-Call which leaves us with: \end{description} + +During the unification process free variables can only move one hop at a time. +Free variables originate from capture constraints. +By applying the capture rule to a constraint of the form $\wcNtype{\Delta}{N} \lessdotCC \type{T}$ the variables declared in $\Delta$ +are now free in the constraint $\type{N} \lessdot \type{T}$. +The other way of free variables traveling into a constraint is by substitution. +This is only possible if a constraint contains wildcard placeholders. +And only free variables which reside in the same constraint as a wildcard placeholders have the possibility of being set in. + +This effect is transitive. Free variables travel from constraint to constraint. +If there is no connection of constraints containing wildcard type placeholders between a free variable and a constraint, +then free variables cannot travel there. + \begin{lemma} - Free variables never leave their scope. - If $\tv{e} \lessdot \tv{x}, \overline{\tv{e} \lessdot \tv{x}}, - \tv{r} \lessdot \tv{a}$ % TODO + Free variables travel only \end{lemma} +\begin{lemma}{Free variables}\label{lemma:freeVariableScope} + Free variables never leave their scope. + If a set of constraints does not share a single wildcard type placeholder with the rest of the constraint set, + then it will never contain free variables used outside of it. +$(\Delta, \sigma) = \unify{}(\Delta_{in}, C \cup C')$ + +and $\text{wtv}(C') \cap \text{wtv}(C) = \emptyset$ +and $\overline{\sigma(\tv{x}) = \wcNtype{\Delta}{N}}$ + +then $\Delta, \Delta', \overline{\Delta}$ are all the variables used in $C'$. +\end{lemma} +\textit{Proof:} This is due to free variables only travel inbetween constraints and themselves via substitution. + +If $\type{S} \lessdotCC \type{T}$ spawns free variables, they will be contained within the reach of the wildcard type placeholders +used for the method call. +No other free variables can move into that scope. +With this lemma we can further proof that during a method call only the generated free variables are used. + +% \begin{lemma} +% Free variables never leave their scope. +% $C' = \set{ +% \overline{\tv{e} \lessdot \tv{x}}, \overline{\tv{x} \lessdotCC \tv{x}}, +% \overline{\tv{r} \lessdot \tv{a}} +% }$ +% $(\Delta, \sigma) = \unify{}(\Delta_{in}, C \cup C')$ + +% and $\text{wtv}(C') \cap \text{wtv}(C) = \emptyset$ +% and $\overline{\sigma(\tv{x}) = \wcNtype{\Delta}{N}}$ + +% then $\Delta, \Delta', \overline{\Delta}$ are all the variables used in $C'$. +% %if a wildcard type placeholder does not appear anywhere else, then only the free variables of its scope can be used for him +% \end{lemma} + % \begin{lemma} Unify does add free variables to types not containing free variables (or wildcard placeholders) % \begin{description} % \item[If] $(\sigma, \Delta) = \unify{}( \Delta', C )$ @@ -288,11 +338,24 @@ Trivial. \unify{} fails when a constraint $\tv{a} \doteq \rwildcard{X}$ arises. %TODO % does this really work. We have to show that the algorithm never gets stuck as long as there is a solution % maybe there are substitutions with types containing free variables that make additional solutions possible. Check! - \begin{lemma}{\unify{} Soundness:}\label{lemma:unifySoundness} \unify{}'s type solutions are correct respective to the subtyping rules defined in figure \ref{fig:subtyping}. \begin{description} \item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$ +\item[Then] there exists a substitution $\sigma'$ with: +\begin{itemize} +\item $\sigma \subseteq \sigma'$ +\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$ +\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \wcNtype{\Delta}{N}}$ +\item $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$ +\end{itemize} +\end{description} +\end{lemma} + +\begin{lemma}{\unify{} Soundness:}%\label{lemma:unifySoundness} +\unify{}'s type solutions are correct respective to the subtyping rules defined in figure \ref{fig:subtyping}. +\begin{description} +\item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$ with $\text{wtv}(\ol{S}) = \emptyset$ and $\text{wtv}(\ol{T}) = \emptyset$ \item[Then] $\Delta, \Delta' \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$ \item[and] either $\Delta, \Delta' \vdash \overline{\sigma(\type{S'}) <: \sigma(\type{T'})}$ From 2c4e84aea37b49fe3cd5e3764d35cc82879efc65 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Thu, 15 Aug 2024 15:13:17 +0200 Subject: [PATCH 11/11] Comment --- constraints.tex | 1 + 1 file changed, 1 insertion(+) diff --git a/constraints.tex b/constraints.tex index 5bece6f..56df85b 100644 --- a/constraints.tex +++ b/constraints.tex @@ -443,6 +443,7 @@ Our constraint generation rules have the form: $\mtypeEnvironment \vdash \expr{e} : \tv{a} \implies C$, that given a method environment $\mtypeEnvironment$ and an expression $\expr{e}$ with type $\tv{a}$ generates the constraint set $C$. +%Inference-rule in the style of: https://dl.acm.org/doi/pdf/10.1145/345099.345100 \begin{mathpar} \inferrule[Method-Cons]{ \mtypeEnvironment \vdash \expr{e} : \tv{e} \implies C \\