Add <._c constraint to Type for field and alter soundness proof
This commit is contained in:
Andreas Stadelmeier
parent
b775045d17
commit
881eecef8a
@ -112,7 +112,7 @@ Wildcard types are not used during the constraint generation step and have no in
|
||||
& \constraint = \begin{array}[t]{@{}l@{}l}
|
||||
\orCons\set{
|
||||
\set{ &
|
||||
\tv{r} \lessdot \exptype{C}{\ol{\wtv{a}}} ,
|
||||
\tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}} ,
|
||||
[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} , \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}
|
||||
|
||||
@ -17,14 +17,13 @@ Type inference produces a correctly typed program.
|
||||
\unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
|
||||
\begin{description}
|
||||
\item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = C$
|
||||
, with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdot \type{T'} } }$
|
||||
and $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
|
||||
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'})}$
|
||||
%and $\Delta \vdash \sigma(\type{S}), \sigma(\type{T})\ \ok$
|
||||
\item[then] $\Delta|\Gamma \vdash \texttt{e} : \sigma(\tv{a})$
|
||||
and $(\Delta, \sigma) = \unify{\Delta', C}$
|
||||
% , 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})$
|
||||
\end{description}
|
||||
\end{lemma}
|
||||
Regular type placeholders represent type annotations.
|
||||
@ -41,23 +40,26 @@ used in let statements and as type parameters for generic method calls.
|
||||
\textit{Proof:}
|
||||
By structural induction over the expression $\texttt{e}$.
|
||||
\begin{description}
|
||||
\item[$\texttt{e}.\texttt{f}$] $\Delta|\Gamma \vdash \texttt{e} : \sigma(\tv{r})$ by assumption.
|
||||
$\Delta', \Delta\vdash \CC{}(\sigma(\tv{r})) <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise.
|
||||
Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$.
|
||||
%TODO: Proof this: The reason is that r is not flagged with a ? and we only add free variables here, that are in \Delta
|
||||
Then $\text{fv}(\wcNtype{\Delta'}{N}) \subseteq \text{dom}(\Delta)$
|
||||
and therefore $\text{fv}(\type{N}) \subseteq \text{dom}(\Delta, \Delta')$.
|
||||
This implies $\Delta, \Delta' \vdash \type{U}_i <: \type{S}$,
|
||||
because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$
|
||||
and $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$
|
||||
\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.
|
||||
$\Delta', \Delta, \Delta_c \vdash \type{N} <: \sigma(\exptype{C}{\overline{\wtv{a}}})$ by premise.
|
||||
%Let $\sigma(\tv{r}) = \wcNtype{\Delta'}{N}$.
|
||||
Let $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) = \wcNtype{\Delta_t}{N_t}$.
|
||||
|
||||
The completion of $|\texttt{e}.\texttt{f}|$ is $\texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f}$
|
||||
|
||||
We now show
|
||||
$\Delta|\Gamma \vdash \texttt{let}\ \texttt{x} = \texttt{e} : \wcNtype{\Delta_c}{N}\ \texttt{in} \ \texttt{x}.\texttt{f} : \sigma(a)$
|
||||
by the T-Field rule.
|
||||
$\Delta \vdash \wcNtype{\Delta_c}{N} <: \wcNtype{\Delta_c}{N}$ by S-Refl.
|
||||
$\Delta, \Delta_c \vdash \type{U}_i <: \sigma(\tv{a})$,
|
||||
because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$ and lemma \ref{lemma:unifySoundness}.
|
||||
$\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$
|
||||
and $\text{fv}(\type{U}_i) \subseteq \text{fv}(\type{N})$ by definition of $\textit{fields}$.
|
||||
|
||||
% Set $\sigma(\tv{r}) = \type{T} = \wcNtype{\Delta'}{N}$.
|
||||
% Then $\Delta | \Gamma \vdash e : \type{T}$ by assumption. $\Delta \vdash \type{T} <: \wcNtype{\Delta'}{N}$ by S-Refl.
|
||||
% $\textit{fields}(\type{N}) = \overline{\type{U}\ f}$ by definition.
|
||||
% $\Delta, \Delta' \vdash \type{U}_i <: \type{S}$ by premise.
|
||||
$\text{dom}(\Delta_c) \subseteq \text{fv}{\type{N}}$ by lemma \ref{lemma:tvsNoFV}.
|
||||
|
||||
$\Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok$ %TODO
|
||||
$\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[$\texttt{e}.\texttt{m}(\ol{e})$]
|
||||
@ -152,10 +154,21 @@ $\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
|
||||
% \end{description}
|
||||
% \end{lemma}
|
||||
|
||||
\begin{lemma} \label{lemma:tvsNoFV}
|
||||
\unify{} does not add free variables to types not containing free variables.
|
||||
\begin{description}
|
||||
\item[If] $(\sigma, \Delta) = \unify{} (C)$
|
||||
\item[and] $\tv{a}$ being a type placeholders used in $C$
|
||||
\item[then] $\text{fv}(\sigma(\tv{a})) = \emptyset$
|
||||
\end{description}
|
||||
\end{lemma}
|
||||
\textit{Proof:}
|
||||
Trivial
|
||||
|
||||
\begin{lemma} \label{lemma:unifyCC}
|
||||
Free variables do not leave their scope.
|
||||
Free variables do not leave their scope. TODO
|
||||
\begin{description}
|
||||
\item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \type{T} \lessdot \type{S} } \cup \set{ \overline{\type{T} \lessdot \type{S} } } )$
|
||||
\item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \type{T} \lessdot \type{S} } \cup \set{ \overline{\type{T} \lessdotCC \type{S} } } )$
|
||||
\item[and] $\text{fv}(\type{T}, \type{S}) \subseteq \text{fv}(\ol{T}, \ol{S})$,
|
||||
$\sigma(\ol{T}) = \ol{\wcNtype{\Delta}{N}}$ and $\sigma(\type{T}) = \wcNtype{\Delta'}{N'}$
|
||||
\item[then] $ \Delta, \overline{\Delta}, \Delta' \vdash \sigma(\type{T}) <: \sigma(\type{S}) $
|
||||
@ -193,8 +206,8 @@ This rule is only applied for the outer wildcard environments for each type.
|
||||
|
||||
% Problem: für tvs dürfen keine Wildcards eingesetzt werden, außer für die
|
||||
|
||||
\begin{lemma}
|
||||
The \unify{} algorithm only produces correct output for constraints not containing free variables.
|
||||
\begin{lemma}\label{lemma:unifySoundness}
|
||||
The \unify{} algorithm only produces correct output.
|
||||
\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[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
|
||||
|
||||
Loading…
Reference in New Issue
Block a user