Commit 07c6e568 authored by Victor Lanvin's avatar Victor Lanvin
Browse files

Space saving

parent c019a305
......@@ -50,6 +50,9 @@ in particular $\recdel e \ell$ deletes the field $\ell$ from $e$, $\recupd e \el
To define record type subtyping and record expression type inference we need the following operators on record types (refer to~\citet{alainthesis} for more details):
\vspace{-2mm}
\begingroup
\allowdisplaybreaks
\begin{eqnarray}
\proj \ell t & = & \left\{\begin{array}{ll}\min \{ u \alt t\leq \orecord{\ell=u}\} &\text{if } t \leq \orecord{\ell = \Any}\\ \text{undefined}&\text{otherwise}\end{array}\right.\\
t_1 + t_2 & = & \min\left\{
......@@ -63,6 +66,7 @@ To define record type subtyping and record expression type inference we need the
\proj {\ell'} u \geq \proj {\ell'} t &\text{ otherwise}
\end{array}\right\}\right\}
\end{eqnarray}
\endgroup
Then two record types $t_1$ and $t_2$ are in subtyping relation, $t_1 \leq t_2$, if and only if for all $\ell \in \Labels$ we have $\proj \ell {t_1} \leq \proj \ell {t_2}$. In particular $\orecord{\!\!}$ is the largest record type.
Expressions are then typed by the following rules (already in algorithmic form).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment