Remove adopt. Add Gen-X to Unify
This commit is contained in:
Andreas Stadelmeier
parent
c53f1b59af
commit
3d10421439
@ -106,6 +106,8 @@ $\texttt{let}\ \texttt{x} : \wcNtype{\Delta'}{N} = \texttt{e} \ \texttt{in}\
|
||||
|
||||
%TODO: show that this type exists \wcNtype{\Delta'}{N} (a \Delta' which only contains free variables of the type N)
|
||||
% and which is a supertype of T_r (so no free variables in T_r)
|
||||
% Solution: Make this a lemma and guarantee that Unify does only create types Delta.T with \Delta subset fv(T)
|
||||
% This is possible because free variables (except those in \Delta_in) are never used in wildcard environments
|
||||
|
||||
We could use unify to generate S by
|
||||
$\unify{}((\Delta, \Delta', \overline{\Delta}), [\ol{\tv{a}}/\ol{X}][\ol{\tv{b}}/\ol{Y}]\set{\ol{N} \lessdot \ol{T}, \type{N} \lessdot \exptype{C}{\ol{X}}})$
|
||||
@ -171,6 +173,17 @@ Method calls generate multiple constraints that share the same wildcard placehol
|
||||
% $\text{fv}(\type{T}) \subseteq \text{dom}(\Delta)$.
|
||||
% %UNIFY fails when there are free variables on the right side of a a =. T constraint
|
||||
|
||||
\begin{lemma}\label{lemma:unifyNoExcessWildcards}
|
||||
\begin{description}
|
||||
\item[If] $(\Delta, \sigma) = \unify{}(\Delta', C)$
|
||||
\item[Then] $\sigma(\tv{a}) = \wcNtype{\Delta''}{N} \implies \text{dom}(\Delta'') \subseteq \text{fv}(\type{N})$
|
||||
\end{description}
|
||||
\end{lemma}
|
||||
\textit{Proof:} Easy -
|
||||
All types given in the input to the \unify{} algorithm already comply with this requirement
|
||||
and none of the rules change.
|
||||
Note: the \rulename{Super} rule removes unnecessary wildcards.
|
||||
|
||||
\begin{lemma}\label{lemma:unifyWellFormedness}
|
||||
\unify{} generates well-formed types as long as well-formed types are supplied.
|
||||
\begin{description}
|
||||
|
||||
180
unify.tex
180
unify.tex
@ -28,6 +28,7 @@ Additional requirements:
|
||||
A constraint set containing the constraint $\tv{a} \lessdot \type{T}$ twice
|
||||
is a different to one that contains it only once.
|
||||
%\item every wildcard is bound to its enclosing type.
|
||||
\item All types have to be well-formed: $\wcNtype{\Delta}{N} \in C \implies \Delta_{in} \vdash \wcNtype{\Delta}{N} \ \ok$
|
||||
\item Naming scheme of every wildcard environment has to be the same.
|
||||
%TODO: We need this so that wildcard substitutions get the correct name. also the Equals rule needs this condition
|
||||
%Example:
|
||||
@ -402,24 +403,24 @@ Their upper and lower bounds are fresh type variables.
|
||||
\end{array}
|
||||
$
|
||||
\\\\
|
||||
\rulename{Adopt}
|
||||
& $
|
||||
\begin{array}[c]{@{}ll}
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \vdash C \cup \, \set{
|
||||
\tv{b} \lessdot \tv{a},
|
||||
\tv{a} \lessdot \type{N}, \tv{b} \lessdot \type{N'}} \\
|
||||
\hline
|
||||
\vspace*{-0.4cm}\\
|
||||
\wildcardEnv \vdash C \cup \, \set{
|
||||
\tv{b} \lessdot \type{N},
|
||||
\tv{b} \lessdot \tv{a},
|
||||
\tv{a} \lessdot \type{N} , \tv{b} \lessdot \type{N'}
|
||||
}
|
||||
\end{array}
|
||||
\end{array}
|
||||
$
|
||||
\\\\
|
||||
% \rulename{Adopt}
|
||||
% & $
|
||||
% \begin{array}[c]{@{}ll}
|
||||
% \begin{array}[c]{l}
|
||||
% \wildcardEnv \vdash C \cup \, \set{
|
||||
% \tv{b} \lessdot \tv{a},
|
||||
% \tv{a} \lessdot \type{N}, \tv{b} \lessdot \type{N'}} \\
|
||||
% \hline
|
||||
% \vspace*{-0.4cm}\\
|
||||
% \wildcardEnv \vdash C \cup \, \set{
|
||||
% \tv{b} \lessdot \type{N},
|
||||
% \tv{b} \lessdot \tv{a},
|
||||
% \tv{a} \lessdot \type{N} , \tv{b} \lessdot \type{N'}
|
||||
% }
|
||||
% \end{array}
|
||||
% \end{array}
|
||||
% $
|
||||
% \\\\
|
||||
\rulename{Adapt}
|
||||
&
|
||||
$
|
||||
@ -622,17 +623,45 @@ This builds a search tree over multiple possible solutions.
|
||||
\end{array}
|
||||
$
|
||||
\\\\
|
||||
\rulename{Subst-X}
|
||||
& $
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
|
||||
C \cup \rwildcard{X} \lessdot \tv{a}\\
|
||||
\hline
|
||||
\wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
|
||||
C \cup \set{
|
||||
\tv{a} \doteq \rwildcard{X}
|
||||
}
|
||||
\end{array} \quad \begin{array}[c]{l}
|
||||
\rwildcard{X} \in \Delta_{in}
|
||||
\end{array}
|
||||
$
|
||||
\\\\
|
||||
\rulename{Gen-X}
|
||||
& $
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
|
||||
C \cup \rwildcard{X} \lessdot \tv{a}\\
|
||||
\hline
|
||||
\wildcardEnv \cup \set{\wildcard{X}{\type{U}}{\type{L}}} \vdash
|
||||
C \cup \set{
|
||||
\type{U} \lessdot \tv{a}
|
||||
}
|
||||
\end{array}
|
||||
$
|
||||
\\\\
|
||||
\rulename{Super}
|
||||
& $
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \tv{a}\\
|
||||
\hline
|
||||
\wildcardEnv \vdash C \cup \set{ \wctype{\Delta}{D}{[\ol{T}/\ol{X}]\ol{N}} \lessdot \tv{a} }
|
||||
\wildcardEnv \vdash C \cup \set{ \wctype{\Delta'}{D}{[\ol{T}/\ol{X}]\ol{N}} \lessdot \tv{a} }
|
||||
%\set{\wctype{\ol{\wtype{W}}}{D}{[\ol{X}/\ol{Y}]\ol{Z}} \lessdot \tv{a}}
|
||||
\end{array} \quad
|
||||
\begin{array}{l}
|
||||
\texttt{class} \ \exptype{C}{\ol{X}} \triangleleft \exptype{D}{\ol{N}} \\
|
||||
\ol{X} \notin \wildcardEnv \cup \Delta
|
||||
\ol{X} \notin \wildcardEnv \cup \Delta,\, \Delta' = \Delta \cap \text{fv}([\ol{T}/\ol{X}]\ol{N})
|
||||
\end{array}
|
||||
$
|
||||
\\\\
|
||||
@ -749,105 +778,32 @@ $
|
||||
\end{tabular}}
|
||||
\end{center}
|
||||
|
||||
% \begin{figure}
|
||||
% \begin{center}
|
||||
% \fbox{
|
||||
% \begin{tabular}[t]{l@{~}l}
|
||||
% \rulename{Remove}
|
||||
% & $
|
||||
% \begin{array}[c]{@{}ll}
|
||||
% \begin{array}[c]{l}
|
||||
% \wildcardEnv \vdash C \\
|
||||
% % \cup \, \set{ \wtv{a} \lessdot \type{T} }\\
|
||||
% \hline
|
||||
% \vspace*{-0.4cm}\\
|
||||
% \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{Trim}
|
||||
% % & $
|
||||
% % \begin{array}[c]{@{}ll}
|
||||
% % \begin{array}[c]{l}
|
||||
% % \wildcardEnv \vdash C
|
||||
% % \cup \, \set{ \wcNtype{\Delta}{N} \lessdot \wctype{\Delta', \wildcard{B}{\type{U}}{\type{L}}}{C}{\ol{S}} }\\
|
||||
% % \hline
|
||||
% % \vspace*{-0.4cm}\\
|
||||
% % C \cup \, \set{ \wcNtype{\Delta}{N} \lessdot \wctype{\Delta'}{C}{\ol{S}} }
|
||||
% % \end{array}
|
||||
% % &\begin{array}[c]{l}
|
||||
% % \rwildcard{B} \notin \ol{S}
|
||||
% % \end{array}
|
||||
% % \end{array}
|
||||
% % $
|
||||
% % \\\\
|
||||
% \end{tabular}}
|
||||
% \end{center}
|
||||
% \caption{Wildcard variable substitution rules}\label{fig:wtv-rules}
|
||||
% \end{figure}
|
||||
|
||||
|
||||
% We apply the \rulename{Clean} rule exhaustively to $C''$:
|
||||
% \begin{gather*}
|
||||
% \begin{array}[c]{lll}
|
||||
% \rulename{Clean} &
|
||||
% \begin{array}[c]{l}
|
||||
% \wildcardEnv \vdash C\\
|
||||
% \hline
|
||||
% [\tv{a}/\wtv{a}]\wildcardEnv, [\tv{a}/\wtv{a}]\sigma \vdash [\tv{a}/\wtv{a}]C %\cup \set{\tv{b} \doteq \tv{a}}
|
||||
% \end{array}
|
||||
% \quad \wtv{a} \in C
|
||||
% \end{array}
|
||||
% \end{gather*}
|
||||
|
||||
% \begin{gather*}
|
||||
% \begin{array}[c]{lll}
|
||||
% \rulename{Subst} &
|
||||
% \begin{array}[c]{l}
|
||||
% \wildcardEnv \vdash C \cup \set{\tv{a} \doteq \wctype{\triangle}{C}{\ol{T}}}\\
|
||||
% \hline
|
||||
% [\wctype{\triangle}{C}{\ol{T}}/\tv{a}]\wildcardEnv \vdash [\wctype{\triangle}{C}{\ol{T}}/\tv{a}]
|
||||
% C \cup \set{\tv{a} \doteq \wctype{\triangle}{C}{\ol{T}}}
|
||||
% \end{array}
|
||||
% & \tv{a} \notin \ol{T} \\
|
||||
% & \\
|
||||
% \rulename{Subst-wc} &
|
||||
% \begin{array}[c]{l}
|
||||
% \wildcardEnv \vdash C \cup \set{\tv{a} \doteq \rwildcard{A}}\\
|
||||
% \hline
|
||||
% [\rwildcard{A}/\tv{a}]\wildcardEnv \vdash [\rwildcard{A}/\tv{a}] C \cup \set{\tv{a} \doteq \rwildcard{A}}
|
||||
% \end{array}
|
||||
% \end{array}
|
||||
% \end{gather*}
|
||||
|
||||
%or $\type{T}$ is not of the form $\wctype{\triangle}{C}{\ol{G}}$ with $\text{fv}(\ol{G}) = \emptyset$.
|
||||
%Here the $\text{fv}(\ol{G})$ also applies to type variables.
|
||||
%$\tv{x} \doteq \exptype{C}{\tv{a}}$ is invalid, because $\tv{a}$ could become a free wildcard in that context.
|
||||
\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 5.
|
||||
%and start over at step 1.
|
||||
%If the constraint set is in solved form afterwards the algorithm proceeds with step 5.
|
||||
\textbf{Step 5:}
|
||||
We apply the rules in figure \ref{fig:cleanup-rules} exhaustively and proceed with step 6.
|
||||
|
||||
\begin{figure}
|
||||
\begin{center}
|
||||
\leavevmode
|
||||
\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}
|
||||
$
|
||||
\\\\
|
||||
\rulename{Ground}
|
||||
& $\begin{array}[c]{@{}ll}
|
||||
\begin{array}[c]{l}
|
||||
@ -958,7 +914,7 @@ becomes $\exptype{List}{\type{String}}$.
|
||||
\end{description}
|
||||
|
||||
\noindent
|
||||
\textbf{Step 5 (Generating Result):}
|
||||
\textbf{Step 6 (Generating Result):}
|
||||
Apply the rules in figure \ref{fig:generation-rules} until $\wildcardEnv = \emptyset$ and $C = \emptyset$.
|
||||
The resulting $\Delta, \sigma$ is a correct solution.
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user