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

Wildcard placeholders

Browse Source
This commit is contained in:
JanUlrich 2024-04-04 14:38:16 +02:00
parent 0c89f28b18
commit ed58017551
1 changed files with 14 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
unify.tex
View File

@ -110,6 +110,20 @@ gets the same wildcard twice.
% Free variables are not allowed to leave their scope. % Free variables are not allowed to leave their scope.
% This is ensured by type variables which are not allowed to be assigned type holding free variables. % This is ensured by type variables which are not allowed to be assigned type holding free variables.
\textbf{Wildcard Placeholders:}
The vital part are the \rulename{Subst} and \rulename{Normalize} rules.
They assert that a normal type placeholder is never replaced by a type containing free variables.
\rulename{Normalize} replaces Wildcard placeholders with normal placeholders right before they get substituted by \rulename{Subst}.
The idea is to keep the possibility of replacing a wildcard placeholder with a free variable as long as possible.
As soon as they appear in a $\ntv{a} \doteq \type{T}$ constraint they can no longer be replaced by free variables.
A type solution for a normal type placeholder will never contain free variables.
This is needed to guarantee well-formed type solutions and also keep free variables inside their scope.
\begin{lstlisting}
let y = { let x = v in v.get() } in y.get()
\end{lstlisting} %TODO: explain: here y has to be a type without free variables.
\subsection{Algorithm} \subsection{Algorithm}
\newcommand{\gtype}[1]{\type{#1}} \newcommand{\gtype}[1]{\type{#1}}