Higher-kinded polymorphism and existential packages

Kinds and constructors are Kind contexts contain distinct variables. The complete kinding rules are preceded by formation:

$\cdot \mathsf{kctx}$

$\mathrm{\Delta }\mathsf{kctx}$$u\notin \mathrm{dom}(\mathrm{\Delta })$

$\mathrm{\Delta },u::\kappa \mathsf{kctx}$

The kinding rules are

$(u::\kappa )\in \mathrm{\Delta }$

$\mathrm{\Delta }⊢u::\kappa$

$\mathrm{\Delta }⊢\mathbb{N}::\mathsf{Ty}$

$\mathrm{\Delta }⊢A::\mathsf{Ty}$$\mathrm{\Delta }⊢B::\mathsf{Ty}$

$\mathrm{\Delta }⊢A\to B::\mathsf{Ty}$

$\mathrm{\Delta }⊢A::\mathsf{Ty}$$\mathrm{\Delta }⊢B::\mathsf{Ty}$

$\mathrm{\Delta }⊢A\times B::\mathsf{Ty}$

$\mathrm{\Delta },u::\kappa ⊢A::\mathsf{Ty}$

$\mathrm{\Delta }⊢\mathrm{\forall }u::\kappa .A::\mathsf{Ty}$

$\mathrm{\Delta },u::\kappa ⊢A::\mathsf{Ty}$

$\mathrm{\Delta }⊢\mathrm{\exists }u::\kappa .A::\mathsf{Ty}$

$\mathrm{\Delta },u::{\kappa }_1⊢A::{\kappa }_2$

$\mathrm{\Delta }⊢\lambda u::{\kappa }_1.A::{\kappa }_1\to {\kappa }_2$

$\mathrm{\Delta }⊢A::{\kappa }_1\to {\kappa }_2$$\mathrm{\Delta }⊢B::{\kappa }_1$

$\mathrm{\Delta }⊢AB::{\kappa }_2$

Constructor one-step reduction is generated by constructor beta and the complete congruence family below:

$(\lambda u::\kappa .A)B{⟶}_{\beta }A[B/u]$

$A{⟶}_{\beta }{A}^{\prime }$

$AB{⟶}_{\beta }{A}^{\prime }B$

$B{⟶}_{\beta }{B}^{\prime }$

$AB{⟶}_{\beta }A{B}^{\prime }$

$A{⟶}_{\beta }{A}^{\prime }$

$(A\to B){⟶}_{\beta }(A^{\prime }\to B)$

$B{⟶}_{\beta }{B}^{\prime }$

$(A\to B){⟶}_{\beta }(A\to B^{\prime })$

$A{⟶}_{\beta }{A}^{\prime }$

$A\times B{⟶}_{\beta }{A}^{\prime }\times B$

$B{⟶}_{\beta }{B}^{\prime }$

$A\times B{⟶}_{\beta }A\times B^{\prime }$

$A{⟶}_{\beta }{A}^{\prime }$

$\lambda u::\kappa .A{⟶}_{\beta }\lambda u::\kappa .A^{\prime }$

$A{⟶}_{\beta }{A}^{\prime }$

$\mathrm{\forall }u::\kappa .A{⟶}_{\beta }\mathrm{\forall }u::\kappa .A^{\prime }$

$A{⟶}_{\beta }{A}^{\prime }$

$\mathrm{\exists }u::\kappa .A{⟶}_{\beta }\mathrm{\exists }u::\kappa .A^{\prime }$

Constructor equality is the equivalence and congruence generated by constructor beta. Its complete noncongruence rules are

$\mathrm{\Delta }⊢A::\kappa$

$\mathrm{\Delta }⊢A\equiv A::\kappa$

$\mathrm{\Delta }⊢A\equiv B::\kappa$

$\mathrm{\Delta }⊢B\equiv A::\kappa$

$\mathrm{\Delta }⊢A\equiv B::\kappa$$\mathrm{\Delta }⊢B\equiv C::\kappa$

$\mathrm{\Delta }⊢A\equiv C::\kappa$

$\mathrm{\Delta },u::{\kappa }_1⊢A::{\kappa }_2$$\mathrm{\Delta }⊢B::{\kappa }_1$

$\mathrm{\Delta }⊢(\lambda u::{\kappa }_1.A)B\equiv A[B/u]::{\kappa }_2$

The complete congruence family is

$\mathrm{\Delta }⊢A_1\equiv B_1::\mathsf{Ty}$$\mathrm{\Delta }⊢A_2\equiv B_2::\mathsf{Ty}$

$\mathrm{\Delta }⊢A_1\to A_2\equiv B_1\to B_2::\mathsf{Ty}$

$\mathrm{\Delta }⊢A_1\equiv B_1::\mathsf{Ty}$$\mathrm{\Delta }⊢A_2\equiv B_2::\mathsf{Ty}$

$\mathrm{\Delta }⊢A_1\times A_2\equiv B_1\times B_2::\mathsf{Ty}$

$\mathrm{\Delta },u::\kappa ⊢A\equiv B::\mathsf{Ty}$

$\mathrm{\Delta }⊢\mathrm{\forall }u::\kappa .A\equiv \mathrm{\forall }u::\kappa .B::\mathsf{Ty}$

$\mathrm{\Delta },u::\kappa ⊢A\equiv B::\mathsf{Ty}$

$\mathrm{\Delta }⊢\mathrm{\exists }u::\kappa .A\equiv \mathrm{\exists }u::\kappa .B::\mathsf{Ty}$

$\mathrm{\Delta },u::{\kappa }_1⊢A\equiv B::{\kappa }_2$

$\mathrm{\Delta }⊢\lambda u::{\kappa }_1.A\equiv \lambda u::{\kappa }_1.B::{\kappa }_1\to {\kappa }_2$

$\mathrm{\Delta }⊢A_1\equiv B_1::{\kappa }_1\to {\kappa }_2$$\mathrm{\Delta }⊢A_2\equiv B_2::{\kappa }_1$

$\mathrm{\Delta }⊢A_1{A}_2\equiv B_1{B}_2::{\kappa }_2$

The first line of the term grammar is the pure $F_{\omega }$ language of chapter 9; the second line is the package extension of chapter 10: Its complete typing table is formed over term contexts generated by

$\mathrm{\Delta }\mathsf{kctx}$

$\mathrm{\Delta }⊢\cdot \mathsf{ctx}$

$\mathrm{\Delta }⊢\mathrm{\Gamma }\mathsf{ctx}$$\mathrm{\Delta }⊢A::\mathsf{Ty}$$x\notin \mathrm{dom}(\mathrm{\Gamma })$

$\mathrm{\Delta }⊢\mathrm{\Gamma },x:A\mathsf{ctx}$

The typing rules are

$(x:A)\in \mathrm{\Gamma }$

$\mathrm{\Delta };\mathrm{\Gamma }⊢x:A$

$\mathrm{\Delta }⊢A::\mathsf{Ty}$$\mathrm{\Delta };\mathrm{\Gamma },x:A⊢e:B$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\lambda x:A.e:A\to B$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e_1:A\to B$$\mathrm{\Delta };\mathrm{\Gamma }⊢e_2:A$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e_1{e}_2:B$

$\mathrm{\Delta },u::\kappa ;\mathrm{\Gamma }⊢e:A$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathrm{\Lambda }u::\kappa .e:\mathrm{\forall }u::\kappa .A$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e:\mathrm{\forall }u::\kappa .A$$\mathrm{\Delta }⊢C::\kappa$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e[C]:A[C/u]$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e_1:A_1$$\mathrm{\Delta };\mathrm{\Gamma }⊢e_2:A_2$

$\mathrm{\Delta };\mathrm{\Gamma }⊢(e_1,e_2):A_1\times A_2$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e:A_1\times A_2$

$\mathrm{\Delta };\mathrm{\Gamma }⊢{\mathsf{pr}}_{i}e:A_i$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{0}:\mathbb{N}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e:\mathbb{N}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{suc}(e):\mathbb{N}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e:A$$\mathrm{\Delta }⊢A\equiv B::\mathsf{Ty}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e:B$

The existential rules, including the nonescape premise, are

$\mathrm{\Delta }⊢C::\kappa$$\mathrm{\Delta },u::\kappa ⊢A::\mathsf{Ty}$$\mathrm{\Delta };\mathrm{\Gamma }⊢e:A[C/u]$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{pack}[C,e]\mathsf{as}\mathrm{\exists }u::\kappa .A:\mathrm{\exists }u::\kappa .A$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e_1:\mathrm{\exists }u::\kappa .A$$\mathrm{\Delta },u::\kappa ;\mathrm{\Gamma },x:A⊢e_2:B$$\mathrm{\Delta }⊢B::\mathsf{Ty}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathsf{unpack}[u,x]=e_1\mathsf{in}{e}_2:B$

The last formation premise is the escape check: $u$ cannot occur free in $B$ because $B$ is formed before $u$ is added.

Call-by-value evaluation uses Deleting the final value and the final two context productions gives a context grammar equivalent to the complete pure congruence family of definition 11.7. The package chapter adds those productions without changing the order of the pure ones. The pure calculus has the three root contractions

$(\lambda x:A.e)v⟶e[v/x]$

$(\mathrm{\Lambda }u::\kappa .e)[C]⟶e[C/u]$

$i\in \{1,2\}$

${\mathsf{pr}}_i(v_1,v_2)⟶v_i$

Its complete congruence family is

$e_1⟶e_1^{\prime }$

$e_1{e}_2⟶e_1^{\prime }{e}_2$

$e_2⟶e_2^{\prime }$

$v_1{e}_2⟶v_1{e}_2^{\prime }$

$e⟶e^{\prime }$

$e[C]⟶e^{\prime }[C]$

$e_1⟶e_1^{\prime }$

$(e_1,e_2)⟶(e_1^{\prime },e_2)$

$e_2⟶e_2^{\prime }$

$(v_1,e_2)⟶(v_1,e_2^{\prime })$

$e⟶e^{\prime }$

${\mathsf{pr}}_{i}e⟶{\mathsf{pr}}_i{e}^{\prime }$

$e⟶e^{\prime }$

$\mathsf{suc}(e)⟶\mathsf{suc}(e^{\prime })$

The package-opening extension is $$\mathsf{unpack}[u,x]=(\mathsf{pack}[C,v]\mathsf{as}\mathrm{\exists }a::\kappa .A_0)\mathsf{in}e⟶e[C/u][v/x].$$ The contextual rule is $e⟶e^{\prime }\Rightarrow E⟨e⟩⟶E⟨e^{\prime }⟩$; there are no other call-by-value steps.

Compatible term beta is closed under every term constructor and has four roots: $$\begin{array}{c}(\lambda x:A.e)d{⟶}_{\beta }e[d/x],(\mathrm{\Lambda }u::\kappa .e)[C]{⟶}_{\beta }e[C/u],\\ {\mathsf{pr}}_i(e_1,e_2){⟶}_{\beta }{e}_i,\\ \mathsf{unpack}[u,x]=(\mathsf{pack}[C,d]\mathsf{as}\mathrm{\exists }a::\kappa .A_0)\mathsf{in}e{⟶}_{\beta }e[C/u][d/x].\end{array}$$

For the static fixed-record boundary used at the end of the chapter, extend the grammars by $$A::=\cdots \mid \{{\ell }_i:A_i{\}}_{i\in I},e::=\cdots \mid \{{\ell }_i=e_i{\}}_{i\in I}\mid e.\ell ,$$ where the finite label set contains no duplicates. The complete additional static rules are

$\mathrm{\Delta }⊢A_i::\mathsf{Ty}(i\in I)$

$\mathrm{\Delta }⊢\{{\ell }_i:A_i{\}}_{i\in I}::\mathsf{Ty}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e_i:A_i(i\in I)$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\{{\ell }_i=e_i{\}}_{i\in I}:\{{\ell }_i:A_i{\}}_{i\in I}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e:\{{\ell }_i:A_i{\}}_{i\in I}$$j\in I$

$\mathrm{\Delta };\mathrm{\Gamma }⊢e.{\ell }_j:A_j$

$\mathrm{\Delta }⊢A_i\equiv B_i::\mathsf{Ty}(i\in I)$

$\mathrm{\Delta }⊢\{{\ell }_i:A_i{\}}_{i\in I}\equiv \{{\ell }_i:B_i{\}}_{i\in I}::\mathsf{Ty}$

This record delta is static only; the chapter states no record dynamics.