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

Soundness e.f WIP

Browse Source
This commit is contained in:
JanUlrich 2024-07-24 21:24:11 +02:00
parent 3548db28ba
commit a98c4b0486
2 changed files with 23 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
constraints.tex
View File

@ -175,7 +175,7 @@ Those type variables count as regular types and can be held by normal type place
\orCons\set{
\set{ &
\tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}} ,
[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} ,
\tv{a} \doteq [\overline{\wtv{a}}/\ol{X}]\type{T},
\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}

37
soundness.tex
View File

@ -141,27 +141,34 @@ 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
Let $\type{T}_1 = \wcNtype{\Delta'}{N} = \sigma(\tv{x})$, $\sigma(\tv{t_1}) = \type{T}_1$,
$\sigma(\tv{a}) = \type{T}_2$ 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}$
First we can say $\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}}})$
%by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
%and lemmas \ref{lemma:unifySoundness} and \ref{lemma:unifyNoFreeVariablesInSupertype}.
By lemma \ref{lemma:unifyWellFormedness} and WF-Var we can deduct
$\text{fv}(\wcNtype{\Delta'}{N}) \subseteq \Delta$
and by constraint $\tv{x} \lessdotCC \exptype{C}{\ol{\wtv{a}}}$
and lemmas \ref{lemma:unifySoundness} and \ref{lemma:unifyNoFreeVariablesInSupertype}
we can finally say
$\Delta, \Delta' \vdash \type{N} <: \sigma(\exptype{C}{\ol{\wtv{a}}})$.
With the constraint $\tv{a} \doteq [\ol{\wtv{a}}/\ol{X}]\type{T}$
and $\sigma([\ol{\wtv{a}}/\ol{X}]\type{T}) \in \text{fields}(\sigma(\exptype{C}{\ol{\wtv{a}}}))$ by F-Class
we proof $\Delta, \Delta' | \Gamma, x : \type{N} \vdash \expr{x}.f_1 : \type{T}_2$.
\item $\Delta, \Delta' \vdash \type{T}_2 <: \type{T}$ by constraint %TODO: Rename constraints
\end{itemize}
% method call: a1 <c C<a>, a2 <c C<b>, a3 <c b?
% here lemma:unifyNoFreeVariablesInSupertype can be used too
%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.