Type substitution.

macros.tex

@@ -105,10 +105,18 @@
 \newcommand{\CompCat}{\CatName{Comp}}
 \newcommand{\ValCat}{\CatName{Val}}
 \newcommand{\VarCat}{\CatName{Var}}
-\newcommand{\TypCat}{\CatName{Type}}
+\newcommand{\ValTypeCat}{\CatName{TVal}}
-\newcommand{\TyVarCat}{\CatName{TyVar}}
+\newcommand{\CompTypeCat}{\CatName{TComp}}
+\newcommand{\PresenceCat}{\CatName{Presence}}
+\newcommand{\TypeCat}{\CatName{Type}}
+\newcommand{\TyVarCat}{\CatName{TVar}}
 \newcommand{\KindCat}{\CatName{Kind}}
-\newcommand{\RowCat}{\RowCat}
+\newcommand{\RowCat}{\CatName{Row}}
+\newcommand{\EffectCat}{\CatName{Effect}}
+\newcommand{\TermCat}{\CatName{Term}}
+\newcommand{\LabelCat}{\CatName{Label}}
+\newcommand{\TyEnvCat}{\CatName{TyEnv}}
+\newcommand{\KindEnvCat}{\CatName{KindEnv}}
 
 %%
 %% Lindley's array stuff.

thesis.tex

@@ -252,24 +252,40 @@ Section~\ref{sec:base-language-type-rules}.
 %
 \begin{figure}
 \begin{syntax}
-    \slab{Value types}    &A,B  &::= & A \to C
+%     \slab{Value types}    &A,B  &::= & A \to C
-                                 \mid \alpha
+%                                  \mid \alpha
+%                                  \mid \forall \alpha^K.C
+%                                  \mid \Record{R}
+%                                  \mid [R]\\
+% \slab{Computation types}
+%                       &C,D  &::= & A \eff E \\
+% \slab{Effect types}   &E    &::= & \{R\}\\
+% \slab{Row types}      &R    &::= & \ell : P;R \mid \rho \mid \cdot \\
+% \slab{Presence types} &P    &::= & \Pre{A} \mid \Abs \mid \theta\\
+% %\slab{Labels}         &\ell &    &                \\
+% % \slab{Types}          &T    &::= & A \mid C \mid E \mid R \mid P \\
+% \slab{Kinds}          &K    &::= & \Type \mid \Row_\mathcal{L} \mid \Presence
+%                              \mid \Comp \mid \Effect \\
+% \slab{Label sets}     &\mathcal{L} &::=& \emptyset \mid \{\ell\} \uplus \mathcal{L}\\
+% %\slab{Type variables} &\alpha, \rho, \theta& \\
+% \slab{Type environments} &\Gamma &::=& \cdot \mid \Gamma, x:A \\
+% \slab{Kind environments} &\Delta &::=& \cdot \mid \Delta, \alpha:K
+\slab{Value types}    &A,B \in \ValTypeCat  &::= & A \to C
                              \mid  \forall \alpha^K.C
-                                 \mid \Record{R}
+                             \mid   \Record{R} \mid [R]
-                                 \mid [R]\\
+                             \mid  \alpha \\
-\slab{Computation types}
+\slab{Computation types\!\!}
-                      &C,D  &::= & A \eff E \\
+                      &C,D \in \CompTypeCat   &::= & A \eff E \\
-\slab{Effect types}   &E    &::= & \{R\}\\
+\slab{Effect types}   &E \in \EffectCat   &::= & \{R\}\\
-\slab{Row types}      &R    &::= & \ell : P;R \mid \rho \mid \cdot \\
+\slab{Row types}      &R \in \RowCat      &::= & \ell : P;R \mid \rho \mid \cdot \\
-\slab{Presence types} &P    &::= & \Pre{A} \mid \Abs \mid \theta\\
+\slab{Presence types\!\!\!\!\!} &P \in \PresenceCat  &::= & \Pre{A} \mid \Abs \mid \theta\\
-%\slab{Labels}         &\ell &    &                \\
+\\
-% \slab{Types}          &T    &::= & A \mid C \mid E \mid R \mid P \\
+\slab{Types}          &T \in \TypeCat    &::= & A \mid C \mid E \mid R \mid P \\
-\slab{Kinds}          &K    &::= & \Type \mid \Row_\mathcal{L} \mid \Presence
+\slab{Kinds}          &K \in \KindCat    &::= & \Type \mid \Comp \mid \Effect \mid \Row_\mathcal{L} \mid \Presence \\
-                             \mid \Comp \mid \Effect \\
+\slab{Label sets}     &\mathcal{L} \in \LabelCat &::=& \emptyset \mid \{\ell\} \uplus \mathcal{L}\\\\
-\slab{Label sets}     &\mathcal{L} &::=& \emptyset \mid \{\ell\} \uplus \mathcal{L}\\
+
-%\slab{Type variables} &\alpha, \rho, \theta& \\
+\slab{Type environments} &\Gamma \in \TyEnvCat   &::=& \cdot \mid \Gamma, x:A \\
-\slab{Type environments} &\Gamma &::=& \cdot \mid \Gamma, x:A \\
+\slab{Kind environments} &\Delta \in \KindEnvCat &::=& \cdot \mid \Delta, \alpha:K \\
-\slab{Kind environments} &\Delta &::=& \cdot \mid \Delta, \alpha:K
 \end{syntax}
   \caption{Syntax of types, kinds, and their environments.}
   \label{fig:base-language-types}
@@ -434,6 +450,21 @@ Kind and type environments are right-extended sequences of bindings. A
 kind environment binds type variables to their kinds, whilst a type
 environment binds term variables to their types.
 
+\paragraph{Type variable} The type structure has three syntactically
+distinct type variables (the kinding system gives us five semantically
+distinct notions of type variables). As we sometimes wish to refer
+collectively to type variables, we define the set of type variables,
+$\TyVarCat$, to be generated by:
+%
+\[
+  \TyVarCat \defas
+  \ba[t]{@{~}l@{~}l}
+         &\{ A \in \ValTypeCat  \mid A \text{ has the form } \alpha \}\\
+    \cup &\{ R \in \RowCat      \mid R \text{ has the form } \rho   \}\\
+    \cup &\{ P \in \PresenceCat \mid P \text{ has the form } \theta \}
+  \ea
+\]
+
 % Value types comprise the function type $A \to C$, whose domain
 % is a value type and its codomain is a computation type $B \eff E$,
 % where $E$ is an effect type detailing which effects the implementing
@@ -472,7 +503,8 @@ environment binds term variables to their types.
 \slab{Computations}  &M,N \in \CompCat  &::= & V\,W \mid V\,A\\
                      &                  &\mid& \Let\; \Record{\ell=x;y} = V \; \In \; N\\
                      &                  &\mid& \Case\; V \{\ell~x \mapsto M; y \mapsto N\} \mid \Absurd^C~V\\
-                     &                  &\mid& \Return~V \mid \Let \; x \revto M \; \In \; N
+                     &                  &\mid& \Return~V \mid \Let \; x \revto M \; \In \; N\\
+\slab{Terms}         &T \in \TermCat    &::= & x \mid V \mid M
 \end{syntax}
 
 \caption{Term syntax of \BCalc{}.}
@@ -539,7 +571,7 @@ Values
 % Polymorphic abstraction
   \inferrule*[Lab=\tylab{PolyLam}]
     {\typv{\Delta,\alpha : K;\Gamma}{M : C} \\
-     \alpha \notin FTV(\Gamma)
+     \alpha \notin \FTV(\Gamma)
     }
     {\typv{\Delta;\Gamma}{\Lambda \alpha^K .\, M : \forall \alpha^K . \,C}}
 \\
@@ -619,46 +651,62 @@ Figure~\ref{fig:base-language-type-rules}. In each typing rule, we
 implicitly assume that each type is well-kinded with respect to the
 kinding environment $\Delta$.
 
-\paragraph{Typing values} The \tylab{Var} rule states that a variable $x$ has
+\paragraph{Typing values} The \tylab{Var} rule states that a variable
-type $A$ if $x$ is bound to $A$ in the type environment $\Gamma$. The
+$x$ has type $A$ if $x$ is bound to $A$ in the type environment
-\tylab{Lam} rules states that a lambda value $(\lambda x.M)$ has type
+$\Gamma$. The \tylab{Lam} rules states that a lambda value
-$A \to C$ if the computation $M$ has type $C$ assuming $x : A$. In the
+$(\lambda x.M)$ has type $A \to C$ if the computation $M$ has type $C$
-\tylab{PolyLam} rule we make use of the set of \emph{free type
+assuming $x : A$. In the \tylab{PolyLam} rule we make use of the set
-  variables} (FTV).
+of \emph{free type variables} ($\FTV$) to ensure that we do not
+inadvertently capture a free type variable from the context.
 %
-We define FTV by mutual induction over type environments, $\Gamma$,
+We define $\FTV$ by mutual induction over type environments, $\Gamma$,
-and the type structure:
+and the type structure, $T$, as follows.
 %
 \[
   \ba[t]{@{~}l@{~~~~~~}c@{~}l}
+  \ba[t]{@{}l}
  \begin{eqs}
+  \FTV &:& \ValTypeCat \to \TyVarCat\\
   \FTV(\alpha)   &\defas& \{\alpha\}\\
   \FTV(\forall \alpha^K.C) &\defas& \FTV(C) \setminus \{\alpha\}\\
   \FTV(A \to C)  &\defas& \FTV(A) \cup \FTV(C)\\
   \FTV(A \eff E) &\defas& \FTV(A) \cup \FTV(E)\\
-  % \FTV(\{R\})    &\defas& \FTV(R)\\
+  \FTV(\{R\})    &\defas& \FTV(R)\\
-  % \FTV(\Record{R}) &\defas& \FTV(R)\\
+  \FTV(\Record{R}) &\defas& \FTV(R)\\
-  % \FTV([R])      &\defas& \FTV(R)\\
+  \FTV([R])      &\defas& \FTV(R)\\
   % \FTV(l:P;R)    &\defas& \FTV(P) \cup \FTV(R)\\
   % \FTV(\Pre{A})  &\defas& \FTV(A)\\
   % \FTV(\Abs)     &\defas& \emptyset\\
   % \FTV(\theta)   &\defas& \{\theta\}
-\end{eqs} & &
+\end{eqs}\ea & &
-\begin{eqs}
-  \FTV([R])      &\defas& \FTV(R)\\
-  \FTV(\Record{R}) &\defas& \FTV(R)\\
-  \FTV(\{R\})    &\defas& \FTV(R)\\
-  \FTV(l:P;R)    &\defas& \FTV(P) \cup \FTV(R)\\
-\end{eqs}\\\\
 \begin{eqs}
+  % \FTV([R])      &\defas& \FTV(R)\\
+  % \FTV(\Record{R}) &\defas& \FTV(R)\\
+  % \FTV(\{R\})    &\defas& \FTV(R)\\
+  \FTV &:& \RowCat \to \TyVarCat\\
+  \FTV(\cdot)    &\defas& \emptyset\\
+  \FTV(\rho)     &\defas& \{\rho\}\\
+  \FTV(l:P;R)    &\defas& \FTV(P) \cup \FTV(R)\\[1.0ex]
+
+  \FTV &:& \PresenceCat \to \TyVarCat\\
   \FTV(\theta)   &\defas& \{\theta\}\\
   \FTV(\Abs)     &\defas& \emptyset\\
-  \FTV(\Pre{A})  &\defas& \FTV(A)
+  \FTV(\Pre{A})  &\defas& \FTV(A)\\
-\end{eqs} & &
+\end{eqs}\\\\
-\begin{eqs}
+\multicolumn{3}{c}{\begin{eqs}
+    \FTV &:& \TyEnvCat \to \TyVarCat\\
   \FTV(\cdot)        &\defas& \emptyset\\
   \FTV(\Gamma,x : A) &\defas& \FTV(\Gamma) \cup \FTV(A)
-\end{eqs}
+\end{eqs}}
+% \begin{eqs}
+%   \FTV(\theta)   &\defas& \{\theta\}\\
+%   \FTV(\Abs)     &\defas& \emptyset\\
+%   \FTV(\Pre{A})  &\defas& \FTV(A)
+% \end{eqs} & &
+% \begin{eqs}
+%   \FTV(\cdot)        &\defas& \emptyset\\
+%   \FTV(\Gamma,x : A) &\defas& \FTV(\Gamma) \cup \FTV(A)
+% \end{eqs}
 \ea
 \]
 %
@@ -691,18 +739,39 @@ 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
+some type $C$. We define type substitution as a ternary function
+defined as follows.
 %
 \[
   \begin{eqs}
-    (A \to C)[B/\alpha] &\defas& A[B/\alpha] \to C[B/\alpha]\\
+    -[-/-] &:& \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& \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
@@ -790,7 +859,7 @@ $V$ for $x$ in some value $W$. We define substitution as a ternary
 function, whose signature is given by
 %
 \[
-\cdot[\cdot/\cdot] : (\CompCat + \ValCat) \times \ValCat \times \VarCat \to \CompCat,
+-[-/-] : \TermCat \times \ValCat \times \VarCat \to \CompCat,
 \]
 %
 and we realise it by pattern matching on the first argument.