PFPL Chapter 18 Higher Kinds

Posted on In Disqus:

This part is not shown on PFPL preview version.

Intros and Examples

Concept of type quantification leads to consideration of quantification over type constructors, which are functions mapping types to types.

For example, take queue here, the abstract type constructor can be expressed by existential type $\exists q::\text{T}\to\text{T}.\sigma$, where $\sigma$ is labeled tuple type and existential type $q\lbrack t\rbrack$ quantifies over kind $\text{T}\to\text{T}$.
$$
\begin{matrix}
\langle&&\text{emp}&&\hookrightarrow&&\forall t::\text{T}.t,&&\\
&&\text{ins}&&\hookrightarrow&&\forall t::\text{T}.t\times q\lbrack t\rbrack\to q\lbrack t\rbrack,&&\\
&&\text{rem}&&\hookrightarrow&&\forall t::\text{T}.q\lbrack t\rbrack\to(t\times q\lbrack t\rbrack)\space\text{opt}&&\rangle
\end{matrix}
$$
Language $\text{F}_\omega$ enriches language F with universal and existential quantification over kinds. This extension accounts for definitional equality of constructors.

Constructors and Kinds

The syntax of kinds and constructors of $\text{F}_\omega$ is given by grammar table
$$
\begin{align}
\text{Kind}&&\kappa&&::=&&\text{Type}&&\text{T}&&\text{types}\\
&&&&&&\text{Unit}&&1&&\text{nullary product}\\
&&&&&&\text{Prod}(\kappa_1;\kappa_2)&&\kappa_1\times\kappa_2&&\text{binary product}\\
&&&&&&\text{Arr}(\kappa_1;\kappa_2)&&\kappa_1\to\kappa_2&&\text{function}\\
\text{Con}&&c&&::=&&u&&u&&\text{variable}\\
&&&&&&\text{arr}&&\to&&\text{function constructor}\\
&&&&&&\text{all}\lbrace\kappa\rbrace&&\forall_\kappa&&\text{universal quantifier}\\
&&&&&&\text{some}\lbrace\kappa\rbrace&&\exists_\kappa&&\text{existential quantifier}\\
&&&&&&\text{proj}\lbrack\text{l}\rbrack(c)&&c\cdot\text{l}&&\text{first projection}\\
&&&&&&\text{proj}\lbrack\text{r}\rbrack(c)&&c\cdot\text{r}&&\text{second projection}\\
&&&&&&\text{app}(c_1;c_2)&&c_1\lbrack c_2\rbrack&&\text{application}\\
&&&&&&\text{unit}&&\langle\rangle&&\text{null tuple}\\
&&&&&&\text{pair}(c_1;c_2)&&\langle c_1,c_2\rangle&&\text{pair}\\
&&&&&&\text{lam}(u,c)&&\lambda(u)\space c&&\text{abstraction}
\end{align}
$$

The syntax of constructors follows the syntax of kinds in that there are introductions and elimination forms for all kinds:

  • The constants $\to$, $\forall_\kappa$, $\exists_\kappa$ are introduction forms for all kind $\text{T}$.
  • No elimination forms, since types are only used to classify expressions.

As for the three constants and the constructors of kind $\text{T}$

  • We use meta-variable $\tau$ for constructors of kind $\text{T}$.
  • $\tau_1\to\tau_2$ for application $\to\lbrack\tau_1\rbrack\lbrack\tau_2\rbrack$.
  • $\forall u::\kappa.\tau$ for $\forall_\kappa\lbrack\lambda(u::\kappa)\space\tau\rbrack$.
  • $\exists u::\kappa.\tau$ for $\exists_\kappa\lbrack\lambda(u::\kappa)\space\tau\rbrack$.

Statics

The statics of constructors and kinds for $\text{F}_\omega$ is specified by $\Delta\vdash c::\kappa$ stating constructor $c$ is well-formed with kind $\kappa$.

Hypotheses $\Delta$ consists of a finite set of assumptions $u_1::\kappa_1,\dots,u_n::\kappa_n$ where $n\geq 0$.

The statics of constructors is defined by the following rules
$$
\displaylines{\dfrac{}{\Delta,u::\kappa\vdash u::\kappa}\\
\dfrac{}{\Delta\vdash\to::\text{T}\to\text{T}\to\text{T}}\\
\dfrac{}{\Delta\vdash\forall_\kappa::(\kappa\to\text{T})\to\text{T}}\\
\dfrac{}{\Delta\vdash\exists_\kappa::(\kappa\to\text{T})\to\text{T}}\\
\dfrac{\Delta\vdash c::\kappa_1\times\kappa_2}{\Delta\vdash c\cdot\text{l}::\kappa_1}\\
\dfrac{\Delta\vdash c::\kappa_1\times\kappa_2}{\Delta\vdash c\cdot\text{r}::\kappa_2}\\
\dfrac{\Delta\vdash c_1::\kappa_2\to\kappa\phantom{“”}\Delta\vdash c_2::\kappa_2}{\Delta\vdash c_1\lbrack c_2\rbrack::\kappa}\\
\dfrac{}{\Delta\vdash\langle\rangle::1}\\
\dfrac{\Delta\vdash c_1::\kappa_1\phantom{“”}\Delta\vdash c_2::\kappa_2}{\Delta\vdash\langle c_1,c_2\rangle::\kappa_1\times\kappa_2}\\
\dfrac{\Delta,u::\kappa_1\vdash c_2::\kappa_2}{\Delta\vdash\lambda(u)\space e_2::\kappa_1\to\kappa_2}}
$$

Constructor Equality

Rules of definitional equality for $\text{F}_\omega$ define when two constructors, in particular two types, are interchangeable in ways of simplifications that can be performed to obtain one from the other.

Judgment $\Delta\vdash c_1\equiv c_2::\kappa$ states that $c_1$ and $c_2$ are definitionally equal constructors of kind $\kappa$.

When $\kappa$ is the kind $\text{T}$, constructors $c_1$ and $c_2$ are definitionally equal types.

Rules of definitional equality of constructors are defined by rules
$$
\displaylines{\dfrac{\Delta\vdash c::\kappa}{\Delta\vdash c\equiv c::\kappa}\\
\dfrac{\Delta\vdash c\equiv c’::\kappa}{\Delta\vdash c’\equiv c::\kappa}\\
\dfrac{\Delta\vdash c\equiv c’::\kappa\phantom{“”}\Delta\vdash c’\equiv c’’::\kappa}{\Delta\vdash c\equiv c’’::\kappa}\\
\dfrac{\Delta\vdash c\equiv c’::\kappa_1\times\kappa_2}{\Delta\vdash c\cdot\text{l}\equiv c’\cdot\text{l}::\kappa_1}\\
\dfrac{\Delta\vdash c\equiv c’::\kappa_1\times\kappa_2}{\Delta\vdash c\cdot\text{r}\equiv c’\cdot\text{r}::\kappa_1}\\
\dfrac{\Delta\vdash c_1\equiv c_1’::\kappa_1\phantom{“”}\Delta\vdash c_2\equiv c_2’::\kappa_2}{\Delta\vdash\langle c_1,c_2\rangle\equiv\langle c_1’,c_2’\rangle::\kappa_1\times\kappa_2}\\
\dfrac{\Delta\vdash c_1::\kappa_1\phantom{“”}\Delta\vdash c_2::\kappa_2}{\Delta\vdash\langle c_1,c_2\rangle\cdot\text{l}\equiv c_1::\kappa_1}\\
\dfrac{\Delta\vdash c_1::\kappa_1\phantom{“”}\Delta\vdash c_2::\kappa_2}{\Delta\vdash\langle c_1,c_2\rangle\cdot\text{r}\equiv c_2::\kappa_2}\\
\dfrac{\Delta\vdash c_1\equiv c_1’::\kappa_2\to\kappa\phantom{“”}\Delta\vdash c_2\equiv c_2’::\kappa_2}{\Delta\vdash c_1\lbrack c_2\rbrack\equiv c_1’\lbrack c_2’\rbrack::\kappa}\\
\dfrac{\Delta,u::\kappa\vdash c_2\equiv c_2’::\kappa_2}{\Delta\vdash\lambda(u:\kappa)\space c_2\equiv\lambda(u:\kappa)\space c_2’::\kappa\to\kappa_2}\\
\dfrac{\Delta,u::\kappa_1\vdash c_2::\kappa_2\phantom{“”}\Delta\vdash c_1::\kappa_1}{\Delta\vdash(\lambda(u:\kappa)\space c_2)\lbrack c_1\rbrack\equiv\lbrack c_1/u\rbrack c_2::\kappa_2}}
$$

The role played by definitional equality is to ensure that instances of type abstractor have same type by simplification.

Expressions and Types

The statics of expressions of $\text{F}_\omega$ is defined using two judgment forms
$$
\begin{cases}
\Delta\vdash\tau\text{ type}&\text{type formation}\\
\Delta\space\Gamma\vdash e:\tau&\text{expression formation}
\end{cases}
$$
where $\Gamma$ is a finite set of hypotheses of form $x_1:\tau_1,\dots,x_n:\tau_n$ such that $\Delta\vdash\tau_i\text{ type}$ for $1\le i\le k$.

The types of $\text{F}_\omega$ are the constructors of kind $\text{T}$ and this being the only rule of introducing types.
$$
\dfrac{\Delta\vdash\tau::\text{T}}{\Delta\vdash\tau\text{ type}}
$$
Definitional equality types classify the same expressions
$$
\dfrac{\Delta\space\Gamma\vdash e:\tau_1\phantom{“”}\Delta\vdash\tau_1\equiv\tau_2::\text{T}}{\Gamma\vdash e:\tau_2}
$$

  • Language $\text{F}_\omega$ extends F to permit universal quantification over arbitrary kinds
  • Language $\text{FE}_\omega$ extends $\text{F}_\omega$ with existential quantification over arbitrary kinds

Statics of quantifiers in $\text{FE}_\omega$ is defined by
$$
\displaylines{\dfrac{\Delta,u::\kappa\space\Gamma\vdash e:\tau}{\Delta\space\Gamma\vdash\Lambda(u::\kappa)\space e:\forall u::\kappa.\tau}\\
\dfrac{\Delta\space\Gamma\vdash e:\forall u::\kappa.\tau\phantom{“”}\Delta\vdash c::\kappa}{\Delta\space\Gamma\vdash e\lbrack c\rbrack:\lbrack c/u\rbrack\tau}\\
\dfrac{\Delta\vdash c::\kappa\phantom{“”}\Delta,u::\kappa\vdash\tau\text{ type}\phantom{“”}\Delta\space\Gamma\vdash e:\lbrack c/u\rbrack\tau}{\Delta\space\Gamma\vdash\text{pack }c\text{ with }e\text{ as }\exists u::\kappa.\tau:\exists u::\kappa.\tau}\\
\dfrac{\Delta\space\Gamma\vdash e_1:\exists u::\kappa.\tau\phantom{“”}\Delta,u::\kappa\space\Gamma,x:\tau\vdash e_2:\tau_2\phantom{“”}\Delta\vdash\tau_2\text{ type}}{\Delta\space\Gamma\vdash\text{open }e_1\text{ as }u::\kappa\text{ with }x:\tau\text{ in }e_2:\tau_2}}
$$

The equational dynamics of F carries over to $\text{F}_\omega$ without changing. One may or may not include definitional equality of constructor arguments since no rules depend on these in canonical form.

If there’s an observable type like nat in the transitional dynamics, there’s no need to simplify $c$ in $e\lbrack c\rbrack$ instantiation since it does not influence any evaluation of expressions of observable type.