From 17559170d0c702b916e572b9de0f7d378160ffd2 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Tue, 19 Mar 2024 20:52:04 +0100 Subject: [PATCH] LessDotCC constraints stay preserved --- unify.tex | 72 ++++++++++++++++++++++++++++++++----------------------- 1 file changed, 42 insertions(+), 30 deletions(-) diff --git a/unify.tex b/unify.tex index e49b0dd..db5ca30 100644 --- a/unify.tex +++ b/unify.tex @@ -259,6 +259,12 @@ $ \end{figure} +The capture constraints are preserved when applying the \rulename{Upper} rule. +%because \texttt{let} statements like +%let x : X = v in +%can be transformed to +%let x : U = v in + \begin{figure} \begin{center} \leavevmode @@ -277,37 +283,38 @@ $ \rulename{Upper} & $ \begin{array}[c]{l} - \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdot \type{G} } \\ + \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdot_1 \type{G} } \\ \hline \vspace*{-0.4cm}\\ - \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdot \type{G} } + \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdot_1 \type{G} } \end{array} - \quad \quad - \begin{array}[c]{l} %TODO: can the second part be removed by adding a X.C <. C constraint at method invocation? - \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdotCC \type{G} } \\ + $ + % \quad \quad + % \begin{array}[c]{l} %TODO: can the second part be removed by adding a X.C <. C constraint at method invocation? + % \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{A} \lessdotCC \type{G} } \\ + % \hline + % \vspace*{-0.4cm}\\ + % \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdotCC \type{G} } + % \end{array} + % $ + \\\\ + \rulename{Lower} + & $ + \begin{array}[c]{l} + \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot_1 \type{A} } \\ \hline \vspace*{-0.4cm}\\ - \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \, \set{ \type{U} \lessdotCC \type{G} } + \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot_1 \type{L} } \end{array} $ \\\\ \rulename{Lower} & $ \begin{array}[c]{l} - \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot \type{A} } \\ + \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \ntv{a} \lessdot_1 \type{A} } \\ \hline \vspace*{-0.4cm}\\ - \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \type{G} \lessdot \type{L} } - \end{array} - $ - \\\\ - \rulename{Lower} - & $ - \begin{array}[c]{l} - \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \ntv{a} \lessdot \type{A} } \\ - \hline - \vspace*{-0.4cm}\\ - \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \ntv{a} \lessdot \type{L} } + \wildcardEnv \cup \set{\wildcard{A}{U}{L}} \vdash C \cup \set{ \ntv{a} \lessdot_1 \type{L} } \end{array} \quad \type{A} \notin \Delta_{in} $ %TODO: a <. X with X in Delta_in => a =. X % other possibliity: is it allowed to see X extends List as class X extends List {} @@ -316,7 +323,7 @@ $ \rulename{Bot} & $ \begin{array}[c]{l} - \wildcardEnv \vdash C \cup \set{ \bot \lessdot \type{T} } \\ + \wildcardEnv \vdash C \cup \set{ \bot \lessdot_1 \type{T} } \\ \hline \vspace*{-0.4cm}\\ \wildcardEnv \vdash C @@ -326,7 +333,7 @@ $ \rulename{Pit} & $ \begin{array}[c]{l} - \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \bot } \\ + \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot_1 \bot } \\ \hline \vspace*{-0.4cm}\\ \wildcardEnv \vdash C \cup \set{ \tv{a} \doteq \bot } @@ -695,6 +702,11 @@ Removing a wildcard works by setting its lower and upper bound to be equal. (Def: $\type{Object} = \wildcard{A}{Object}{Object}$). The \rulename{Equals} rule is responsible for this. +The subtype constraints are a subset of the capture constraints $(\type{T} \lessdot \type{S}) \implies (\type{T} \lessdotCC \type{S})$. +Every transformation on a subtype constraint can also be applied to a capture constraint, but the capture constraints need to be preserved. +We indicate this by numbering the constraints in each transformation. +Constraints with the same number stay the same type. + \textbf{Example:} \begin{displaymath} \begin{array}[c]{@{}ll} @@ -821,15 +833,15 @@ This builds a search tree over multiple possible solutions. \rulename{Same} & $ \begin{array}[c]{l} - \wildcardEnv \vdash - C \cup \type{G} \lessdot \ntv{a}\\ + \wildcardEnv \cup \set{\overline{\wildcard{A}{\type{U}}{\type{L}}}} \vdash + C \cup \wctype{\Delta'}{C}{\ol{X}} \lessdot \ntv{a}\\ \hline - \wildcardEnv \vdash + \wildcardEnv \cup \set{\overline{\wildcard{A}{\type{U}}{\type{L}}}} \vdash C \cup \set{ - \ntv{a} \doteq \type{G} + \ntv{a} \doteq \wctype{\Delta',\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{X}} } \end{array} \quad \begin{array}[c]{l} - \text{fv}(\type{G}) \in \Delta_{in} + \text{fv}(\wctype{\Delta'}{C}{\ol{X}}) / \Delta_{in} = \overline{\rwildcard{A}} \end{array} $ \\\\ @@ -949,10 +961,10 @@ This builds a search tree over multiple possible solutions. & $ \begin{array}[c]{l} \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N}, - \tv{a} \lessdot \tv{b}} + \tv{a} \lessdot_1 \tv{b}} \\ \hline - \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \tv{b}, \tv{b} \lessdot \type{N} } + \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot_1 \tv{b}, \tv{b} \lessdot \type{N} } \end{array} $ \\\\ @@ -960,11 +972,11 @@ This builds a search tree over multiple possible solutions. \rulename{Raise} & $ \begin{array}[c]{l} - \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot \type{N}, + \wildcardEnv \vdash C \cup \set{ \tv{a} \lessdot_1 \type{N}, \tv{a} \lessdot \tv{b}} \\ \hline - \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \type{N}, \type{N} \lessdot \tv{b} } + \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot_1 \type{N}, \type{N} \lessdot \tv{b} } \end{array} $ \end{tabular} @@ -973,7 +985,7 @@ This builds a search tree over multiple possible solutions. \caption{Step 2 branching: Multiple rules can be applied to the same constraint} \label{fig:step2-rules} \end{figure} - + \begin{figure} \begin{center} \fbox{