From b2a2ca4bc4cd027b63bccd57cd999c88aa3eae11 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Thu, 23 Jan 2020 17:27:59 +0000 Subject: [PATCH] Type substitution. --- thesis.tex | 25 ++++++++++++++++++++++--- 1 file changed, 22 insertions(+), 3 deletions(-) diff --git a/thesis.tex b/thesis.tex index b61da4f..beab28e 100644 --- a/thesis.tex +++ b/thesis.tex @@ -745,14 +745,33 @@ defined as follows. \[ \begin{eqs} -[-/-] &:& \TypeCat \times \TypeCat \times \TyVarCat \to \TypeCat\\ - (A \to C)[B/\alpha] &\defas& A[B/\alpha] \to C[B/\alpha]\\ + (A \eff E)[B/\beta] &\defas& A[B/\beta] \eff E[B/\beta]\\ + (A \to C)[B/\beta] &\defas& A[B/\beta] \to C[B/\beta]\\ + (\forall \alpha^K.C)[B/\beta] &\defas& \begin{cases} + \forall \alpha^K.C & \text{if } \alpha = \beta\\ + \forall \alpha^K.C[B/\beta] & \text{otherwise} + \end{cases}\\ \alpha[B/\beta] &\defas& \begin{cases} B & \text{if } \alpha = \beta\\ \alpha & \text{otherwise} - \end{cases} + \end{cases}\\ + \Record{R}[B/\beta] &\defas& \Record{R[B/\beta]}\\ + {[R]}[B/\beta] &\defas& [R[B/\beta]]\\ + \{R\}[B/\beta] &\defas& \{R[B/\beta]\}\\ + \cdot[B/\beta] &\defas& \cdot\\ + \rho[B/\beta] &\defas& \begin{cases} + B & \text{if } \rho = \beta\\ + \rho & \text{otherwise} + \end{cases}\\ + (\ell : P;R)[B/\beta] &\defas& (\ell : P[B/\beta]; R[B/\beta])\\ + \theta[B/\beta] &\defas& \begin{cases} + B & \text{if } \rho = \beta\\ + \theta & \text{otherwise} + \end{cases}\\ + \Abs[B/\beta] &\defas& \Abs\\ + \Pre{A}[B/beta] &\defas& \Pre{A[B/\beta]} \end{eqs} \] -\dhil{Complete the implementation\dots} % The \tylab{Split} rule handles typing of record destructing. When splitting a record term $V$ on some label $\ell$ binding it to $x$ and