Add TODO. Fix introduction example (WIP). Add explanation to UNify (WIP)
This commit is contained in:
Andreas Stadelmeier
parent
24cfd8cb75
commit
5bcffb7d70
@ -123,9 +123,9 @@ class Example {
|
||||
\begin{lstlisting}[style=fgj]
|
||||
genList() {
|
||||
if( ... ) {
|
||||
return new List<String>();
|
||||
return new List().add(1);
|
||||
} else {
|
||||
return new List<Integer>();
|
||||
return new List().add("String");
|
||||
}
|
||||
}
|
||||
\end{lstlisting}
|
||||
@ -137,9 +137,9 @@ genList() {
|
||||
\begin{lstlisting}[style=tfgj]
|
||||
List<?> genList() {
|
||||
if( ... ) {
|
||||
return new List<String>();
|
||||
return new Box<Integer>(1);
|
||||
} else {
|
||||
return new List<Integer>();
|
||||
return new Box<String>("String");
|
||||
}
|
||||
}
|
||||
\end{lstlisting}
|
||||
|
||||
22
martin.bib
22
martin.bib
@ -67,12 +67,22 @@ keywords = {subtyping, type inference, principal types}
|
||||
year={1965}}
|
||||
|
||||
@article{MM82,
|
||||
author={A. Martelli and U. Montanari},
|
||||
title={An Efficient Unification Algorithm},
|
||||
journal={ACM Transactions on Programming Languages and Systems},
|
||||
volume={4},
|
||||
pages={258-282},
|
||||
year={1982}}
|
||||
author = {Martelli, Alberto and Montanari, Ugo},
|
||||
title = {An Efficient Unification Algorithm},
|
||||
year = {1982},
|
||||
issue_date = {April 1982},
|
||||
publisher = {Association for Computing Machinery},
|
||||
address = {New York, NY, USA},
|
||||
volume = {4},
|
||||
number = {2},
|
||||
issn = {0164-0925},
|
||||
url = {https://doi.org/10.1145/357162.357169},
|
||||
doi = {10.1145/357162.357169},
|
||||
journal = {ACM Trans. Program. Lang. Syst.},
|
||||
month = {apr},
|
||||
pages = {258–282},
|
||||
numpages = {25}
|
||||
}
|
||||
|
||||
@InProceedings{Plue07_3,
|
||||
author = {Martin Pl{\"u}micke},
|
||||
|
||||
15
todo-11.4.24
Normal file
15
todo-11.4.24
Normal file
@ -0,0 +1,15 @@
|
||||
- Eingangsbeispiel
|
||||
- Motivation (gibt es ein nicht funktionierendes Beispiel für lokale Typinferenz was mit unserem algorithmus funktioniert)
|
||||
- Zeile 52 steht LetFJ, muss eingeführt werden
|
||||
- Operatoren motivieren. Denotable expressable types
|
||||
- Java macht es anders. es gibt keine let statements
|
||||
- In java kann ich die lets nur in bestimmter Weise einbauen. Die ANF Transformation macht aus TamedFJ das letFJ
|
||||
|
||||
- constraints nicht zu früh erwähnen
|
||||
- informal erwähnen. um capture conversion zu behandeln braucht es neue constraints
|
||||
- ganz vorne auflisten. Capture Conversion ist eine Neuheit
|
||||
|
||||
Figure 4 und 5 in ein Bild
|
||||
- man könnte die syntax unterlegen und sagen die unterlegten elemente fallen weg
|
||||
- in beiden Syntaxen die Methodendeklarationen sollen gleich sein. beides return benutzen
|
||||
- anschließend bei der convertierung zu TamedFJ nur die Änderungen beschreiben (Änderungen nur in Expressions)
|
||||
158
unify.tex
158
unify.tex
@ -1153,6 +1153,164 @@ $
|
||||
\label{fig:generation-rules}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}
|
||||
|
||||
\begin{center}
|
||||
\fbox{
|
||||
\begin{tabular}[t]{l@{~}l}
|
||||
\rulename{Equals} %TODO
|
||||
& $
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \vdash C \cup \, \set{ \wcNtype{\Delta}{N} \doteq \wcNtype{\Delta'}{N'} } \\
|
||||
\hline
|
||||
\vspace*{-0.4cm}\\
|
||||
\wildcardEnv \vdash C \cup \,
|
||||
\set{
|
||||
\wcNtype{\Delta}{N} \lessdot \wcNtype{\Delta'}{N'}, \wcNtype{\Delta'}{N'} \lessdot \wcNtype{\Delta}{N}
|
||||
}
|
||||
\end{array} %\quad |\Delta| = |\Delta'|
|
||||
% \quad \text{fv}(\type{N}) = \text{fv}(\type{N'}) = \emptyset
|
||||
$
|
||||
\\\\
|
||||
\ruleReduceWC{}
|
||||
&
|
||||
$
|
||||
\begin{array}[c]{@{}ll}
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \vdash
|
||||
C \cup \, \set{ \exptype{C}{\ol{S}} \lessdot
|
||||
\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}} } \\
|
||||
\hline
|
||||
\vspace*{-0.4cm}\\
|
||||
\wildcardEnv
|
||||
\vdash C \cup \, \set{
|
||||
\ol{\type{S}} \doteq [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{\type{T}},
|
||||
\ol{\wtv{a}} \lessdot [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{U}, [\ol{\wtv{a}}/\overline{\rwildcard{A}}]\ol{L} \lessdot \ol{\wtv{a}} }
|
||||
\end{array}
|
||||
%\quad \ol{Y} = \textit{fresh}(\ol{X})
|
||||
\quad \begin{array}[c]{l}
|
||||
\ol{\wtv{a}} \ \text{fresh}\\
|
||||
%\text{fv}(\exptype{C}{\ol{S}}) \subseteq \text{dom}(\overline{\wildcard{B}{\type{U'}}{\type{L'}}})
|
||||
%\text{dom}(\overline{\wildcard{A}{\type{U}}{\type{L}}}) \subseteq \text{fv}(\exptype{C}{\ol{T}}) \\
|
||||
%\text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset
|
||||
\end{array}
|
||||
\end{array}
|
||||
$
|
||||
\\\\
|
||||
\rulename{Capture}
|
||||
&
|
||||
$
|
||||
\begin{array}[c]{@{}ll}
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \vdash
|
||||
C \cup \, \set{ \wctype{\overline{\wildcard{B}{\type{U}}{\type{L}}}}{C}{\ol{S}} \lessdotCC \type{T} } \\
|
||||
\hline
|
||||
\vspace*{-0.4cm}\\
|
||||
\wildcardEnv \cup \overline{\wildcard{C}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{U}}{[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}]\type{L}}}
|
||||
\vdash C \cup \, \set{
|
||||
[\ol{\rwildcard{C}}/\ol{\rwildcard{B}}] \exptype{C}{\ol{S}} \lessdot \type{T} }
|
||||
\end{array}
|
||||
%\quad \ol{Y} = \textit{fresh}(\ol{X})
|
||||
\quad \begin{array}[c]{l}
|
||||
\ol{\rwildcard{C}} \ \text{fresh}\\
|
||||
%\text{fv}(\type{T}) \neq \emptyset
|
||||
\end{array}
|
||||
\end{array}
|
||||
$
|
||||
\\\\
|
||||
\rulename{Prepare} %The lessdotCC constraint only ensures that the left side looses its wildcardEnvironment.
|
||||
%It does not ensure that the left side doesn't contain free variables. If you want to ensure that you have to give the left side a normal placeholder
|
||||
&
|
||||
$
|
||||
\begin{array}[c]{@{}ll}
|
||||
\begin{array}[c]{l}
|
||||
\wildcardEnv \vdash
|
||||
C \cup \, \set{ \type{N} \lessdot \type{N'} } \\
|
||||
\hline
|
||||
\vspace*{-0.4cm}\\
|
||||
\wildcardEnv \vdash
|
||||
C \cup \, \set{ \type{N} \lessdotCC \type{N'} } \\
|
||||
\end{array}
|
||||
%\quad \ol{Y} = \textit{fresh}(\ol{X})
|
||||
\quad \begin{array}[c]{l}
|
||||
\text{fv}(\type{N'}) \subseteq \Delta_{in} \\
|
||||
\text{wtv}(\type{N'}) = \emptyset
|
||||
\end{array}
|
||||
\end{array}
|
||||
$
|
||||
\end{tabular}}
|
||||
\end{center}
|
||||
\caption{Type Reduction rules}\label{fig:reductionRules}
|
||||
\end{figure}
|
||||
|
||||
\subsection{Explanation}
|
||||
Our \unify{} process uses a similar concept to the standard unification by Martelli and Montanari \cite{MM82},
|
||||
consisting of terms, relations and variables.
|
||||
Instead of terms we have types of the form $\exptype{C}{\ol{T}}$ and
|
||||
the variables are called type placeholders.
|
||||
The input consist out of subtype relations.
|
||||
The goal is to find a solution (an unifier) which is a substitution for type placeholders
|
||||
which satisfies all input subtype constraints.
|
||||
|
||||
Types are reduced until they %either reach a discrepancy like $\type{String} \doteq \type{Integer}$
|
||||
reach a form like $\tv{a} \doteq \type{T}$.
|
||||
Afterwards \unify{} substitutes type placehodler $\tv{a}$ with $\type{T}$.
|
||||
This is done until a substitution for all type placehodlers and therefore a valid solution is reached.
|
||||
The reduction and substitutions are done in the first step of the algorithm.
|
||||
|
||||
%The type reduction is done by the rules in figure \ref{fig:reductionRules}
|
||||
|
||||
\unify{} cannot reduce constraints without checking a few prerequisites.
|
||||
Take the constraint $\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdot \exptype{C}{\wtv{a}}$ for example.
|
||||
If we apply a reduction here we get $\rwildcard{X} \doteq \wtv{a}$.
|
||||
The resulting $\sigma(\wtv{a}) = \rwildcard{X}$ seems like a correct substitution,
|
||||
but by S-Exists $\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \nless: \exptype{C}{\rwildcard{X}}$.
|
||||
Reason: Free variables on the right side of a subtype relations are not allowed to show up as bound variables on the left side.
|
||||
$\rwildcard{X}$ in this case.
|
||||
Therefore the \rulename{Reduce} rule only reduces constraints where the left side does not declare any wildcards.
|
||||
But if the right side neither contains wildcard type placeholders nor free variables the constraint can be reduced anyways.
|
||||
The \rulename{Prepare} rule then converts this constraint to a capture constraint.
|
||||
Afterwards the \rulename{Capture} rule removes the wildcard declarations on the left side an the constraint can be reduced.
|
||||
|
||||
\textit{Example} of the type reduction rules in figure \ref{fig:reductionRules} with the input
|
||||
$\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$
|
||||
The first step is the \rulename{Capture} rule.
|
||||
%The right side of the constraint does not contain any free variables.
|
||||
$\begin{array}{c}
|
||||
\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}\\
|
||||
\hline %Capture
|
||||
\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdotCC \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
|
||||
\end{array}$
|
||||
|
||||
\begin{NiceTabular}{l}
|
||||
$\ \wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}$ \\
|
||||
$\nextdeduction{
|
||||
\wctype{\rwildcard{X}}{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdotCC \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
|
||||
} $\\
|
||||
$\nextdeduction{
|
||||
\rwildcard{X} \vdash \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X}} \lessdot \exptype{Pair}{\wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \wtv{a}}
|
||||
} $\\
|
||||
$\nextdeduction{
|
||||
\rwildcard{X} \vdash \wctype{\rwildcard{Y}}{List}{\rwildcard{Y}} \doteq \wctype{\rwildcard{Y}}{List}{\rwildcard{Y}}, \rwildcard{X} \doteq \wtv{a}
|
||||
} $\\
|
||||
$\nextdeduction{
|
||||
\wildcard{X}{Object}{\type{String}} \vdash
|
||||
\type{String} \lessdot \mathcolorbox{addition}{\type{String}}, \tv{a} \doteq \rwildcard{X}
|
||||
} $\\
|
||||
$\nextdeduction{
|
||||
\wildcard{X}{Object}{\type{String}} \vdash
|
||||
\cancel{\type{String} \lessdot \rwildcard{X}}, \tv{a} \doteq \rwildcard{X}
|
||||
} $\\
|
||||
\CodeAfter
|
||||
\begin{tikzpicture}
|
||||
\node [right] at (2-|last) { \colorbox{white}{\rulename{Prepare}} } ;
|
||||
\node [right] at (3-|last) { \colorbox{white}{\rulename{Capture}} } ;
|
||||
\node [right] at (4-|last) { \colorbox{white}{\rulename{Reduce}} } ;
|
||||
\node [right] at (5-|last) { \colorbox{white}{\rulename{Equals}} } ;
|
||||
\node [right] at (6-|last) { \colorbox{white}{\rulename{Erase}} } ;
|
||||
\end{tikzpicture}
|
||||
\end{NiceTabular}
|
||||
|
||||
\subsection{Capture Conversion during Unification}
|
||||
The \unify{} algorithm applies a capture conversion when needed.
|
||||
A constraint of the form $\wcNtype{\Delta'}{N} \lessdot \type{T}$,
|
||||
|
||||
Loading…
Reference in New Issue
Block a user