From cb1d5c056a4c5faadd0d41da4df906287df255fc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Fri, 3 Apr 2020 17:25:27 +0100 Subject: [PATCH] fix type substitution --- thesis.tex | 115 ++++++++++++++++++++++++++++++++++------------------- 1 file changed, 75 insertions(+), 40 deletions(-) diff --git a/thesis.tex b/thesis.tex index e74d5ff..32a6af7 100644 --- a/thesis.tex +++ b/thesis.tex @@ -593,6 +593,59 @@ to $\alpha$-conversion~\cite{Church32} of types. \] % +\paragraph{Type substitution} +We define a type substitution map, +$\sigma : (\TyVarCat \times \TypeCat)^\ast$ as list of pairs mapping a +type variable to its replacement. The domain of a substitution map is +set generated by projecting the first component, i.e. +% +\[ + \bl + \dom : (\TyVarCat \times \TypeCat)^\ast \to \TyVarCat\\ + \dom(\sigma) \defas \{ \alpha \mid (\alpha,\_) \in \sigma \} + \el +\] +% +The application of a type substitution map on a type term, written +$T\sigma$ for some type $T$, is defined inductively on the type +structure as follows. +% +\[ + \ba[t]{@{~}l@{~}c@{~}r} + \multicolumn{3}{c}{ + \begin{eqs} + (A \eff E)\sigma &\defas& A\sigma \eff E\sigma\\ + (A \to C)\sigma &\defas& A\sigma \to C\sigma\\ + (\forall \alpha^K.C)\sigma &\defas& \forall \alpha^K.C\sigma \quad \text{if } \alpha \notin \dom(\sigma)\\ + \alpha\sigma &\defas& \begin{cases} + A & \text{if } (\alpha,A) \in \sigma\\ + \alpha & \text{otherwise} + \end{cases} + \end{eqs}}\\ + \begin{eqs} + \Record{R}\sigma &\defas& \Record{R[B/\beta]}\\ + {[R]}\sigma &\defas& [R\sigma]\\ + \{R\}\sigma &\defas& \{R\sigma\}\\ + \cdot\sigma &\defas& \cdot\\ + \rho\sigma &\defas& \begin{cases} + R & \text{if } (\rho, R) \in \sigma\\ + \rho & \text{otherwise} + \end{cases}\\ + \end{eqs} + & ~~~~~~~~~~ & + \begin{eqs} + (\ell : P;R)\sigma &\defas& (\ell : P\sigma; R\sigma)\\ + \theta\sigma &\defas& \begin{cases} + P & \text{if } (\theta,P) \in \sigma\\ + \theta & \text{otherwise} + \end{cases}\\ + \Abs\sigma &\defas& \Abs\\ + \Pre{A}\sigma &\defas& \Pre{A\sigma} + \end{eqs} + \ea +\] +% + \paragraph{Types and their inhabitants} We now have the basic vocabulary to construct types in $\BCalc$. For instance, the signature of the standard polymorphic identity function @@ -680,6 +733,9 @@ above, an inhabitant of this type performs no effects of its own as the (right-most) effect row is a singleton row containing a distinct effect variable $\varepsilon'$. +\paragraph{Syntactic sugar} +Detail the syntactic sugar\dots + \subsection{Terms} \label{sec:base-language-terms} % @@ -702,7 +758,7 @@ effect variable $\varepsilon'$. \end{figure} % The syntax for terms is given in -Figure~\ref{fig:base-language-term-syntax}. We assume countably +Figure~\ref{fig:base-language-term-syntax}. We assume a countably infinite set of names $\VarCat$ from which we draw fresh variable names. We shall typically denote term variables by $x$, $y$, or $z$. % @@ -711,11 +767,11 @@ The syntax partitions terms into values and computations. Value terms comprise variables ($x$), lambda abstraction ($\lambda x^A . \, M$), type abstraction ($\Lambda \alpha^K . \, M$), and the introduction forms for records and variants. Records are -introduced using the empty record $\Record{}$ and record extension -$\Record{\ell = V; W}$, whilst variants are introduced using injection -$(\ell~V)^R$, which injects a field with label $\ell$ and value $V$ -into a row whose type is $R$. We include the row type annotation in -order to support bottom-up type reconstruction. +introduced using the empty record $(\Record{})$ and record extension +$(\Record{\ell = V; W})$, whilst variants are introduced using +injection $((\ell~V)^R)$, which injects a field with label $\ell$ and +value $V$ into a row whose type is $R$. We include the row type +annotation in to support bottom-up type reconstruction. All elimination forms are computation terms. Abstraction and type abstraction are eliminated using application ($V\,W$) and type @@ -741,8 +797,12 @@ kind information (term abstraction, type abstraction, injection, operations, and empty cases). However, we shall omit these annotations whenever they are clear from context. -\paragraph{Free variables} We define the function -$\FV : \TermCat \to \VarCat$ to compute the free variables of any +\paragraph{Free variables} A given term is said to be \emph{closed} if +every applied occurrence of a variable is preceded by some +corresponding binding occurrence. Any applied occurrence of a variable +that is not preceded by a binding occurrence is said be \emph{free + variable}. We define the function $\FV : \TermCat \to \VarCat$ +inductively on the term structure to compute the free variables of any given term. % \[ @@ -771,6 +831,12 @@ given term. \end{eqs} \el \] +% +The function computes the set of free variables bottom-up. Most cases +are homomorphic on the syntax constructors. The interesting cases are +those constructs which feature term binders: lambda abstraction, let +bindings, pair destructing, and case splitting. In each of those cases +we subtract the relevant binder(s) from the set of free variables. \subsection{Typing rules} \label{sec:base-language-type-rules} @@ -891,38 +957,7 @@ domain type of the abstractor agree. The type application rule \tylab{PolyApp} tells us that a type application $V\,A$ is well-typed whenever the abstractor term $V$ has the polymorphic type $\forall \alpha^K.C$ and the type $A$ has kind -$K$. This rule makes use of type substitution. We write $C[A/\alpha]$ -to mean substitute some type $A$ for some type variable $\alpha$ in -some type $C$. We define type substitution as a ternary function -defined as follows. -% -\[ - \begin{eqs} - -[-/-] &:& \TypeCat \times \TypeCat \times \TyVarCat \to \TypeCat\\ - (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& \forall \alpha^K.C[B/\beta] \quad \text{if } \alpha \neq \beta \text{ and } \alpha \notin \FTV(B)\\ - \alpha[B/\beta] &\defas& \begin{cases} - B & \text{if } \alpha = \beta\\ - \alpha & \text{otherwise} - \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} -\] +$K$. This rule makes use of type substitution. % The \tylab{Split} rule handles typing of record destructing. When splitting a record term $V$ on some label $\ell$ binding it to $x$ and