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

Combine let and field access in soundness proof

Browse Source
This commit is contained in:
JanUlrich 2024-07-24 10:16:30 +02:00
parent df24f3fd2f
commit a44568f789
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
soundness.tex
View File

@ -134,12 +134,13 @@ By structural induction over the expression $\texttt{e}$.
Therefore we can say $\Delta,\Delta' | \Gamma, \expr{x}:\type{N} \vdash \expr{t}_2 : \sigma(\tv{e}_2)$ by assumption
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[$\expr{v}.\texttt{f}$]
\item[$\texttt{let}\ \texttt{x} = \texttt{t}_1 \ \texttt{in}\ \expr{x}.\texttt{f}$]
%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.
% can they contain free variables from other places? They could, but isolation prevents that.
% TODO: but how to proof?
%generated constraints: t1 <. x, x <. N, T <. t2
We are allowed to use capture conversion for $\expr{v}$ here.
$\Delta \vdash \expr{v} : \sigma(\tv{a})$ by assumption.
$\Delta \vdash \sigma(\tv{a}) <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ and