# System F$$_\omega^{++}$$

$$F_\omega$$ is the calculus of higher-kinded type constructors, combining two axes of the lambda cube (polymorphism and type operators).

The syntax of $$F_\omega$$ is an extension of $$F$$. First, we need to adjust our syntax to use type constructors (or just "constructors") instead of just types. By convention, we will use $$\tau$$ to denote a nullary constructor, a constructor kinded at $$*$$ (see below).

$\require{bussproofs} c, \tau := \alpha \mid c \rightarrow c \mid \forall (\alpha : k).c \mid \lambda (\alpha : k) .c \mid c\ c$

where $$\alpha$$ is a type variable used in quantification and type abstraction.

Next, we will add $$k$$, to denote kinds:

$k := * \mid k \rightarrow k$

We also need terms to inhabit those types:

$e := x \mid \lambda (x:\tau).e \mid \Lambda(\alpha:k).e \mid e[\tau]$

Our context, $$\Gamma$$, may contain judgments about types and terms.

$\Gamma := \cdot \mid \Gamma, x:\tau \mid \Gamma : \alpha:k$

You may also see the kinding judgment written as $$\alpha :: k$$.

Finally, as noted earlier, we will need to extend $$F_\omega$$ with primitive product kinds to handle ML modules (hence the ++ in $$F_\omega^{++}$$):

\begin{aligned} k &:= \dots \mid k \times k \\ c &:= \dots \mid \langle c, c \rangle \mid \pi_1 c \mid \pi_2 c \end{aligned}

This language is defined statically as follows:

Rules 1.1 (Kinding): $$\Gamma \vdash c:k$$

$\begin{prooftree} \AxiomC{\Gamma(\alpha) = k} \UnaryInfC{\Gamma \vdash \alpha : k} \end{prooftree} \qquad \begin{prooftree} \AxiomC{\Gamma \vdash c_1:*} \AxiomC{\Gamma \vdash c_2:*} \BinaryInfC{\Gamma \vdash c_1 \rightarrow c_2 : *} \end{prooftree} \qquad \begin{prooftree} \AxiomC{\Gamma, \alpha:k \vdash c:*} \UnaryInfC{\Gamma \vdash \forall(\alpha:k).c:*} \end{prooftree}$ $\begin{prooftree} \AxiomC{\Gamma \vdash c_1:k \rightarrow k'} \AxiomC{\Gamma \vdash c_2:k} \BinaryInfC{\Gamma \vdash c_1\ c_2 : k'} \end{prooftree} \qquad \begin{prooftree} \AxiomC{\Gamma, \alpha:k \vdash c:k'} \UnaryInfC{\Gamma \vdash \lambda (\alpha:k).c : k \rightarrow k'} \end{prooftree}$ $\begin{prooftree} \AxiomC{\Gamma \vdash c_1:k_1} \AxiomC{\Gamma \vdash c_2:k_2} \BinaryInfC{\Gamma \vdash \langle c_1, c_2 \rangle : k_1 \times k_2} \end{prooftree}\qquad \begin{prooftree} \AxiomC{\Gamma \vdash c:k_1 \times k_2} \UnaryInfC{\Gamma \vdash \pi_1 c : k_1} \end{prooftree}\qquad \begin{prooftree} \AxiomC{\Gamma \vdash c:k_1 \times k_2} \UnaryInfC{\Gamma \vdash \pi_2 c : k_2} \end{prooftree}$

Rules 1.2 (Typing): $$\Gamma \vdash e:\tau$$

$\begin{prooftree} \AxiomC{\Gamma(x) = \tau} \UnaryInfC{\Gamma \vdash x:\tau} \end{prooftree}\qquad \begin{prooftree} \AxiomC{\Gamma, x:\tau \vdash e:\tau'} \AxiomC{\Gamma \vdash \tau:*} \BinaryInfC{\Gamma \vdash \lambda(x:\tau).e : \tau \rightarrow \tau'} \end{prooftree}\qquad \begin{prooftree} \AxiomC{\Gamma, \vdash e_1:\tau \rightarrow \tau'} \AxiomC{\Gamma \vdash e_2:\tau} \BinaryInfC{\Gamma \vdash e_1\ e_2 : \tau'} \end{prooftree}$ $\begin{prooftree} \AxiomC{\Gamma, \alpha:k \vdash e:\tau} \UnaryInfC{\Gamma \vdash \Lambda(\alpha:k).e : \forall(\alpha:k).\tau} \end{prooftree}\qquad \begin{prooftree} \AxiomC{\Gamma \vdash e:\forall(\alpha:k).\tau'} \AxiomC{\Gamma \vdash \tau:k} \BinaryInfC{\Gamma \vdash e[\tau] : [\tau/\alpha]\tau'} \end{prooftree}$

Note that these rules aren't sufficient -- If we have $$f : \forall(\beta:* \rightarrow *). \beta\ \texttt{int} \rightarrow \texttt{unit}$$, we'd want to have $$f[\lambda(\alpha:*).\alpha]\ 12 : \texttt{unit}$$. However, by the above rules, we type $$f[\lambda(\alpha:*):\alpha]$$ at $$((\lambda \alpha.\alpha) \ \texttt{int}) \rightarrow \texttt{unit}$$, not $$\texttt{int} \rightarrow \texttt{unit}$$.

To remedy this, we need some way to express that $$(\lambda \alpha.\alpha) \ \texttt{int}$$ is equivalent to $$\texttt{int}$$, which we will accomplish by defining a new judgment $$\Gamma \vdash c \equiv c' : k$$, then adding to rules 1.2 the equivalence rule

$\begin{prooftree} \AxiomC{\Gamma \vdash e:\tau} \AxiomC{\Gamma \vdash \tau \equiv \tau':*} \BinaryInfC{\Gamma \vdash e:\tau'} \end{prooftree}$

Rules 1.3 (Constructor Equivalence): $$\Gamma \vdash c \equiv c':k$$

Equivalence $\begin{prooftree} \AxiomC{\Gamma \vdash c:k} \UnaryInfC{\Gamma \vdash c \equiv c:k} \end{prooftree} \qquad \begin{prooftree} \AxiomC{\Gamma \vdash c \equiv c':k} \UnaryInfC{\Gamma \vdash c' \equiv c:k} \qquad \end{prooftree} \qquad \begin{prooftree} \AxiomC{\Gamma \vdash c_1 \equiv c_2:k} \AxiomC{\Gamma \vdash c_2 \equiv c_3:k} \BinaryInfC{\Gamma \vdash c_1 \equiv c_3:k} \end{prooftree}$

Compatibility $\begin{prooftree} \AxiomC{\Gamma \vdash \tau_1 \equiv \tau_1' : *} \AxiomC{\Gamma \vdash \tau_2 \equiv \tau_2' : *} \BinaryInfC{\Gamma \vdash \tau_1 \rightarrow \tau_2 \equiv \tau_1' \rightarrow \tau_2' : *} \end{prooftree}\qquad \begin{prooftree} \AxiomC{\Gamma, \alpha:k \vdash \tau \equiv \tau' : *} \UnaryInfC{\Gamma \vdash \forall(\alpha:k).\tau \equiv \forall(\alpha:k).\tau':*} \end{prooftree}$ $\begin{prooftree} \AxiomC{\Gamma, \alpha:k \vdash c \equiv c':k'} \UnaryInfC{\Gamma \vdash \lambda(\alpha:k).c \equiv \lambda(\alpha:k).c': k \rightarrow k'} \end{prooftree} \qquad \begin{prooftree} \AxiomC{\Gamma, \alpha:k \vdash c_1 \equiv c_1':k \rightarrow k'} \AxiomC{\Gamma \vdash c_2 \equiv c_2':k} \BinaryInfC{\Gamma \vdash c_1\ c_2 \equiv c_1'\ c_2':k'} \end{prooftree}$ $\begin{prooftree} \AxiomC{\Gamma \vdash c_1 \equiv c_1':k_1} \AxiomC{\Gamma \vdash c_2 \equiv c_2':k_2} \BinaryInfC{\Gamma \vdash \langle c_1, c_2 \rangle \equiv \langle c_1', c_2' \rangle : k_1 \times k_2} \end{prooftree}$ $\begin{prooftree} \AxiomC{\Gamma \vdash c \equiv c' : k_1 \times k_2} \UnaryInfC{\Gamma \vdash \pi_1c \equiv \pi_1c' : k_1} \end{prooftree}\qquad \begin{prooftree} \AxiomC{\Gamma \vdash c \equiv c' : k_1 \times k_2} \UnaryInfC{\Gamma \vdash \pi_2c \equiv \pi_2c' : k_2} \end{prooftree}$

Reduction/beta $\begin{prooftree} \AxiomC{\Gamma, \alpha:k \vdash c:k'} \AxiomC{\Gamma \vdash c':k} \BinaryInfC{\Gamma \vdash (\lambda (\alpha:k).c)\ c' \equiv [c'/\alpha]c:k'} \end{prooftree}$ $\begin{prooftree} \AxiomC{\Gamma \vdash c_1:k_1} \UnaryInfC{\Gamma \vdash \pi_1\langle c_1, c_2\rangle \equiv c_1:k_1} \end{prooftree}\qquad \begin{prooftree} \AxiomC{\Gamma \vdash c_2:k_2} \UnaryInfC{\Gamma \vdash \pi_2\langle c_1, c_2\rangle \equiv c_2:k_2} \end{prooftree}$

Extensionality/eta $\begin{prooftree} \AxiomC{\Gamma \vdash c:k_1 \rightarrow k_2} \AxiomC{\Gamma \vdash c':k_1 \rightarrow k_2} \AxiomC{\Gamma, \alpha:k_1 \vdash c\ \alpha \equiv c'\ \alpha:k_2} \TrinaryInfC{\Gamma \vdash c \equiv c' : k_1 \rightarrow k_2} \end{prooftree}$ $\begin{prooftree} \AxiomC{\Gamma \vdash \pi_1 c \equiv \pi_1 c':k_1} \AxiomC{\Gamma \vdash \pi_2 c \equiv \pi_2 c':k_2} \BinaryInfC{\Gamma \vdash c \equiv c':k_1 \times k_2} \end{prooftree}$

Note that in many cases, we enforce that some constructors are types (kind $$*$$) -- we certainly can't have tuples or lambda abstractions underlying a $$\forall$$ type, for example.

The first set of rules, labeled "equivalence", ensure that this is indeed an equivalence/congruence relation.

The beta rules are the interesting ones. With them, we can prove (assuming we've defined the relevant primitive types):

$\begin{prooftree} \AxiomC{} \UnaryInfC{\vdash \texttt{int}:*} \AxiomC{} \UnaryInfC{\beta:* \vdash \beta:*} \BinaryInfC{\vdash (\lambda \beta.\beta)\ \texttt{int} \equiv\texttt{int}:*} \UnaryInfC{\vdash (\lambda \beta.\beta)\ \texttt{int} \rightarrow \texttt{unit} \equiv \texttt{int} \rightarrow \texttt{unit}:*} \end{prooftree}$

Finally, the extensionality rules allow us to evaluate "underneath" tuples and lambda abstractions. You might think of these as conducting an "experiment" to see whether the relevant constructors behave equivalently.

## Remarks

• As it turns out, in this system, the $$:k$$ annotation on equivalence is unnecessary, as they are uniquely determined by the kinding rules.

Theorem (Regularity).

1. If $$\vdash \Gamma\ ok$$ and $$\Gamma \vdash e:\tau$$, then $$\Gamma \vdash \tau:*$$.

2. If $$\vdash \Gamma\ ok$$ and $$\Gamma \vdash c \equiv c':k$$, then $$\Gamma \vdash c:k$$ and $$\Gamma \vdash c':k$$ Proof.

3. By induction over the judgment $$\Gamma \vdash e:\tau$$.

4. By induction over the judgment $$\Gamma \vdash c \equiv c':k$$. $$\square$$

where $$\vdash \Gamma\ ok$$ is a judgment ensuring that all types in $$\Gamma$$ are well-formed.

Rules 1.4 (Well-formed contexts): $$\vdash \Gamma\ ok$$ $\begin{prooftree} \AxiomC{} \UnaryInfC{\vdash \cdot\ ok} \end{prooftree}\qquad \begin{prooftree} \AxiomC{\Gamma\ ok} \AxiomC{\Gamma \vdash \tau:*} \BinaryInfC{\vdash \Gamma, x:\tau\ ok} \end{prooftree}\qquad \begin{prooftree} \AxiomC{\vdash \Gamma\ ok} \UnaryInfC{\vdash \Gamma, \alpha:k\ ok} \end{prooftree}$