diff --git a/soundness.tex b/soundness.tex index 3a5ae1f..2754d93 100644 --- a/soundness.tex +++ b/soundness.tex @@ -21,12 +21,23 @@ Type inference produces a correctly typed program. and $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$ and $\vdash \ol{L} : \mtypeEnvironment{}$ and $\Gamma \subseteq \mtypeEnvironment{}$ - \item[given] a $\Delta, \sigma$ with $\Delta \vdash \overline{\sigma(\type{S}) <: \sigma(\type{T})}$ + \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'})}$ %and $\Delta \vdash \sigma(\type{S}), \sigma(\type{T})\ \ok$ \item[then] $\Delta|\Gamma \vdash \texttt{e} : \sigma(\tv{a})$ \end{description} \end{lemma} +Regular type placeholders represent type annotations. +These are the only types a \wildFJ{} program needs to be correctly typed. +The type placeholders flagged as wildcard placeholders are intermediate types +used in let statements and as type parameters for generic method calls. + +%Unify needs to return S aswell and guarantee that the \Delta' environment are the wildcards +% only used inside the constraint the wildcard variable occurs +% should Unify also return the \Delta' environment? Otherwise the bounds of free wildcard variables are lost + +% Or is it possible to deduct the right \ol{S} directly from the types in the normal TPHs? + \textit{Proof:} By structural induction over the expression $\texttt{e}$. \begin{description} @@ -38,7 +49,8 @@ By structural induction over the expression $\texttt{e}$. and therefore $\text{fv}(\type{N}) \subseteq \text{dom}(\Delta, \Delta')$. This implies $\Delta, \Delta' \vdash \type{U}_i <: \type{S}$, because of the constraint $[\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a}$ - and $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$. + and $\textit{fields}(\sigma(\exptype{C}{\overline{\wtv{a}}})) = \sigma([\overline{\wtv{a}}/\ol{X}]\type{T})$ + and $\text{fv}(\type{U}_i) \subseteq \text{fv}(\type{N})$ by definition of $\textit{fields}$. % Set $\sigma(\tv{r}) = \type{T} = \wcNtype{\Delta'}{N}$. % Then $\Delta | \Gamma \vdash e : \type{T}$ by assumption. $\Delta \vdash \type{T} <: \wcNtype{\Delta'}{N}$ by S-Refl. @@ -48,7 +60,42 @@ By structural induction over the expression $\texttt{e}$. $\Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok$ %TODO %Easy, because unify only generates substitutions for normal type placeholders which are OK - \item[$\texttt{e}.\texttt{m}(\ol{e})$] Given + \item[$\texttt{e}.\texttt{m}(\ol{e})$] + \begin{gather} + \label{sp:1} + \Delta, \Delta', \overline{\Delta} \vdash \ol{N} <: [\ol{S}/\ol{X}]\ol{U} \\ + \label{sp:2} + \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \\ + \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \\ + \label{sp:4} + \Delta \vdash \ol{T} <: \ol{\wcNtype{\Delta}{N}} \\ + \end{gather} + \ref{sp:1} is guaranteed by the constraints $\ol{r} \lessdot \ol{T}$. + $\ol{\tv{r}} \lessdot \ol{T}$ says that there is a $\Delta'$ with + $\Delta, \Delta' \vdash CC(\sigma(\tv{r})) <: \type{T}$. + + If $\overline{\sigma(\tv{r}) = \wcNtype{\Delta}{N}}$ + then \ref{sp:1} due to lemma \ref{lemma:unifyCC}. + % X.List <. List + % set \sigma(r) = X.N + % If there exists a subtype r <: T, then r <: X.N, N <: T with X.N == r + % If CC(X.N) <: T, then N <: T + % R <: X.N due to S-Refl. + % \Delta, X \vdash N <: T due to assumption and S-Exists. + % What if X.N <: Y (where is this Y coming from?) + % %TODO: + % We have to show, that all constraints using the same wtv's C = X1.T1 <. X2.T2 ,... + % with a? \in T1, T2, .... + % then \Delta' \subseteq X1, X2, ... for \Delta, \Delta \vdash sigma(T1) <: sigma(X2.T2), .... + + % when only wildcards in the top level domain from the constraints involving the a? variables are involved + % then they are all contained in $\Delta, \Delta', \overline{Delta}$, which makes S ok true! (does it?) + % and due to r <. T, the judgements N <: [S/X]U and T_r <: \Delta.N are true! + + %TODO for Unify: + We have to make sure, that wildcards are correctly saved in the Wildcard environment + + % If $\ol{\tv{r}} \lessdot \ol{T}$ how can we say that \Delta' only uses \end{description} \begin{lemma} @@ -105,6 +152,22 @@ $\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$. % \end{description} % \end{lemma} +\begin{lemma} \label{lemma:unifyCC} +\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}) }$ +\end{description} + + % Wildcard place holders only use free variables occuring in the same constraint as them. + % \begin{description} + % \item[If] $(\sigma, \Delta) = \unify{}( C )$ + % \item[Then] $\text{fv}(\sigma(\tv{a})) \subseteq \set{ \text{fv}(\type{T}) \cup \text{fv}(\type{S}) \mid \tv{a} \in \text{tph}(\type{T},\type{S}), (\type{T} \lessdot \type{S}) \in C }$ + % \end{description} +\end{lemma} +\textit{Proof:} +%TODO: is it true even? + \begin{lemma} The \unify{} algorithm only produces correct output for constraints not containing free variables. \begin{description} @@ -116,6 +179,21 @@ and $\Delta, \Delta' \vdash \overline{\CC{}(\sigma(\type{S'})) <: \sigma(\type{T % and $\sigma(\type{T'}) = \sigma(\type{T'})$. The function $\CC{}$ is given as $\CC{}(\wcNtype{\Delta}{N}) = \type{N}$ + + +% Unify cannot guarantee that only wildcards declared on the left side are used. Example input: +% List <. List +% b? =. X +% but if the left side is a normal type (no fv's) then this can be guaranteed (maybe?) +%String <. X_String % here X is not in the environment + +% What is the problem? +% a? can only use wildcards, which are declared in \Delta or on the left side +% Otherwise constraints of the form a <. T cannot ensure soundness! + +% We could say that a? only gets free variables hold by the constraints a? appears in + +% a constraint a <. T means that there are free variables \end{description} \end{lemma} @@ -138,10 +216,10 @@ The function $\CC{}$ is given as $\CC{}(\wcNtype{\Delta}{N}) = \type{N}$ For every step in the \unify{} algorithm: Assuming the unifier $\sigma$ is correct for a constraint set $C'$, the unifier is also correct for the constraint set $C$ before the transformation. -\begin{description} -\item[Assumption:] $\unify{}(C) = (\Delta, \sigma)$, with $\Delta \vdash \sigma(C)$ -\item[Induction step:] For every case $C'$ which can be transformed to $C$ we have to show $\Delta \vdash \sigma(C')$ -\end{description} +% \begin{description} +% \item[Assumption:] $\unify{}(C) = (\Delta, \sigma)$, with $\Delta \vdash \sigma(C)$ +% \item[Induction step:] For every case $C'$ which can be transformed to $C$ we have to show $\Delta \vdash \sigma(C')$ +% \end{description} \unify{} terminates with $C = \emptyset$ for which the preposition holds: $\Delta \vdash \sigma(\emptyset)$