diff --git a/constraints.tex b/constraints.tex index 2d1917d..0ba40a2 100644 --- a/constraints.tex +++ b/constraints.tex @@ -144,11 +144,11 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi \typeExpr{} &({\mtypeEnvironment} , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2) = \\ & \begin{array}{ll} \textbf{let} - & \tv{e} \ \text{fresh} \\ + & \tv{e}, \tv{x} \ \text{fresh} \\ & \consSet_R = \typeExpr({\mtypeEnvironment}, \expr{e}_1, \tv{e})\\ & \constraint = \set{ - \tv{e} \lessdotCC \tv{x} + \tv{e} \lessdot \tv{x} }\\ {\mathbf{in}} & { \consSet_R \cup \set{\constraint}} \cup \typeExpr(\mtypeEnvironment \cup \set{\expr{x} : \tv{x}}) @@ -190,7 +190,7 @@ The ones to already typed methods and calls to untyped methods. \textbf{let} & \tv{r}, \ol{\tv{r}} \text{ fresh} \\ & \constraint = [\overline{\wtv{b}}/\ol{Y}]\set{ - \ol{S} \lessdot \ol{T}, \type{T} \lessdot \tv{a}, + \ol{S} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a}, \ol{Y} \lessdot \ol{N} }\\ \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T}) \\ & \mathbf{where}\ \begin{array}[t]{l} diff --git a/soundness.tex b/soundness.tex index 23fd93b..a95bee1 100644 --- a/soundness.tex +++ b/soundness.tex @@ -329,18 +329,17 @@ If there is a solution for a constraint set $C$, then there is also a solution f % does this really work. We have to show that the algorithm never gets stuck as long as there is a solution % maybe there are substitutions with types containing free variables that make additional solutions possible. Check! -\begin{lemma}\label{lemma:unifySoundness} -The \unify{} algorithm only produces correct output. +\begin{lemma}{\unify{} Soundness:}\label{lemma:unifySoundness} +\unify{}'s type solutions are correct respective to the subtyping rules defined in figure \ref{fig:subtyping}. \begin{description} \item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$ -%\item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$ -\item[Then] there exists a $\sigma'$ with: -$\sigma \subseteq \sigma'$ and -$\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$ -and $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$ where $\overline{\sigma(\type{S'}) = \wcNtype{\Delta}{N}}$, -otherwise $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \sigma'(\type{T'})}$ -% and $\sigma(\type{T'}) = \sigma(\type{T'})$. - +\item[Then] there exists a substitution $\sigma'$ and a set of types $\overline{\wcNtype{\Delta}{N}}$ with: +\begin{itemize} +\item $\sigma \subseteq \sigma'$ +\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$ +\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \wcNtype{\Delta}{N}}$ +\item $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$ +\end{itemize} \end{description} \end{lemma} diff --git a/unify.tex b/unify.tex index 722c814..c04af21 100644 --- a/unify.tex +++ b/unify.tex @@ -259,11 +259,8 @@ $ \end{figure} -The capture constraints are preserved when applying the \rulename{Upper} rule. -%because \texttt{let} statements like -%let x : X = v in -%can be transformed to -%let x : U = v in +%The capture constraints are preserved when applying the \rulename{Upper} rule. +% This is legal: a T List same(List a, List b){} - -% This program has no correct type. the same method requires -% \begin{lstlisting} -% List f; -% List problem(){ -% return same(problem(), problem()) ?: f; -% } -% \end{lstlisting} -% \begin{constraints} -% r <. List -% r <. List -% X.List <. r -% \end{constraints} -% %TODO - \unify{} generates wildcard types for constraints of the form $\type{N} \lessdot \tv{a}$ with the \rulename{\generalizeRule} rule. Otherwise only the wildcards already defined in the input constraints will be included in the result. \rulename{\generalizeRule} attempts to give $\tv{a}$ a more general type by replacing only the type parameters with fresh wildcards. @@ -1145,15 +1056,6 @@ need to be handled in a similiar fashion. The type variable $\tv{b}$ could either be a sub or a supertype of the type $\type{N}$. We have to consider both possibilities. \\[1em] -% The specification of the \unify{} algorithm has only two rules generating $\doteq$-Constraints -% , \rulename{Reduce} and \rulename{Ground}. -% $\doteq$-Constraints and the accompaning substitutions are dangerous respective to the soundness of the algorithm. -% For the soundness proof of the \unify{} algorithm we have to show every generation of equals constraints -% and the subsequent application of the \rulename{subst} rule is correct. -% We try to use them as sparsely as possible to simplify the soundness proof. -% You can notice this at \rulename{Equals} or \rulename{Force}: -% Instead of setting $\type{U} \doteq \type{L}$, we say -% $\type{U} \lessdot \type{L}, \type{L} \lessdot \type{U}$. \noindent \textbf{Step 3} @@ -1164,23 +1066,6 @@ If $C$ does not contain any wildcard variables the algorithm proceeds with step \begin{center} \fbox{ \begin{tabular}[t]{l@{~}l} -% \rulename{Remove} % kann beim Subst step gemacht werden und ist nur nötig wenn ein a =. T constraint mit wtv(T) > 1 entsteht -% & $ -% \begin{array}[c]{@{}ll} -% \begin{array}[c]{l} -% \wildcardEnv \vdash C \\ -% % \cup \, \set{ \wtv{a} \lessdot \type{T} }\\ -% \hline -% \vspace*{-0.4cm}\\ -% \subst{\tv{a}}{\wtv{a}}\wildcardEnv \vdash [\tv{a}/\wtv{a}]C -% \end{array} -% &\begin{array}[c]{l} -% \wtv{a} \in C \\ -% \tv{a} \ \text{fresh} -% \end{array} -% \end{array} -% $ -% \\\\ \rulename{Remove-Cons} & $ \begin{array}[c]{l} \wildcardEnv \vdash C \cup \set{\type{S} \lessdotCC \type{T} } \\ @@ -1192,23 +1077,6 @@ If $C$ does not contain any wildcard variables the algorithm proceeds with step \end{tabular}} \end{center} -% \textbf{Step 4:} -% If there are constraints of the form $(\tv{a} \lessdot \tv{b})$ remaining in the constraint set then -% apply the \rulename{Sub-Elim} rule and start over with step 1. -% Otherwise continue to step 5. -% \begin{center} -% \fbox{ -% \begin{tabular}[t]{l@{~}l} -% \rulename{SubElim} -% & $\begin{array}[c]{l} -% \wildcardEnv \vdash C \cup \set{\tv{a} \lessdot \tv{b}}\\ -% \hline -% [\tv{a}/\tv{b}]\wildcardEnv \vdash [\tv{a}/\tv{b}]C \cup \set{ \tv{b} \doteq \tv{a} } -% \end{array} -% $ -% \end{tabular}} -% \end{center} - \noindent \textbf{Step 4:} We apply the rules in figure \ref{fig:cleanup-rules} exhaustively and proceed with step 6. @@ -1242,43 +1110,6 @@ C \cup \set{ \tv{a} \doteq \bot } %\text{length}( \overline{\tv{a} \lessdot \type{T}} ) > 1 \end{array} \end{array}$ -% \\\\ % The force rule is unnecessary because every type placeholder has an upper bound Object (a <. Object) The match rule eliminates those wildcards -% \rulename{Force} &$ -% \begin{array}[c]{@{}ll} -% \begin{array}[c]{l} -% \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} -% \vdash C \cup \, \set{ -% \tv{a} \lessdot \type{N} } \\ -% \hline -% \vspace*{-0.4cm}\\ -% \wildcardEnv -% \vdash -% C \cup \, \set{ \tv{a} \lessdot [\type{U}/\rwildcard{X}]\type{N}, -% \type{U} \doteq \type{L} } -% \end{array} -% &\begin{array}[c]{l} -% \type{X} \in \text{fv}(\type{N}) \\ -% %\Delta' = \Delta \cup \set{\wildcard{X}{\type{U}}{\type{L}}} -% \end{array} -% \end{array}$ -% \\\\ -% \rulename{FlatOut} &$ -% \begin{array}[c]{@{}ll} -% \begin{array}[c]{l} -% \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} -% \vdash C \cup \, \set{ -% \tv{a} \lessdot \wcNtype{\Delta}{N} } \\ -% \hline -% \vspace*{-0.4cm}\\ -% \wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} -% \vdash -% C -% \end{array} -% &\begin{array}[c]{l} -% \type{X} \in \text{fv}(\wcNtype{\Delta}{N}) \\ -% \tv{a} \notin C , \, \tv{a} \notin \wildcardEnv, \tv{a} \notin \sigma -% \end{array} -% \end{array}$ \end{tabular}} \end{center} \caption{Cleanup rules}\label{fig:cleanup-rules}