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

Describe tph helper function

Browse Source
This commit is contained in:
Andreas Stadelmeier 2023-12-27 19:03:25 +01:00
parent 8f3d49d70f
commit ab5f9d0f73
2 changed files with 11 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
prolog.tex
View File

@ -97,6 +97,8 @@
\newcommand{\localVarAssumption}{\ensuremath{\mathtt{\eta}}}
\newcommand{\expandLB}{\textit{expandLB}}
\newcommand{\tph}{\text{tph}}
\def\exptypett#1#2{\texttt{#1}\textrm{{\tt <#2}}\textrm{{\tt >}}\xspace}
\def\exp#1#2{#1(\,#2\,)\xspace}
\newcommand{\ldo}{, \ldots , }

11
unify.tex
View File

@ -522,7 +522,11 @@ The \rulename{Equals} rule is responsible for this.
\end{array}
\end{displaymath}
\textbf{Helper functions:}
\begin{description}
\item[$\tph{}$] returns all type placeholders inside a given type.
\textit{Example:} $\tph(\wctype{\wildcard{X}{\tv{a}}{\bot}}{Pair}{\wtv{b},\rwildcard{X}}) = \set{\tv{a}, \wtv{b}}$
\item [$\ll$ relation:]
The $\ll$ relation is the reflexive and transitive closure of the \texttt{extends} relations:
\begin{displaymath}
@ -676,10 +680,13 @@ This builds a search tree over multiple possible solutions.
%There are two different ways of handling a $\type{T} \lessdot \tv{a}$ constraint:
%TODO: why the \generalizeRule is basically the Same rule for regular type placeholders
%where is the mistake in the old unify algorithm?
%when working with equality the problems arise! Free variables should not escape their scope
% Replacing regular type placeholders causes problems related to method calls and capture conversion.
% <X> List<X> same(List<X> a, List<X> b){}
% This program has no correct type. the same method requires
% \begin{lstlisting}
% List<?> f;
% List<?> problem(){
@ -938,7 +945,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}
\text{tph}(\type{N}) = \emptyset, \text{fv}(\type{N}) = \emptyset \\
\tph(\type{N}) = \emptyset, \text{fv}(\type{N}) = \emptyset \\
\rwildcard{B} \ \text{fresh}, \tv{b} \notin \text{dom}(\sigma)
\end{array}
$
@ -963,7 +970,7 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
\set{\tv{a} \to \type{T} }
} \quad
\begin{array}{l}
\text{tph}(\type{T}) = \emptyset \\
\tph(\type{T}) = \emptyset \\
\tv{a} \notin \text{dom}(\sigma)
\end{array}
$