fix type substitution

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