Syntactic categories.

macros.tex

@@ -105,10 +105,18 @@
 \newcommand{\CompCat}{\CatName{Comp}}
 \newcommand{\ValCat}{\CatName{Val}}
 \newcommand{\VarCat}{\CatName{Var}}
-\newcommand{\TypCat}{\CatName{Type}}
-\newcommand{\TyVarCat}{\CatName{TyVar}}
+\newcommand{\ValTypeCat}{\CatName{TVal}}
+\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

@@ -251,26 +251,42 @@ Section~\ref{sec:base-language-type-rules}.
 \label{sec:base-language-types}
 %
 \begin{figure}
-  \begin{syntax}
-    \slab{Value types}    &A,B  &::= & A \to C
-                                 \mid \alpha
+\begin{syntax}
+%     \slab{Value types}    &A,B  &::= & A \to C
+%                                  \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 [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
-  \end{syntax}
+                             \mid   \Record{R} \mid [R]
+                             \mid  \alpha \\
+\slab{Computation types\!\!}
+                      &C,D \in \CompTypeCat   &::= & A \eff E \\
+\slab{Effect types}   &E \in \EffectCat   &::= & \{R\}\\
+\slab{Row types}      &R \in \RowCat      &::= & \ell : P;R \mid \rho \mid \cdot \\
+\slab{Presence types\!\!\!\!\!} &P \in \PresenceCat  &::= & \Pre{A} \mid \Abs \mid \theta\\
+\\
+\slab{Types}          &T \in \TypeCat    &::= & A \mid C \mid E \mid R \mid P \\
+\slab{Kinds}          &K \in \KindCat    &::= & \Type \mid \Comp \mid \Effect \mid \Row_\mathcal{L} \mid \Presence \\
+\slab{Label sets}     &\mathcal{L} \in \LabelCat &::=& \emptyset \mid \{\ell\} \uplus \mathcal{L}\\\\
+
+\slab{Type environments} &\Gamma \in \TyEnvCat   &::=& \cdot \mid \Gamma, x:A \\
+\slab{Kind environments} &\Delta \in \KindEnvCat &::=& \cdot \mid \Delta, \alpha:K \\
+\end{syntax}
   \caption{Syntax of types, kinds, and their environments.}
   \label{fig:base-language-types}
 \end{figure}
@@ -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,61 @@ 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
-type $A$ if $x$ is bound to $A$ in the type environment $\Gamma$. The
-\tylab{Lam} rules states that a lambda value $(\lambda x.M)$ has type
-$A \to C$ if the computation $M$ has type $C$ assuming $x : A$. In the
-\tylab{PolyLam} rule we make use of the set of \emph{free type
-  variables} (FTV).
+\paragraph{Typing values} The \tylab{Var} rule states that a variable
+$x$ has type $A$ if $x$ is bound to $A$ in the type environment
+$\Gamma$. The \tylab{Lam} rules states that a lambda value
+$(\lambda x.M)$ has type $A \to C$ if the computation $M$ has type $C$
+assuming $x : A$. In the \tylab{PolyLam} rule we make use of the set
+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$,
-and the type structure:
+We define $\FTV$ by mutual induction over type environments, $\Gamma$,
+and the type structure, $T$, as follows.
 %
 \[
   \ba[t]{@{~}l@{~~~~~~}c@{~}l}
-\begin{eqs}
+  \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(\Record{R}) &\defas& \FTV(R)\\
-  % \FTV([R])      &\defas& \FTV(R)\\
+  \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)\\
   % \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([R])      &\defas& \FTV(R)\\
+  % \FTV(\Record{R}) &\defas& \FTV(R)\\
+  % \FTV(\{R\})    &\defas& \FTV(R)\\
+  \FTV &:& \RowCat \to \TyVarCat\\
   \FTV(l:P;R)    &\defas& \FTV(P) \cup \FTV(R)\\
-\end{eqs}\\\\
-\begin{eqs}
+  \FTV(\cdot)    &\defas& \emptyset\\\\
+
+  \FTV &:& \PresenceCat \to \TyVarCat\\
   \FTV(\theta)   &\defas& \{\theta\}\\
   \FTV(\Abs)     &\defas& \emptyset\\
-  \FTV(\Pre{A})  &\defas& \FTV(A)
-\end{eqs} & &
-\begin{eqs}
+  \FTV(\Pre{A})  &\defas& \FTV(A)\\
+\end{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,10 +738,12 @@ 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}
+    -[-/-] &:& \TypeCat \times \TypeCat \times \TyVarCat \to \TypeCat\\
     (A \to C)[B/\alpha] &\defas& A[B/\alpha] \to C[B/\alpha]\\
     \alpha[B/\beta]     &\defas& \begin{cases}
                                     B & \text{if } \alpha = \beta\\