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

Fix and comment

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-01-26 16:50:56 +01:00
parent ba4b78b57b
commit 0101341841
1 changed files with 7 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
soundness.tex
View File

@ -21,7 +21,7 @@ TODO:
\unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct. \unify{}'s type solutions for a constraint set generated by $\typeExpr{}$ are correct.
\begin{description} \begin{description}
\item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = C$ \item[if] $\typeExpr{}(\mtypeEnvironment{}, \texttt{e}, \tv{a}) = C$
and $(\Delta, \sigma) = \unify{\Delta', C}$ and $(\Delta, \sigma) = \unify{}(\Delta', C)$
% , with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } }$ % , with $C = \set{ \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } }$
% and $\vdash \ol{L} : \mtypeEnvironment{}$ % and $\vdash \ol{L} : \mtypeEnvironment{}$
% and $\Gamma \subseteq \mtypeEnvironment{}$ % and $\Gamma \subseteq \mtypeEnvironment{}$
@ -63,6 +63,12 @@ By structural induction over the expression $\texttt{e}$.
$\text{dom}(\Delta_c) \subseteq \text{fv}{\type{N}}$ by lemma \ref{lemma:tvsNoFV}. $\text{dom}(\Delta_c) \subseteq \text{fv}{\type{N}}$ by lemma \ref{lemma:tvsNoFV}.
% X.List<X> <. List<a?>
% $\sigma(\ol{\tv{r}}) = \overline{\wcNtype{\Delta}{N}}$,
% $\ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
% TODO: S ok? We could proof $\Delta, \Delta' \overline{\Delta} \vdash \ol{S} \ \ok$
% by proofing every substitution in Unify is ok aslong as every type in the inputs is ok
$\Delta \vdash \sigma(\tv{a}), \wcNtype{\Delta_c}{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 %Easy, because unify only generates substitutions for normal type placeholders which are OK