From edc7f871087a3753d4b2f3a2538cb02dcc6f0417 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Thu, 1 Feb 2024 14:54:44 +0100 Subject: [PATCH] Type Soundness --- soundness.tex | 53 ++++++++++++++++++++++++++++++--------------------- 1 file changed, 31 insertions(+), 22 deletions(-) diff --git a/soundness.tex b/soundness.tex index e8aa7fc..4d1c5e8 100644 --- a/soundness.tex +++ b/soundness.tex @@ -21,13 +21,13 @@ TODO: \unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct. \begin{description} \item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = C$ - and $(\Delta, \sigma) = \unify{}(\Delta', C)$ + and $(\Delta_u, \sigma) = \unify{}(\Delta', C)$ and let $\Delta = \Delta_u \cup \Delta'$ % , 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] $\Delta|\Gamma \vdash |\texttt{e}| : \sigma(\tv{a})$ + \item[then] there is a completion $|\texttt{e}|$ with $\Delta|\Gamma \vdash |\texttt{e}| : \sigma(\tv{a})$ \end{description} \end{lemma} Regular type placeholders represent type annotations. @@ -42,7 +42,7 @@ used in let statements and as type parameters for generic method calls. % 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}$. +By structural induction over the expression $\texttt{e}$. \begin{description} \item[$\texttt{e}.\texttt{f}$] Let $\sigma(\tv{r}) = \wcNtype{\Delta_c}{N}$, then $\Delta|\Gamma \vdash \texttt{e} : \wcNtype{\Delta_c}{N}$ by assumption. @@ -97,30 +97,39 @@ By structural induction over the expression $\texttt{e}$. \item[$\texttt{e}.\texttt{m}(\ol{e})$] Lets have a look at the case where the receiver and parameter types are all named types. -So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta'}{N}$: -\begin{gather} - \label{sp:0} - \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T} \\ - \label{sp:1} - \Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U} \\ - \label{sp:2} - \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \\ - \label{sp:3} - \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\ - \label{sp:4} - \Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}} - \end{gather} - \ref{sp:0}, \ref{sp:1} and \ref{sp:2} are guaranteed by the generated constraints and lemma \ref{lemma:unifySoundness} and \ref{lemma:unifyCC}. - \ref{sp:4} due to $\ol{T} = \ol{\wcNtype{\Delta}{N}}$ and S-Refl. $\Delta, \Delta' \vdash \type{T}_r <: \wcNtype{\Delta'}{N}$ accordingly. +So $\sigma(\ol{\tv{r}}) = \ol{T} = \ol{\wcNtype{\Delta_u}{N}}$ and $\sigma(\tv{r}) = \type{T}_r = \wcNtype{\Delta_u}{N}$ +and a $\Delta'$, $\overline{\Delta}$ where $\Delta' \subseteq \Delta_u$, $\overline{\Delta \subseteq \Delta_u}$ +and $\text{dom}(\Delta') = (\text{fv}(\type{N})/\Delta)$, $\overline{\text{dom}(\Delta) = (\text{fv}(\type{N})/\Delta)}$ in + +$\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{e} \ \texttt{in}\ +\texttt{let}\ \ol{x} : \overline{\wcNtype{\Delta'}{N}} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x})$ + +%TODO: show that this type exists \wcNtype{\Delta'}{N} (a \Delta' which only contains free variables of the type N) +% and which is a supertype of T_r (so no free variables in T_r) + This implies $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ and $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ + $\Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T}$, + $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U}$, + and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}$ + are guaranteed by the generated constraints and lemma \ref{lemma:unifySoundness} and \ref{lemma:unifyCC}. + $\Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}}$ due to $\ol{T} = \ol{\wcNtype{\Delta}{N}}$ and S-Refl. $\Delta, \Delta' \vdash \type{T}_r <: \wcNtype{\Delta'}{N}$ accordingly. $\Delta|\Gamma \vdash \texttt{t}_r : \type{T}_r$ and $\Delta|\Gamma \vdash \ol{t} : \ol{T}_r$ by assumption. $\Delta, \Delta' \vdash \ol{\wcNtype{\Delta}{N}} \ \ok$ by lemma \ref{lemma:unifyWellFormedness}, therefore $\Delta, \Delta', \overline{\Delta} \vdash \ol{N} \ \ok$, which implies $\Delta, \Delta', \overline{\Delta} \vdash \ol{U} \ \ok$ - by lemma \ref{lemma:wfHereditary} and \ref{sp:3} by premise of WF-Class. + by lemma \ref{lemma:wfHereditary} and $\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok $ by premise of WF-Class. The same goes for $\wcNtype{\Delta'}{N}$. - $\text{dom}(\Delta') \subseteq \text{fv}(\type{N})$ TODO! -%\ref{sp:3} -%TODO: S is not in \sigma. They are generated by a local type inference algorithm + % \begin{gather} +% \label{sp:0} +% \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} \type{T} \\ +% \label{sp:1} +% \Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U} \\ +% \label{sp:2} +% \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \\ +% \label{sp:3} +% \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\ +% \label{sp:4} +% \Delta, \Delta' \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}} +% \end{gather} Method calls generate multiple constraints that share the same wildcard placeholders ($\ol{\wtv{a}}$, $\ol{\wtv{b}}$). %TODO: show that only those wildcards in the parameters and receiver type are used ($\ol{\Delta}$)