stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Change = \emptyset to \subseteq Delta

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-01-31 18:05:42 +01:00
parent 921adc85b1
commit 4725943448
1 changed files with 8 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
unify.tex
View File

@ -189,7 +189,7 @@ $
\vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}, \wildcard{B}{U'}{L'}} \vdash C \cup \, \set{ \type{L} \doteq \type{U} , \type{U'} \doteq \type{L'}, \type{U} \doteq \type{U'} }
\end{array} \quad
\text{fv}(\type{U}, \type{U'}, \type{L}, \type{L'}) = \emptyset
\text{fv}(\type{U}, \type{U'}, \type{L}, \type{L'}) \subseteq \Delta_in
$
\\\\
\rulename{Tame}
@ -199,7 +199,7 @@ $
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \cup \set{\wildcard{A}{\type{U}}{\type{L}}} \vdash C \cup \, \set{ \type{L} \doteq \type{T}, \type{U} \doteq \type{T} }
\end{array} \quad \text{fv}(\type{U}, \type{L}) = \emptyset
\end{array} \quad \text{fv}(\type{U}, \type{L}) \subseteq \Delta_in
$
\\\\
% \rulename{Equals} %TODO
@ -397,7 +397,7 @@ Their upper and lower bounds are fresh type variables.
\end{array}
%\quad \ol{Y} = \textit{fresh}(\ol{X})
\quad \begin{array}[c]{l}
\text{fv}(\wctype{\Delta}{C}{\ol{S}}, \wctype{\Delta'}{C}{\ol{T}}) = \emptyset
\text{fv}(\wctype{\Delta}{C}{\ol{S}}, \wctype{\Delta'}{C}{\ol{T}}) \subseteq \Delta_in
\end{array}
\end{array}
$
@ -479,7 +479,7 @@ Starting with the \rulename{circle} rule. Afterwards the other rules in figure \
If we find an illicit constraint assigning a type containing free variables to a type placeholder not flagged as a wildcard placeholder the algorithm fails.
$\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \neq \emptyset$ $\implies$ fail!
$\set{\tv{a} \doteq \type{N}} \in C$ with $\text{fv}(\type{N}) \cap \Delta_in \neq \emptyset$ $\implies$ fail!
The first step of the algorithm is able to remove wildcards.
Removing a wildcard works by setting its lower and upper bound to be equal.
@ -736,7 +736,7 @@ If $C$ does not contain any wildcard variables the algorithm proceeds with step
\tv{a} \ \text{fresh}
\end{array}
\end{array}
$
$
\\\\
\rulename{Remove-Cons} & $
\begin{array}[c]{l}
@ -967,7 +967,7 @@ For this step to succeed there should only be four kinds of constraints left.
%\item\label{item:3} $\tv{a} \lessdot \tv{b}$ %, with $a$ and $b$ both isolated type variables
\item $\tv{a} \doteq \tv{b}$
%\item $\wtv{a} \doteq \type{G}$
\item\label{item:1} $\tv{a} \lessdot \wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}$, with $\text{fv}(\wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}) = \emptyset$
\item\label{item:1} $\tv{a} \lessdot \wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}$, with $\text{fv}(\wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}) \subseteq \Delta_in$
\item\label{item:2} $\tv{a} \doteq \wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}$, with $\tv{a} \notin \ol{\type{T}}$ % and $\text{fv}(\wctype{\ol{\wtype{W}}}{C}{\ol{\type{T}}}) = \emptyset$
\item\label{item:3} $\tv{a} \doteq \rwildcard{X}$
\end{enumerate}
@ -1008,7 +1008,7 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
\wildcardEnv \vdash [\type{B}/\tv{b}]C \implies \Delta \cup \set{\wildcard{B}{\type{N}}{\bot}}, \sigma \cup \set{\tv{b} \to \type{B}}
} \quad
\begin{array}{l}
\tph(\type{N}) = \emptyset, \text{fv}(\type{N}) \subseteq \Delta \\
\tph(\type{N}) = \emptyset, \text{fv}(\type{N}) \subseteq \Delta \cup \Delta_in \\
\rwildcard{B} \ \text{fresh}, \tv{b} \notin \text{dom}(\sigma), \Delta \vdash \type{N} \ \ok
\end{array}
$
@ -1041,7 +1041,7 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
} \quad
\begin{array}{l}
\tph(\type{T}) = \emptyset \\ %,\, \text{fv}(\type{T}) \subseteq \Delta \\ % T ok implies that
\tv{a} \notin \text{dom}(\sigma),\, \Delta \vdash \type{T} \ \ok
\tv{a} \notin \text{dom}(\sigma),\, \Delta, \Delta_in \vdash \type{T} \ \ok
\end{array}
$
\\\\