stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Soundness e.f

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-07-24 15:48:59 +02:00
parent a44568f789
commit 3548db28ba
1 changed files with 34 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
soundness.tex
View File

@ -107,7 +107,7 @@ A correct typing for method calls can be deducted from those type informations.
% \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,\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.
@ -135,6 +135,33 @@ By structural induction over the expression $\texttt{e}$.
and $\Delta, \Delta' \vdash \sigma(\tv{e}_2) <: \sigma(\tv{a})$ by lemma \ref{lemma:unifySoundness}
given the constraint $\tv{e}_2 \lessdot \tv{a}$.
\item[$\texttt{let}\ \texttt{x} = \texttt{t}_1 \ \texttt{in}\ \expr{x}.\texttt{f}$]
The let statement in the input is untyped and we have to create a let statement
$\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{t}_1 \ \texttt{in}\ \expr{x}.\texttt{f}$
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<a>, T <. t2
Let $\type{T}_1 = \wcNtype{\Delta'}{N} = \sigma(\tv{x})$, $\sigma(\tv{t_1}) = \type{T}_1$ 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}$
\end{itemize}
%TODO: use a lemma that says if Unify succeeds, then it also succeeds if the capture converted types are used.
% but it also works with a subset of the initial constraints.
% the generated constraints do not share wildcard placehodlers with other constraints.
@ -586,6 +613,12 @@ $\sigma(\wildcardEnv) = \sigma([\type{T}/\tv{a}]\wildcardEnv)$
Same as Subst
\end{description}
\begin{lemma}
\label{lemma:unifyNoFreeVariablesInSupertype}
A constraint $\tv{a} \lessdotCC \type{T}$ or $\tv{a} \lessdot \type{T}$ implies that
$\text{fv}(\sigma(\type{T})) \subseteq \text{fv}(\sigma(\tv{a}))$.
Only free variables, which are part of the left side are used on the right side.
\end{lemma}
% \subsection{Converting to Wild FJ}
% Wildcards are existential types which have to be \textit{unpacked} before they can be used.