Start with Type soundness for method call
This commit is contained in:
Andreas Stadelmeier
parent
c742bc03f8
commit
e6807e65fc
@ -21,12 +21,23 @@ Type inference produces a correctly typed program.
|
||||
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})}$
|
||||
\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})$
|
||||
\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}
|
||||
@ -38,7 +49,8 @@ By structural induction over the expression $\texttt{e}$.
|
||||
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})$.
|
||||
and $\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.
|
||||
@ -48,7 +60,42 @@ By structural induction over the expression $\texttt{e}$.
|
||||
$\Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok$ %TODO
|
||||
%Easy, because unify only generates substitutions for normal type placeholders which are OK
|
||||
|
||||
\item[$\texttt{e}.\texttt{m}(\ol{e})$] Given
|
||||
\item[$\texttt{e}.\texttt{m}(\ol{e})$]
|
||||
\begin{gather}
|
||||
\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'} \\
|
||||
\Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\
|
||||
\label{sp:4}
|
||||
\Delta \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}} \\
|
||||
\end{gather}
|
||||
\ref{sp:1} is guaranteed by the constraints $\ol{r} \lessdot \ol{T}$.
|
||||
$\ol{\tv{r}} \lessdot \ol{T}$ says that there is a $\Delta'$ with
|
||||
$\Delta, \Delta' \vdash CC(\sigma(\tv{r})) <: \type{T}$.
|
||||
|
||||
If $\overline{\sigma(\tv{r}) = \wcNtype{\Delta}{N}}$
|
||||
then \ref{sp:1} due to lemma \ref{lemma:unifyCC}.
|
||||
% X.List<X> <. List<a?>
|
||||
% set \sigma(r) = X.N
|
||||
% If there exists a subtype r <: T, then r <: X.N, N <: T with X.N == r
|
||||
% If CC(X.N) <: T, then N <: T
|
||||
% R <: X.N due to S-Refl.
|
||||
% \Delta, X \vdash N <: T due to assumption and S-Exists.
|
||||
% What if X.N <: Y (where is this Y coming from?)
|
||||
% %TODO:
|
||||
% We have to show, that all constraints using the same wtv's C = X1.T1 <. X2.T2 ,...
|
||||
% with a? \in T1, T2, ....
|
||||
% then \Delta' \subseteq X1, X2, ... for \Delta, \Delta \vdash sigma(T1) <: sigma(X2.T2), ....
|
||||
|
||||
% when only wildcards in the top level domain from the constraints involving the a? variables are involved
|
||||
% then they are all contained in $\Delta, \Delta', \overline{Delta}$, which makes S ok true! (does it?)
|
||||
% and due to r <. T, the judgements N <: [S/X]U and T_r <: \Delta.N are true!
|
||||
|
||||
%TODO for Unify:
|
||||
We have to make sure, that wildcards are correctly saved in the Wildcard environment
|
||||
|
||||
% If $\ol{\tv{r}} \lessdot \ol{T}$ how can we say that \Delta' only uses
|
||||
\end{description}
|
||||
|
||||
\begin{lemma}
|
||||
@ -105,6 +152,22 @@ $\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
|
||||
% \end{description}
|
||||
% \end{lemma}
|
||||
|
||||
\begin{lemma} \label{lemma:unifyCC}
|
||||
\begin{description}
|
||||
\item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \overline{\wcNtype{\Delta}{N} \lessdot \type{T} } } )$
|
||||
\item[and] $\text{fv}(\ol{T}) \notin C$, $\text{fv}(\ol{\wcNtype{\Delta}{N}}) \notin C$
|
||||
\item[Then] $\Delta, \overline{\Delta} \vdash \overline{ \sigma(\type{N}) <: \sigma(\type{T}) }$
|
||||
\end{description}
|
||||
|
||||
% Wildcard place holders only use free variables occuring in the same constraint as them.
|
||||
% \begin{description}
|
||||
% \item[If] $(\sigma, \Delta) = \unify{}( C )$
|
||||
% \item[Then] $\text{fv}(\sigma(\tv{a})) \subseteq \set{ \text{fv}(\type{T}) \cup \text{fv}(\type{S}) \mid \tv{a} \in \text{tph}(\type{T},\type{S}), (\type{T} \lessdot \type{S}) \in C }$
|
||||
% \end{description}
|
||||
\end{lemma}
|
||||
\textit{Proof:}
|
||||
%TODO: is it true even?
|
||||
|
||||
\begin{lemma}
|
||||
The \unify{} algorithm only produces correct output for constraints not containing free variables.
|
||||
\begin{description}
|
||||
@ -116,6 +179,21 @@ and $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T
|
||||
% and $\sigma(\type{T'}) = \sigma(\type{T'})$.
|
||||
|
||||
The function $\CC{}$ is given as $\CC{}(\wcNtype{\Delta}{N}) = \type{N}$
|
||||
|
||||
|
||||
% Unify cannot guarantee that only wildcards declared on the left side are used. Example input:
|
||||
% List<b?> <. List<b?>
|
||||
% b? =. X
|
||||
% but if the left side is a normal type (no fv's) then this can be guaranteed (maybe?)
|
||||
%String <. X_String % here X is not in the environment
|
||||
|
||||
% What is the problem?
|
||||
% a? can only use wildcards, which are declared in \Delta or on the left side
|
||||
% Otherwise constraints of the form a <. T cannot ensure soundness!
|
||||
|
||||
% We could say that a? only gets free variables hold by the constraints a? appears in
|
||||
|
||||
% a constraint a <. T means that there are free variables
|
||||
\end{description}
|
||||
\end{lemma}
|
||||
|
||||
@ -138,10 +216,10 @@ The function $\CC{}$ is given as $\CC{}(\wcNtype{\Delta}{N}) = \type{N}$
|
||||
For every step in the \unify{} algorithm:
|
||||
Assuming the unifier $\sigma$ is correct for a constraint set $C'$, the unifier is also correct for the
|
||||
constraint set $C$ before the transformation.
|
||||
\begin{description}
|
||||
\item[Assumption:] $\unify{}(C) = (\Delta, \sigma)$, with $\Delta \vdash \sigma(C)$
|
||||
\item[Induction step:] For every case $C'$ which can be transformed to $C$ we have to show $\Delta \vdash \sigma(C')$
|
||||
\end{description}
|
||||
% \begin{description}
|
||||
% \item[Assumption:] $\unify{}(C) = (\Delta, \sigma)$, with $\Delta \vdash \sigma(C)$
|
||||
% \item[Induction step:] For every case $C'$ which can be transformed to $C$ we have to show $\Delta \vdash \sigma(C')$
|
||||
% \end{description}
|
||||
|
||||
\unify{} terminates with $C = \emptyset$ for which the preposition holds:
|
||||
$\Delta \vdash \sigma(\emptyset)$
|
||||
|
||||
Loading…
Reference in New Issue
Block a user