From 518739f2911221b46550775df959a8cfa6f60c9a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Thu, 23 Jan 2020 15:03:18 +0000 Subject: [PATCH] Syntactic categories. --- macros.tex | 14 ++++-- thesis.tex | 141 ++++++++++++++++++++++++++++++++++++----------------- 2 files changed, 106 insertions(+), 49 deletions(-) diff --git a/macros.tex b/macros.tex index a504ca9..c734a9b 100644 --- a/macros.tex +++ b/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. diff --git a/thesis.tex b/thesis.tex index c69e975..bd2cb1f 100644 --- a/thesis.tex +++ b/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 - \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} +\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] + \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@{~~~~~~}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(\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\\