Remove Same rule. SameW rule is for both constraints
This commit is contained in:
Andreas Stadelmeier
parent
4b183937f5
commit
3a9f2d3e16
@ -560,23 +560,44 @@ During the course of the \unify{} algorithm more and more types emerge.
|
||||
As soon as enough type information is given \unify{} can conduct a capture conversion if needed.
|
||||
The constraints where this is possible are marked as capture constraints.
|
||||
|
||||
Type information flows top down.
|
||||
Argument types of a method invocation impact its return type.
|
||||
But knowing the return type does not imply distinct argument types.
|
||||
We know from the argument types of \texttt{receive} -which are given- that the \texttt{copy} method
|
||||
needs to return a type of the form $\exptype{Pair}{\type{X}, \type{Y}}$
|
||||
where \type{X} and \type{Y} can be any types as long as \type{Y} is a subtype of \type{X}.
|
||||
Without wildcards this would leave us with a clue what the type should look like.
|
||||
\section{Discussion Pair Example}
|
||||
We can make it work with a special rule in the \unify{}.
|
||||
But this will only help in this specific example and not generally solve the issue.
|
||||
A type $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ has atleast two immediate supertypes:
|
||||
$\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ and
|
||||
$\wctype{\rwildcard{X}, \rwildcard{Y}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$.
|
||||
Imagine a type $\exptype{Triple}{\rwildcard{X},\rwildcard{X},\rwildcard{X}}$ already has
|
||||
% TODO: how many supertypes are there?
|
||||
X.Triple<X,X,X> <: X,Y.Triple<X,Y,X> <:
|
||||
X,Y,Z.Triple<X,Y,Z>
|
||||
|
||||
%TODO: simplify this example. lSpeial <. List<x> and List<x> <. id is sufficient
|
||||
% The unify algorithm needs to resolve l <c List<x?> to l <. X.List<X>, X.List<X> <c List<x?>
|
||||
\begin{verbatim}
|
||||
<X> Pair<X,X> make(List<X> l){ ... }
|
||||
<X> boolean compare(Pair<X,X> p) { ... }
|
||||
|
||||
% this is not complete:
|
||||
l <c Pair<x?, y?>
|
||||
l <. X,Y.Pair<X,Y>, X,Y.Pair<X,Y> <. Pair<x?, y?>
|
||||
List<?> l;
|
||||
Pair<?,?> p;
|
||||
|
||||
compare(make(l)); // Valid
|
||||
compare(p); // Error
|
||||
\end{verbatim}
|
||||
|
||||
Our type inference algorithm is not able to solve this example.
|
||||
When we convert this to \TamedFJ{} and generate constraints we end up with:
|
||||
%TODO: Finish this example! does it work?
|
||||
\begin{lstlisting}[style=tamedfj]
|
||||
let x = l in let m = make(x) in compare(m)
|
||||
\end{lstlisting}
|
||||
\begin{constraints}
|
||||
|
||||
\end{constraints}
|
||||
|
||||
%TODO
|
||||
|
||||
\begin{lstlisting}[style=letfj]
|
||||
let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = l in let m = make(x) in compare(m)
|
||||
\end{lstlisting}
|
||||
|
||||
% if a x =. y emerge:
|
||||
X =. Y, which will delete both wildcards
|
||||
|
||||
|
||||
\end{itemize}
|
||||
|
||||
57
unify.tex
57
unify.tex
@ -402,23 +402,8 @@ which are used for the upper and lower bounds.
|
||||
% \end{array}
|
||||
% \end{displaymath}
|
||||
|
||||
%TODO new rules:
|
||||
% b <. List<x?>
|
||||
% ----------------
|
||||
% b =. bot | b <. List<x>
|
||||
|
||||
% b <. List<X>
|
||||
% ----------------
|
||||
% b =. bot | XU =. XL, a =. XU [a/X]C
|
||||
|
||||
% b =. C<X>
|
||||
% --------------
|
||||
% b =. X.C<X>
|
||||
% TODO: SameW rule can also be applied to normal type variables, because we have the contract rule now:
|
||||
|
||||
% a <c List<x?>
|
||||
% --------------
|
||||
% a <. X.List<X>, X.List<X> <c List<x?>
|
||||
% if there are a <. List<x?> constraints remaining in the end, then this can be a sign of a irregular input constraint set.
|
||||
|
||||
\begin{figure}
|
||||
\begin{center}
|
||||
@ -905,35 +890,35 @@ $\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \cap \Delta_{in}
|
||||
\begin{center}
|
||||
\fbox{
|
||||
\begin{tabular}[t]{l@{~}l}
|
||||
\rulename{SameW}
|
||||
\rulename{Same}
|
||||
& $
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \vdash
|
||||
C \cup \type{G} \lessdot \wtv{a}\\
|
||||
C \cup \type{G} \lessdot \tv{a}\\
|
||||
\hline
|
||||
\wildcardEnv \vdash
|
||||
C \cup \set{
|
||||
\wtv{a} \doteq \type{G}
|
||||
\tv{a} \doteq \type{G}
|
||||
}
|
||||
\end{array}
|
||||
$
|
||||
\\\\
|
||||
\cdashline{1-2} \\
|
||||
\rulename{Same}
|
||||
& $
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \cup \set{\overline{\wildcard{A}{\type{U}}{\type{L}}}} \vdash
|
||||
C \cup \wctype{\Delta'}{C}{\ol{X}} \lessdot \ntv{a}\\
|
||||
\hline
|
||||
\wildcardEnv \cup \set{\overline{\wildcard{A}{\type{U}}{\type{L}}}} \vdash
|
||||
C \cup \set{
|
||||
\ntv{a} \doteq \wctype{\Delta',\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{X}}
|
||||
}
|
||||
\end{array} \quad \begin{array}[c]{l}
|
||||
\text{fv}(\wctype{\Delta'}{C}{\ol{X}}) / \Delta_{in} = \overline{\rwildcard{A}}
|
||||
\end{array}
|
||||
$
|
||||
\\\\
|
||||
% \cdashline{1-2} \\
|
||||
% \rulename{Same}
|
||||
% & $
|
||||
% \begin{array}[c]{l}
|
||||
% \wildcardEnv \cup \set{\overline{\wildcard{A}{\type{U}}{\type{L}}}} \vdash
|
||||
% C \cup \wctype{\Delta'}{C}{\ol{X}} \lessdot \ntv{a}\\
|
||||
% \hline
|
||||
% \wildcardEnv \cup \set{\overline{\wildcard{A}{\type{U}}{\type{L}}}} \vdash
|
||||
% C \cup \set{
|
||||
% \ntv{a} \doteq \wctype{\Delta',\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{X}}
|
||||
% }
|
||||
% \end{array} \quad \begin{array}[c]{l}
|
||||
% \text{fv}(\wctype{\Delta'}{C}{\ol{X}}) / \Delta_{in} = \overline{\rwildcard{A}}
|
||||
% \end{array}
|
||||
% $
|
||||
% \\\\
|
||||
\cdashline{1-2} \\
|
||||
\rulename{\generalizeRule}
|
||||
& $
|
||||
@ -981,7 +966,7 @@ $\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \cap \Delta_{in}
|
||||
% $
|
||||
\\\\
|
||||
\cdashline{1-2} \\
|
||||
\rulename{\generalizeRule{}W}
|
||||
\rulename{\generalizeRule{}W} %TODO: Change description for step 2!
|
||||
& $
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \vdash C \cup \wctype{\Delta}{C}{\ol{T}} \lessdot \wtv{a}\\
|
||||
|
||||
Loading…
Reference in New Issue
Block a user