System F

The type-variable context $\mathrm{\Delta }$ is a list of distinct variables; every type in $\mathrm{\Gamma }$ is formed under $\mathrm{\Delta }$. Formation and Church typing are the following complete rules.

$\cdot \mathsf{typectx}$

$\mathrm{\Delta }\mathsf{typectx}X\notin \mathrm{\Delta }$

$\mathrm{\Delta },X\mathsf{typectx}$

$\mathrm{\Delta }\mathsf{typectx}$

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

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

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

$X\in \mathrm{\Delta }$

$\mathrm{\Delta }⊢X\mathsf{type}$

$\mathrm{\Delta }⊢A\mathsf{type}$$\mathrm{\Delta }⊢B\mathsf{type}$

$\mathrm{\Delta }⊢A\to B\mathsf{type}$

$\mathrm{\Delta },X⊢A\mathsf{type}X\notin \mathrm{\Delta }$

$\mathrm{\Delta }⊢\mathrm{\forall }X.A\mathsf{type}$

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

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

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

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

$\mathrm{\Delta };\mathrm{\Gamma }⊢t:A\to B$$\mathrm{\Delta };\mathrm{\Gamma }⊢u:A$

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

$\mathrm{\Delta },X;\mathrm{\Gamma }⊢t:AX\notin \mathrm{\Delta }$

$\mathrm{\Delta };\mathrm{\Gamma }⊢\mathrm{\Lambda }X.t:\mathrm{\forall }X.A$

$\mathrm{\Delta };\mathrm{\Gamma }⊢t:\mathrm{\forall }X.A$$\mathrm{\Delta }⊢B\mathsf{type}$

$\mathrm{\Delta };\mathrm{\Gamma }⊢t[B]:A[B/X]$

The two compatible beta roots are $$(\lambda x:A.t)u{⟶}_{\beta }t[u/x],(\mathrm{\Lambda }X.t)[B]{⟶}_{\beta }t[B/X].$$ The relation ${⟶}_{\beta }$ is closed under both sides of application, the bodies of $\lambda$ and $\mathrm{\Lambda }$, and the operator of type application. Equivalently, from $t{⟶}_{\beta }{t}^{\prime }$ one may infer $$\begin{array}{c}\lambda x:A.t{⟶}_{\beta }\lambda x:A.t^{\prime },\mathrm{\Lambda }X.t{⟶}_{\beta }\mathrm{\Lambda }X.t^{\prime },t[B]{⟶}_{\beta }{t}^{\prime }[B],\\ tu{⟶}_{\beta }{t}^{\prime }u,ut{⟶}_{\beta }u{t}^{\prime }.\end{array}$$ The call-by-value subrelation instead uses $$v::=\lambda x:A.t\mid \mathrm{\Lambda }X.t,E::=[]\mid Et\mid vE\mid E[A],$$ closes the two beta roots only under $E$, and requires a value argument at the term-beta root. This is the operational system of definition 5.8. For confluence, the complete parallel beta relation is

$x{\Rrightarrow }_{\beta }x$

$s{\Rrightarrow }_{\beta }{s}^{\prime }$

$\lambda x:A.s{\Rrightarrow }_{\beta }\lambda x:A.s^{\prime }$

$s{\Rrightarrow }_{\beta }{s}^{\prime }$$u{\Rrightarrow }_{\beta }{u}^{\prime }$

$su{\Rrightarrow }_{\beta }{s}^{\prime }{u}^{\prime }$

$s{\Rrightarrow }_{\beta }{s}^{\prime }$

$\mathrm{\Lambda }X.s{\Rrightarrow }_{\beta }\mathrm{\Lambda }X.s^{\prime }$

$s{\Rrightarrow }_{\beta }{s}^{\prime }$

$s[A]{\Rrightarrow }_{\beta }{s}^{\prime }[A]$

$s{\Rrightarrow }_{\beta }{s}^{\prime }$$u{\Rrightarrow }_{\beta }{u}^{\prime }$

$(\lambda x:A.s)u{\Rrightarrow }_{\beta }{s}^{\prime }[u^{\prime }/x]$

$s{\Rrightarrow }_{\beta }{s}^{\prime }$

$(\mathrm{\Lambda }X.s)[A]{\Rrightarrow }_{\beta }{s}^{\prime }[A/X]$

For Curry System F, erase the annotations, $\mathrm{\Lambda }$, and type application from the term grammar. Its complete typing rules are

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

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

$\mathrm{\Delta };\mathrm{\Gamma },x:A{⊢}_{C}m:B$

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

$\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{C}m:A\to B$$\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{C}n:A$

$\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{C}mn:B$

$\mathrm{\Delta },X;\mathrm{\Gamma }{⊢}_{C}m:AX\notin \mathrm{\Delta }$

$\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{C}m:\mathrm{\forall }X.A$

$\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{C}m:\mathrm{\forall }X.A$$\mathrm{\Delta }⊢B\mathsf{type}$

$\mathrm{\Delta };\mathrm{\Gamma }{⊢}_{C}m:A[B/X]$

Chapter 6 changes none of these syntax, formation, typing, or reduction rules. Its relations live in the metatheory over closed typed beta-classes; the relational interpretation and abstraction theorem are therefore recorded in appendix C, appendix D rather than as a second object-language rule table.