35 lines
1.9 KiB
TeX
35 lines
1.9 KiB
TeX
|
|
||
|
|
\section{Additional 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}}$
|
||
|
|
|
||
|
|
%\textbf{Wildcard renaming}\\
|
||
|
|
\item[Wildcard renaming:]
|
||
|
|
The \rulename{Reduce} rule separates wildcards from their environment.
|
||
|
|
At this point each wildcard gets a new and unique name.
|
||
|
|
To only rename the respective wildcards the reduce rule renames wildcards up to alpha conversion:
|
||
|
|
($[\ol{C}/\ol{B}]$ in the \rulename{reduce} rule)
|
||
|
|
\begin{align*}
|
||
|
|
[\type{A}/\type{B}]\type{B} &= \type{A} \\
|
||
|
|
[\type{A}/\type{B}]\type{C} &= \type{C} & \text{if}\ \type{B} \neq \type{C}\\
|
||
|
|
[\type{A}/\type{B}]\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} &= \wcNtype{\overline{\wildcard{X}{[\type{A}/\type{B}]\type{U}}{[\type{A}/\type{B}]\type{L}}}}{[\type{A}/\type{B}]N} & \text{if}\ \type{B} \notin \overline{\rwildcard{X}} \\
|
||
|
|
[\type{A}/\type{B}]\wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} &= \wcNtype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{N} & \text{if}\ \type{B} \in \overline{\rwildcard{X}} \\
|
||
|
|
\end{align*}
|
||
|
|
\item[Free Variables:]
|
||
|
|
The $\text{fv}$ function assumes every wildcard type variable to be a free variable aswell.
|
||
|
|
% TODO: describe a function which determines free variables? or do an example?
|
||
|
|
\begin{align*}
|
||
|
|
\text{fv}(\rwildcard{A}) &= \set{ \rwildcard{A} } \\
|
||
|
|
\text{fv}(\tv{a}) &= \emptyset \\
|
||
|
|
%\text{fv}(\wtv{a}) &= \set{\wtv{a}} \\
|
||
|
|
\text{fv}(\wctype{\Delta}{C}{\ol{T}}) &= \set{\text{fv}(\type{T}) \mid \type{T} \in \ol{T}} / \text{dom}(\Delta) \\
|
||
|
|
\end{align*}
|
||
|
|
|
||
|
|
\item[Fresh Wildcards:]
|
||
|
|
$\text{fresh}\ \overline{\wildcard{A}{\tv{u}}{\tv{l}}}$ generates fresh wildcards.
|
||
|
|
The new names $\ol{A}$ are fresh, aswell as the type variables $\ol{\tv{u}}$ and $\ol{\tv{l}}$,
|
||
|
|
which are used for the upper and lower bounds.
|
||
|
|
\end{description}
|