Typechecking the SKC

Typechecking will act similarly to what we've done before; many of these judgements should look familiar (for ease of typesetting I'm choosing to use superscripts for modes instead of writing it on top of the character from here onwards).

JudgmentMeaning
\(\Gamma^+ \vdash k^+ \Leftarrow \text{kind}\)Kind validity
\(\Gamma^+ \vdash k^+ \Leftrightarrow k'^+ : \text{kind}\)Kind equivalence
\(\Gamma^+ \vdash k^+ \unlhd k'^+\)Subkinding
\(\Gamma^+ \vdash c^+ \Rightarrow k^-\)Kind synthesis
\(\Gamma^+ \vdash c^+ \Leftarrow k^+\)Kind checking
\(\Gamma^+ \vdash c^+ \uparrow k^- \)Natural kind
\(\Gamma^+ \vdash c^+ \Leftrightarrow c'^+ : k^+\)Algorithmic equivalence
\(\Gamma^+ \vdash c^+ \leftrightarrow c'^+ : k^-\)Structural path equivalence
\(\Gamma^+ \vdash c^+ \rightsquigarrow c'^-\)Weak-head reduction
\(\Gamma^+ \vdash c^+ \Downarrow c'^-\)Weak-head normalization
\(\Gamma^+ \vdash e^+ \Rightarrow \tau^-\)Type synthesis
\(\Gamma^+ \vdash e^+ \Leftarrow \tau^+\)Type checking

As our term and constructor language is entirely unchanged from \(F_\omega\), we can import the type checking/synthesis rules nearly wholesale. The only change is that we now need to check that the kind introduced by a \(\forall\) introduction is well-formed, via adding a kind validity premise:

\[\require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma \vdash k \Leftarrow \text{kind}$} \AxiomC{$\Gamma, \alpha:k \vdash e \Rightarrow \tau$} \BinaryInfC{$\Gamma \vdash \Lambda(\alpha:k).e \Rightarrow \forall(\alpha:k).\tau$} \end{prooftree} \]

Kinds

Next, we introduce the idea of a principal kind. In the presence of subkinding, it may be possible infer many non-equivalent kinds for a given constructor, so we want to produce the one that is "most specific". A kind \(k\) is principal for a type constructor \(c\) in context \(\Gamma\) if:

  • \(\Gamma \vdash c:k\)
  • For all kinds \(k'\), if \(\Gamma \vdash c:k'\), then \(\Gamma \vdash k \le k'\).

For example, if \(\alpha\) has kind \(*\), then its principal kind is \(S(\alpha)\). This is where higher order singletons become see their main use -- if \(c:k\), then the principal kind of \(c\) is \(S(c:k)\).

Rules 2.6 (Kind validity): \(\Gamma \vdash k \Leftarrow \text{kind}\)

\[ \begin{prooftree} \AxiomC{} \UnaryInfC{$\Gamma \vdash * \Leftarrow \text{kind}$} \end{prooftree}\qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c \Leftarrow *$} \UnaryInfC{$\Gamma \vdash S(c) \Leftarrow \text{kind}$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash k_1 \Leftarrow \text{kind}$} \AxiomC{$\Gamma, \alpha:k_1 \vdash k_2 \Leftarrow \text{kind}$} \BinaryInfC{$\Gamma \vdash \Sigma(\alpha:k_1).k_1 \Leftarrow \text{kind}$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash k_1 \Leftarrow \text{kind}$} \AxiomC{$\Gamma, \alpha:k_1 \vdash k_2 \Leftarrow \text{kind}$} \BinaryInfC{$\Gamma \vdash \Pi(\alpha:k_1).k_1 \Leftarrow \text{kind}$} \end{prooftree} \]

Should be largely unsurprising.

Rules 2.7 (Kind synthesis): \(\Gamma \vdash c \Rightarrow k\)

\[ \begin{prooftree} \AxiomC{$\Gamma(\alpha) = k$} \UnaryInfC{$\Gamma \vdash \alpha \Rightarrow S(\alpha:k)$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash \tau_1 \Leftarrow *$} \AxiomC{$\Gamma \vdash \tau_2 \Leftarrow *$} \BinaryInfC{$\Gamma \vdash \tau_1 \rightarrow \tau_2 \Rightarrow S(\tau_1 \rightarrow \tau_2)$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash k \Leftarrow \text{kind}$} \AxiomC{$\Gamma, \alpha:k \vdash \tau \Leftarrow *$} \BinaryInfC{$\Gamma \vdash \forall(\alpha:k).\tau \Rightarrow S(\forall(\alpha:k).\tau)$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash k \Leftarrow \text{kind}$} \AxiomC{$\Gamma, \alpha:k\vdash c \Rightarrow k'$} \BinaryInfC{$\Gamma \vdash \lambda(\alpha:k).c \Rightarrow \Pi(\alpha:k).k'$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c_1 \Rightarrow k_1$} \AxiomC{$\Gamma \vdash c_2 \Rightarrow k_2$} \BinaryInfC{$\Gamma \vdash \langle c_1,c_2 \rangle \Rightarrow k_1 \times k_2$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash c \Rightarrow \Sigma(\alpha:k_1).k_2$} \UnaryInfC{$\Gamma \vdash \pi_1c \Rightarrow k_1$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c \Rightarrow \Sigma(\alpha:k_1).k_2$} \UnaryInfC{$\Gamma \vdash \pi_2c \Rightarrow [\pi_1c/\alpha]k_1$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c_1 \Rightarrow \Pi(\alpha:k).k'$} \AxiomC{$\Gamma \vdash c_2 \Leftarrow k$} \BinaryInfC{$\Gamma \vdash c_1\ c_2: [c_2/\alpha]k$} \end{prooftree} \]

Recall that the formation rules for dependent and non-dependent tuples are actually equivalent, so we take the simpler one.

Kind checking only has one rule, which details subsumption.

Rules 2.8 (Kind checking): \(\Gamma \vdash c \Leftarrow k\)

\[ \begin{prooftree} \AxiomC{$\Gamma \vdash c \Rightarrow k'$} \AxiomC{$\Gamma \vdash k' \unlhd k$} \BinaryInfC{$\Gamma \vdash c \Leftarrow k$} \end{prooftree} \]

Rules 2.9 (Subkinding): \(\Gamma \vdash k \unlhd k'\)

\[ \begin{prooftree} \AxiomC{} \UnaryInfC{$\Gamma \vdash * \unlhd *$} \end{prooftree}\qquad \begin{prooftree} \AxiomC{} \UnaryInfC{$\Gamma \vdash S(c) \unlhd *$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c \Leftrightarrow c' :*$} \UnaryInfC{$\Gamma \vdash S(c) \unlhd S(c')$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash k_1' \unlhd k_1$} \AxiomC{$\Gamma \alpha:k_1' \vdash k_2' \unlhd k_2$} \BinaryInfC{$\Gamma \vdash \Pi(\alpha:k_1).k_2 \unlhd \Pi(\alpha:k_1').k_2'$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash k_1 \unlhd k_1'$} \AxiomC{$\Gamma, \alpha:k_1 \vdash k_2 \unlhd k_2'$} \BinaryInfC{$\Gamma \vdash \Sigma(\alpha:k_1).k_2 \unlhd \Sigma(\alpha:k_1').k_2'$} \end{prooftree} \]

Once again, in the rules for \(\Pi\)- and \(\Sigma\)-kinds, the kind of the type variable is set to be that of the superkind, as it will be valid in both of the dependent kinds.

Rules 2.10 (Algorithmic equivalence): \(\Gamma \vdash c \Leftrightarrow c':k\)

\[ \begin{prooftree} \AxiomC{} \UnaryInfC{$\Gamma \vdash c \Leftrightarrow c' : S(c'')$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c_1 \Downarrow c_1'$} \AxiomC{$\Gamma \vdash c_2 \Downarrow c_2'$} \AxiomC{$\Gamma \vdash c_1' \leftrightarrow c_2' : k$} \TrinaryInfC{$\Gamma \vdash c_1 \Leftrightarrow c_2 : *$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma, \alpha:k_1 \vdash c\ \alpha \Leftrightarrow c'\ \alpha:k_2$} \UnaryInfC{$\Gamma \vdash c \Leftrightarrow c' : \Pi(\alpha:k_1).k_2$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash \pi_1c \Leftrightarrow \pi_1c' : k_1$} \AxiomC{$\Gamma \vdash \pi_2c \Leftrightarrow \pi_2c' : [\pi_1c/\alpha]k_2$} \BinaryInfC{$\Gamma \vdash c \Leftrightarrow c' : \Sigma(\alpha:k_1).k_2$} \end{prooftree} \]

The singleton rule follows via regularity (soundness). In the rule at kind \(*\), we can ignore the kinds returned from \(\leftrightarrow\) for the same reason -- if, in the resultant code, we ever query \(\Gamma \vdash c_1 \equiv c_2 : k\), we'd better have that \(\Gamma \vdash c_1:k\) and \(\Gamma \vdash c_2:k\).

Natural Kinds

Structural equality is about the same as \(F_\omega\), with one major caveat. Consider the following:

\[\beta:*, \alpha:S(\beta) \vdash \alpha \Leftrightarrow \beta : *\]

This should certainly be derivable by the definition of the singleton kinds. However, we need some extra machinery to be able to express this -- \(\alpha\) is certainly not structurally equal to \(\beta\), as they are different free variables. We will define the "natural kind" of a constructor to be the "obvious" result, without trying to be clever or more specific. But first, weak head reduction:

Rules 2.11 (Weak head reduction and normalization)

\[ \begin{prooftree} \AxiomC{$\Gamma \vdash c_1 \rightsquigarrow c_2$} \AxiomC{$\Gamma \vdash c_2 \Downarrow c_3$} \BinaryInfC{$\Gamma \vdash c_1 \Downarrow c_3$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c \not\rightsquigarrow$} \UnaryInfC{$\Gamma \vdash c \Downarrow c$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash p \uparrow S(c)$} \UnaryInfC{$\Gamma \vdash p \rightsquigarrow c$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash c_1 \rightsquigarrow c_1'$} \UnaryInfC{$\Gamma \vdash c_1\ c_2 \rightsquigarrow c_1'\ c_2$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c \rightsquigarrow c'$} \UnaryInfC{$\Gamma \vdash \pi_1c \rightsquigarrow \pi_1c'$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c \rightsquigarrow c'$} \UnaryInfC{$\Gamma \vdash \pi_2c \rightsquigarrow \pi_2c'$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{} \UnaryInfC{$\Gamma \vdash (\lambda(\alpha:k).c_1)\ c_2 \rightsquigarrow [c_2/\alpha]c_1$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{} \UnaryInfC{$\Gamma \vdash \pi_1 \langle c_1, c_2 \rangle \rightsquigarrow c_1$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{} \UnaryInfC{$\Gamma \vdash \pi_2 \langle c_1, c_2 \rangle \rightsquigarrow c_2$} \end{prooftree} \]

As before, we will restrict structural equality and natural kinding to only apply to those tycons that are weak head normalized. Recall that such constructors are either lambdas, \(\forall\)-types, or paths. We don't want to natural kind lambdas or \(\forall\), since they will give us \(*\), which isn't what we're looking for with these rules. As such, we have used \(p\) to represent path constructors.

Rules 2.12 (Natural Kind): \(\Gamma \vdash p \uparrow k\)

\[ \begin{prooftree} \AxiomC{$\Gamma(\alpha) = k$} \UnaryInfC{$\Gamma \vdash \alpha \uparrow k$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash p \uparrow \Pi(\alpha:k_1).k_2$} \UnaryInfC{$\Gamma \vdash p\ c \uparrow [c/\alpha]k_2$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash p \uparrow \Sigma(\alpha:k_1).k_2$} \UnaryInfC{$\Gamma \vdash \pi_1p \uparrow k_1$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash p \uparrow \Sigma(\alpha:k_1).k_2$} \UnaryInfC{$\Gamma \vdash \pi_2p \uparrow [\pi_1p/\alpha]k_2$} \end{prooftree} \]

Note that we don't bother looking up a natural kind for \(c_1\ c_2\), because it will never be a singleton, so why bother?

Now, we can derive the earlier example. Letting \(\Gamma = \beta:*, \alpha: S(\beta)\), we have

\[ \begin{prooftree} \AxiomC{} \UnaryInfC{$\Gamma(\alpha) = S(\beta)$} \UnaryInfC{$\Gamma \vdash \alpha \uparrow S(\beta)$} \UnaryInfC{$\Gamma \vdash \alpha \rightsquigarrow \beta$} \AxiomC{} \UnaryInfC{$\Gamma \vdash \beta \not\rightsquigarrow$} \BinaryInfC{$\Gamma \vdash \alpha \Downarrow \beta$} \AxiomC{} \UnaryInfC{$\Gamma \vdash \beta \not\rightsquigarrow$} \UnaryInfC{$\Gamma \vdash \beta \Downarrow \beta$} \AxiomC{} \UnaryInfC{$\Gamma(\beta) = *$} \UnaryInfC{$\Gamma \vdash \beta \leftrightarrow \beta:*$} \TrinaryInfC{$\Gamma \vdash \alpha \Leftrightarrow \beta : *$} \end{prooftree} \]

Structural Equivalence, at last

For completeness, the structural equality rules, which are largely unchanged from \(F_\omega\):

Rules 2.13 (Structural equality): \(\Gamma \vdash p \leftrightarrow p'\)

\[ \begin{prooftree} \AxiomC{$\Gamma(\alpha) = k$} \UnaryInfC{$\Gamma \vdash \alpha \leftrightarrow \alpha : k$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash \tau_1 \Leftrightarrow \tau_1':*$} \AxiomC{$\Gamma \vdash \tau_2 \Leftrightarrow \tau_2':*$} \BinaryInfC{$\Gamma \vdash \tau_1 \rightarrow \tau_2 \leftrightarrow \tau_1' \rightarrow \tau_2' : *$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash k \Leftrightarrow k' : \text{kind}$} \AxiomC{$\Gamma, \alpha:k \vdash c \Leftrightarrow c' : *$} \BinaryInfC{$\Gamma \vdash \forall(\alpha:k).c \leftrightarrow \forall(\alpha:k').c'$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash p \leftrightarrow p' : \Sigma(\alpha:k_1).k_2$} \UnaryInfC{$\Gamma \vdash \pi_1p \leftrightarrow \pi_1p'$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash p \leftrightarrow p' : \Sigma(\alpha:k_1).k_2$} \UnaryInfC{$\Gamma \vdash \pi_2p \leftrightarrow \pi_2p'$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash p_1 \leftrightarrow p_2:\Pi(\alpha:k_1).k_2$} \AxiomC{$\Gamma \vdash c_1 \Leftrightarrow c_2:k_1$} \BinaryInfC{$\Gamma \vdash p_1\ c_1 \leftrightarrow p_1\ c_2:[c_1/\alpha]k_2$} \end{prooftree} \]

Remarks

  • Professor Crary glossed over or entirely skipped some of the rules mentioned here, particularly kind equivalence (which made the homework extra fun...). I have included those rules from Nick Roberts' notes for the sake of completeness.