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

Add <:_? constraint (work in progress)

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-01-09 16:28:19 +01:00
parent e6807e65fc
commit 93c0b76b9c
2 changed files with 26 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
soundness.tex
View File

@ -153,12 +153,20 @@ $\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
% \end{lemma}
\begin{lemma} \label{lemma:unifyCC}
Free variables do not leave their scope.
\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}) }$
\item[If] $(\sigma, \Delta) = \unify{}( C \cup \set{ \type{T} \lessdot \type{S} } \cup \set{ \overline{\type{T} \lessdot \type{S} } } )$
\item[and] $\text{fv}(\type{T}, \type{S}) \subseteq \text{fv}(\ol{T}, \ol{S})$,
$\sigma(\ol{T}) = \ol{\wcNtype{\Delta}{N}}$ and $\sigma(\type{T}) = \wcNtype{\Delta'}{N'}$
\item[then] $ \Delta, \overline{\Delta}, \Delta' \vdash \sigma(\type{T}) <: \sigma(\type{S}) $
% \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}
Their scope is the set of constraints, which contain the same free variable placeholders.
% Wildcard place holders only use free variables occuring in the same constraint as them.
% \begin{description}
% \item[If] $(\sigma, \Delta) = \unify{}( C )$
@ -167,6 +175,19 @@ $\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
\end{lemma}
\textit{Proof:}
%TODO: is it true even?
The input set does not contain free variables, only free variable placeholders.
The only time \unify{} add a wildcard to the $\wildcardEnv$ is the \rulename{Capture} rule.
This rule is only applied for the outer wildcard environments for each type.
%where to get a Box<Box<a?>> ?
% Box<Box<a?>> <. Box<? super Box<?>>
% %What is with wildcards in the lower bounds of type
% Box<Box<a?>> <. X_Y.Box<Y>.Box<X>
% Y.Box<Y> <. Box<a?>
% Y =. a?
\begin{lemma}
The \unify{} algorithm only produces correct output for constraints not containing free variables.

4
unify.tex
View File

@ -44,7 +44,7 @@ The \unify{} algorithm internally uses the following data types:
\begin{tabular}{lcll}
$C $ &$::=$ &$\overline{c}$ & Constraint set \\
$c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
$c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \lessdotCC \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
$\type{T}, \type{U}, \type{L} $ & $::=$ & $\tv{a} \mid \wtv{a} \mid \gtype{G}$ & Type variable or Type \\
$\gtype{G}$ & $::=$ & $\type{X} \mid \ntype{N}$ & Wildcard, or Class Type \\
$\ntype{N}, \ntype{S}$ & $::=$ & $\wctype{\triangle}{C}{\ol{T}} $ & Class Type \\
@ -359,7 +359,7 @@ Their upper and lower bounds are fresh type variables.
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash
C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}} \lessdot \wctype{\Delta}{C}{\ol{T}} } \\
C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U'}}{\type{L'}}}}{C}{\ol{S}} \lessdotCC \wctype{\Delta}{C}{\ol{T}} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \overline{\wildcard{C}{\type{U'}}{\type{L'}}}