|
|
|
@ -6001,20 +6001,20 @@ 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 variables} 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 |
|
|
|
\] |
|
|
|
% \paragraph{Type variables} 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$, |
|
|
|
|
