15-417 HOT Compilation, Spring 2020

• Professor: Karl Crary
• Scribe: Cameron Wong
• Carnegie Mellon University

Joining a grand tradition, I'm going to attempt and inevitably give up at typesetting the notes for this class.

Material is grouped by subject and is roughly ordered by when we covered them in class. There is no separation by individual lectures. The order of material in a given subsection is, roughly following class presentation order, but may be reordered according to what I personally find to be clearer.

These are somewhat inspired by Nick Roberts' attempt, and a lot of the early material is... well, not lifted, but definitely influenced by his explanations.

I will do my best to keep my personal comments restricted to the remarks. Any mistakes are mine. These notes will include no more SML code than was presented in lecture.

This document is intended to be read as an mdbook, which, at the time of this writing, can be viewed here.

source

Structure of the Compiler

The compiler developed by this class will follow the following progression:

where each IL- language is some intermediate form. Until IL-Alloc, each intermediary language is also typed, which will aid in ensuring that the passes are well-formed.

It is possible to preserve types all the way down, foregoing the type erasure leading into IL-Alloc. Such compilers often have an "hourglass effect", in which the intermediary typesystems get increasingly simple down to a point, at which they become more complex again. Consider a typed memory representation of the sum type \(A+B\), for example. We have to store a tag (for which variant) along with the object itself, giving us a layout of

Our typesystem must be powerful enough to express these layouts accurately, hence the extra complexity. This may continue all the way down to, say, a typed assembly language. In this class, however, we only have enough time to cover up to IL-Alloc, and will thus generate C from there.

System Fw

System \(F_\omega\) is a system of higher-kinded types and type-constructors. It is relevant to compiling SML in the way that it relates to the module system. If we extend the kind system of "true" \(F_\omega\) with product kinds, we might represent the module signature

sig
  type t
  type 'a u
end

as the kind \(* \times (* \rightarrow *)\), and so on. This even extends to functors that act on modules via type-level lambdas.

System F

As a warmup to \(F_\omega\), a brief review of the rules for System F.

\[\require{bussproofs} \begin{aligned} \tau &:= \alpha \mid \tau \rightarrow \tau \mid \forall \alpha . \tau \\ e &:= x \mid \lambda (x:\tau).e \mid e\ e \mid \Lambda \alpha.e \mid e[\tau] \end{aligned} \]

When typechecking System F, we use two judgments, \(\Gamma \vdash x: \tau\) and \(\Gamma \vdash \tau:*\)¹. The latter is often written \(\Gamma \vdash \tau\ type\), but we will use this notation so it becomes familiar for the future.

\[ \begin{prooftree} \AxiomC{$\Gamma(\alpha)= * $} \UnaryInfC{$\Gamma \vdash \alpha: * $} \end{prooftree}\qquad \begin{prooftree} \AxiomC{$\Gamma \vdash \tau_1: * $} \AxiomC{$\Gamma \vdash \tau_2: * $} \BinaryInfC{$\Gamma \vdash \tau_1 \rightarrow \tau_2: * $} \end{prooftree}\qquad \begin{prooftree} \AxiomC{$\Gamma, \alpha:* \vdash \tau : *$} \UnaryInfC{$\Gamma \vdash \forall \alpha.\tau : *$} \end{prooftree} \]

\[ \begin{prooftree} \AxiomC{$\Gamma(x) = \tau$} \UnaryInfC{$\Gamma \vdash x : \tau$} \end{prooftree}\qquad \begin{prooftree} \AxiomC{$\Gamma, x:\tau_1 \vdash e:\tau_2$} \UnaryInfC{$\Gamma \vdash \lambda (x:\tau_1) . e : \tau_1 \rightarrow \tau_2$} \end{prooftree}\qquad \begin{prooftree} \AxiomC{$\Gamma, \alpha:* \vdash e:\tau$} \UnaryInfC{$\Gamma \vdash \Lambda \alpha. e : \forall \alpha . \tau$} \end{prooftree} \]

The defining feature of System F is the \(\Lambda \alpha.e\) syntax form, with its corresponding \(\forall \alpha.e\) type, the so-called "type-lambdas" or "polymorphic values". Just as value lambdas annotate their argument, we may also choose to do so with type lambdas, as \(\Lambda (\alpha : *).e\). Then the rule for typing big lambda expressions becomes

\[ \begin{prooftree} \AxiomC{$\Gamma, \alpha:* \vdash e:\tau$} \UnaryInfC{$\Gamma \vdash \Lambda (\alpha:*). e : \forall \alpha . \tau$} \end{prooftree} \]

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} \]

Typechecking \(F_\omega^{++}\)

Algorithmically typechecking \(F_\omega\) is more complex. The existence of the reflexive, symmetric and transitive equivalence rules may make proof search more difficult. For example, if the current proof obligations are to show that \(c_1 \equiv c_3 : k\), to use the transitivity rule we would need to guess a \(c_2\) to pass through.

The type system of \(F_\omega\) is equivalent to the simply-typed lambda calculus, so one approach for checking whether two constructors are equivalent is to beta-normalize them, then compare them structurally. This would work, but does not generalize well to later systems.

The immediately relevant judgments are:

The \(+\) and \(-\) symbols denote modality (\(+\) is input and \(-\) is output), but are not otherwise necessary. These judgments form a standard bidirectional typechecking (and kind-checking) algorithm.

In the process, we will also need four more judgments:

Inference Rules

Rules 1.5 (Type synthesis): \(\Gamma \vdash e \Rightarrow \tau\)

\[\require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma(x) = \tau$} \UnaryInfC{$\Gamma \vdash x \Rightarrow \tau$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash \tau \Leftarrow *$} \AxiomC{$\Gamma, x:\tau \vdash e \Rightarrow \tau'$} \BinaryInfC{$\Gamma \vdash \lambda(x:\tau).e \Rightarrow \tau \rightarrow \tau'$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash e_1 \Rightarrow \tau$} \AxiomC{$\Gamma \vdash \tau \Downarrow \tau_1 \rightarrow \tau_2$} \AxiomC{$\Gamma \vdash e_1 \Leftarrow \tau_1$} \TrinaryInfC{$\Gamma \vdash e_1\ e_2 \Rightarrow \tau_2$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma, \alpha:k \vdash e \Rightarrow \tau$} \UnaryInfC{$\Gamma \vdash \Lambda(\alpha:k).e \Rightarrow \forall(\alpha:k).\tau$} \end{prooftree}\qquad \begin{prooftree} \AxiomC{$\Gamma \vdash e \Rightarrow \tau$} \AxiomC{$\Gamma \vdash \tau \Downarrow \forall(\alpha:k).\tau'$} \AxiomC{$\Gamma \vdash c \Leftarrow k$} \TrinaryInfC{$\Gamma \vdash e[c] \Rightarrow [c/\alpha]\tau'$} \end{prooftree} \]

Unlike in 15-317, we mandate the type annotation on the parameter of a lambda, so we can synthesize its type. In the last two rules, we cannot "pattern match" on the synthesized type of the candidate function, because it could have beta redexes. Instead, we normalize it.

Rules 1.6 (Type checking): \(\Gamma \vdash e \Leftarrow \tau\)

\[ \begin{prooftree} \AxiomC{$\Gamma \vdash e \Rightarrow \tau'$} \AxiomC{$\Gamma \vdash \tau \Leftrightarrow \tau' : *$} \BinaryInfC{$\Gamma \vdash e \Leftarrow \tau$} \end{prooftree} \]

We don't yet have a way to construct an invalid kind, so we don't need to ensure that kinds are well-formed (yet).

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

\[ \begin{prooftree} \AxiomC{$\Gamma(\alpha) = k$} \UnaryInfC{$\Gamma \vdash \alpha \Rightarrow k$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash \tau_1 \Leftarrow *$} \AxiomC{$\Gamma \vdash \tau_2 \Leftarrow *$} \BinaryInfC{$\Gamma \vdash \tau_1 \rightarrow \tau_2 \Rightarrow *$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma, \alpha:k \vdash \tau \Leftarrow *$} \UnaryInfC{$\Gamma \vdash \forall(\alpha:k).\tau \Rightarrow *$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma, \alpha:k \vdash c \Rightarrow k'$} \UnaryInfC{$\Gamma \vdash \lambda(\alpha:k).c \Rightarrow k \rightarrow k'$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c_1 \Rightarrow k_1 \rightarrow k_2$} \AxiomC{$\Gamma \vdash c_2 \Rightarrow k_1$} \BinaryInfC{$\Gamma \vdash c_1\ c_2 \Rightarrow k_2$} \end{prooftree} \] \[ \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} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c \Rightarrow k_1 \times k_2$} \UnaryInfC{$\Gamma \vdash \pi_1c \Rightarrow k_1$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c \Rightarrow k_1 \times k_2$} \UnaryInfC{$\Gamma \vdash \pi_2c \Rightarrow k_2$} \end{prooftree} \]

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

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

The rule for kind checking could be written more compactly to use the same variable \(k\) in both premise and conclusion (thus dropping the \(k = k'\) premise), but we write it this way so it can generalize to later calculi (particularly the notion of equality).

When writing the equivalence rules, we will use extensionality to recurse on the kind via the appropriate projections or function application. What we don't do is normalize both types and check equivalence, because this doesn't generalize to the calculus of singleton kinds.

Rules 1.9 (Algorithmic Equivalence): \(\Gamma \vdash c \Leftrightarrow c' : k\)

\[ \begin{prooftree} \AxiomC{$\Gamma, \alpha:k \vdash c\ \alpha \Leftrightarrow c'\ \alpha:k_2$} \UnaryInfC{$\Gamma \vdash c \Leftrightarrow c' : k_1 \rightarrow 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' : k_2$} \BinaryInfC{$\Gamma \vdash c \Leftrightarrow c':k_1 \times k_2$} \end{prooftree} \] \[ \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':*$} \TrinaryInfC{$\Gamma \vdash c_1 \Leftrightarrow c_2:*$} \end{prooftree} \]

Normalization only happens once we reach the kind \(*\).

A normal form is one that has contracted all \(\beta\)-redices. We will instead use weak-head normal form, in which an arrow constructor or a universal constructor is at the outermost level (we don't recursively normalize).

Rules 1.10 (Weak-head normalization): \(\Gamma \vdash c \Downarrow c'\)

\[ \begin{prooftree} \AxiomC{$\Gamma \vdash c \rightsquigarrow c'$} \AxiomC{$\Gamma \vdash c' \Downarrow c''$} \BinaryInfC{$\Gamma \vdash c \Downarrow c''$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c \not\rightsquigarrow$} \UnaryInfC{$\Gamma \vdash c \Downarrow c$} \end{prooftree} \]

Although we could formally defined the judgment \(\Gamma \vdash c \not\rightsquigarrow\), we will choose not to for brevity. This could be implemented in ML by raising an exception or returning a NONE option if none of the stepping rules apply.

Rules 1.11 (Weak-head reduction): \(\Gamma \vdash c \rightsquigarrow c'\)

\[ \begin{prooftree} \AxiomC{} \UnaryInfC{$\Gamma \vdash (\lambda (\alpha:k).c)\ c' \rightsquigarrow [c'/\alpha]c$} \end{prooftree}\qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c_1 \rightsquigarrow c_1'$} \UnaryInfC{$\Gamma \vdash c_1\ c_2 \rightsquigarrow c_1'\ c_2$} \end{prooftree} \] \[ \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} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash c_1 \rightsquigarrow c_1'$} \UnaryInfC{$\Gamma \vdash \langle c_1, c_2 \rangle \rightsquigarrow \langle c_1', c_2 \rangle$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c_2 \rightsquigarrow c_2'$} \UnaryInfC{$\Gamma \vdash \langle c_1, c_2 \rangle \rightsquigarrow \langle c_1, c_2' \rangle$} \end{prooftree} \]

When weak-head normalizing, we only reduce under application and projection. This way, when we encounter types such as \(((\lambda \alpha.\alpha) \ (\lambda \alpha.\alpha)) c\), we can reduce them.

A weak-head normalized constructor can only take certain forms. Those which could be normalized further but are not we'll call "paths".

\[ \begin{aligned} \text{whnf}\ \hat{c} &:= c \rightarrow c \mid \forall(\alpha:k).c \mid p \\ \text{path}\ p &:= \alpha \mid p\ c \mid \pi_1p \mid \pi_2p \end{aligned} \]

By the extensionality rules, we ensure that we reach kind \(*\), so this grammar is exhaustive. Paths are obviously neutral, and whnf terms are almost neutral, except that the subterms (bodies of universal type and arrow) may contain redices.

Rules 1.12 (Structural Equivalence): \(\Gamma \vdash \hat{c_1} \rightarrow \hat{c_2}: k\)

\[ \begin{prooftree} \AxiomC{$\Gamma \vdash c_1 \Leftrightarrow c_1': *$} \AxiomC{$\Gamma \vdash c_2 \Leftrightarrow c_2': *$} \BinaryInfC{$\Gamma \vdash c_1 \rightarrow c_2 \leftrightarrow c_1' \rightarrow c_2'$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma, \alpha:k \vdash \tau \Leftrightarrow \tau': *$} \UnaryInfC{$\Gamma \vdash \forall(\alpha:k).\tau \leftrightarrow \forall(\alpha:k).\tau':*$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma(\alpha) = k$} \UnaryInfC{$\Gamma \vdash \alpha \leftrightarrow \alpha : k$} \end{prooftree}\qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c_1 \leftrightarrow c_1' : k_1 \rightarrow k_2$} \AxiomC{$\Gamma \vdash c_2 \Leftrightarrow c_2' : k_1$} \BinaryInfC{$\Gamma \vdash c_1\ c_2 \leftrightarrow c_1'\ c_2' : k_2$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash c \leftrightarrow c' : k_1 \times k_2$} \UnaryInfC{$\Gamma \vdash \pi_1c \leftrightarrow \pi_1c':k_1$} \end{prooftree}\qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c \leftrightarrow c' : k_1 \times k_2$} \UnaryInfC{$\Gamma \vdash \pi_2c \leftrightarrow \pi_2c':k_2$} \end{prooftree} \]

Algorithmic structural equivalence is not too surprising. The kind is synthesized as an output, which allows it to be put back in as an input to the algorithmic equivalence judgment.

The Singleton Kind Calculus

The next type theory we'll be exploring is the calculus of singleton kinds. This is necessary to represent type-fixed signatures, like

sig
  type t = int
  type u
  val a : t
end

How do we kind this? We can't kind the t tycon at \(*\), because that would allow nonconformant structures (say, those assigning t to string) to ascribe.

The answer is to add a new kind constructor S(c) of singleton kinds, kinds with only one inhabitant. Set-theoretically, S(c) represents the singleton set \({c}\), but that's about where the similarities end.

It turns out that this simple construct (and its intuitive properties) require a lot more power in its machinery.

Singleton kinds, declaratively

The singleton kind calculus relevant to us is syntactically an extension of \(F_\omega\) (plus products), with identical constructors and terms. The kinds, of course, are extended with the \(S(c)\) singleton kind. But to fully represent modules, we need more power.

Consider the signature

sig
  type t
  type u = t * int
end

Intuitively, we might write this kind as \(* \times S(t \times \texttt{int})\), but this isn't well-formed (the type variable \(t\) is not in scope). This necessitates the use of dependent kinds, \(\Sigma\)- and \(\Pi\)-kinds. These subsume normal arrow and (non-dependent) product kinds, giving us

\[\require{bussproofs}k := * \mid S(c) \mid \Sigma(\alpha:k).k \mid \Pi(\alpha:k).k\]

Of course, we will still use \(k \rightarrow k'\) and \(k \times k'\) as shorthand for \(\Pi(\alpha:k).k'\) and \(\Sigma(\alpha:k).k'\) respectively if \(k\) is not free in \(k'\).

The judgments we will use are

The addition of singleton kinds necessitates subkinding to handle cases like int, which has kind \(*\) but also kind \(S(\texttt{int})\).

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

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

Rules 2.2 (Kind equivalence): \(\Gamma \vdash k \equiv k' : \text{kind}\)

\[ \begin{prooftree} \AxiomC{} \UnaryInfC{$\Gamma \vdash * \equiv * : \text{kind}$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c \equiv c' : *$} \UnaryInfC{$\Gamma \vdash S(c) \equiv S(c') :\text{kind}$} \end{prooftree} \]

\[ \begin{prooftree} \AxiomC{$\Gamma \vdash k_1 \equiv k_1' : \text{kind}$} \AxiomC{$\Gamma, \alpha:k_1 \vdash k_2 \equiv k_2' : \text{kind}$} \BinaryInfC{$\Gamma \vdash \Pi(\alpha:k_1).k_2 \equiv \Pi(\alpha:k_1').k_2'$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash k_1 \equiv k_1' : \text{kind}$} \AxiomC{$\Gamma, \alpha:k_1 \vdash k_2 \equiv k_2' : \text{kind}$} \BinaryInfC{$\Gamma \vdash \Sigma(\alpha:k_1).k_2 \equiv \Sigma(\alpha:k_1').k_2'$} \end{prooftree} \]

Before moving onward, we'll need some more machinery. By the above rules, we can only define singleton kinds for types (constructors kinded at \(*\)). As a typechecking mechanism, this is important, lest someone write type t = list. When declaring our whole system, however, this can be inconvenient. Let us define the generalized singleton \(S(c:k)\) be defined as follows:

\[ \begin{aligned} S(c:*) &\triangleq S(c) \\ S(c:\Pi(\alpha:k_1).k_2) &\triangleq \Pi(\alpha:k_1).S(c\ \alpha : k_2) \\ S(c:\Sigma(\alpha:k_1).k_2) &\triangleq S(\pi_1c : k_1) \times S(\pi_2c:[\pi_1c/\alpha]k_2) \\ S(c:S(c')) &\triangleq S(c) \end{aligned} \]

Note that the \(\Sigma\) clause could be more concisely written as \(\Sigma(\alpha:S(\pi_1c:k_1)).S(\pi_2c:k_2)\), but we choose to expand it out for clarity. Ideally, this definition should fit to the following condition (written as a derived rule):

\[ \begin{prooftree} \alwaysDashedLine \AxiomC{$\Gamma \vdash c:k$} \AxiomC{$\vdash \Gamma\ ok$} \BinaryInfC{$\Gamma \vdash S(c:k)\ ok$} \end{prooftree} \]

which it does.

Why is all this necessary? Previously, when checking constructor equivalence, neither \(\Gamma\) nor \(k\) were used. But what about in this system?

\[ \lambda (\alpha:*) . \alpha \overset{?}{=} \lambda (\alpha:*) . \texttt{int} \]

Before, we would say that this is "obviously false". Calling one on a type that is not int demonstrates this. But now, with subkinding, we might say that

\[\cdot \vdash \lambda (\alpha:*) . \alpha : S(\texttt{int}) \rightarrow *\]

because \(S(\texttt{int}) \le *\). But then, these two lambdas should be equivalent, because if \(\alpha : S(\texttt{int})\), then \(\alpha\) must be (equivalent to) \(\texttt{int}\) itself! So clearly the kind we are checking at matters.

Similarly, we need the context as well. Consider

\[ \beta (\lambda(\alpha:*).\alpha) \overset{?}{=} \beta(\lambda(\alpha:*).\texttt{int}) \]

Now, the kind of \(\beta\) fixes the kinds of the lambdas (which, as we saw above, matters).

Rules 2.3 (Subkinding): \(\Gamma \vdash k \le k'\)

Preorder: \[ \begin{prooftree} \AxiomC{$\Gamma \vdash k \equiv k':\text{kind}$} \UnaryInfC{$\Gamma \vdash k \le k'$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash k_1 \le k_2$} \AxiomC{$\Gamma \vdash k_2 \le k_3$} \BinaryInfC{$\Gamma \vdash k_1 \le k_3$} \end{prooftree} \]

Other: \[ \begin{prooftree} \AxiomC{$\Gamma \vdash c:*$} \UnaryInfC{$\Gamma \vdash S(c) \le *$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c \equiv c' : *$} \RightLabel{$*$} \UnaryInfC{$\Gamma \vdash S(c) \le S(c')$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash k_1' \le k_1$} \AxiomC{$\Gamma, \alpha:k_1' \vdash k_2 \le k_2'$} \AxiomC{$\Gamma, \alpha:k_1 \vdash k_2 : \text{kind}$} \TrinaryInfC{$\Gamma \vdash \Pi(\alpha:k_1).k_2 \le \Pi(\alpha:k_1').k_2'$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash k_1 \le k_1'$} \AxiomC{$\Gamma, \alpha:k_1 \vdash k_2 \le k_2'$} \AxiomC{$\Gamma, \alpha:k_1' \vdash k_2' : \text{kind}$} \TrinaryInfC{$\Gamma\vdash\Sigma(\alpha:k_1).k_2\le\Sigma(\alpha:k_1').k_2'$} \end{prooftree} \]

The starred rule is actually unnecessary, as it falls out from the symmetry rule.

The rule for \(\Pi\) types flips the direction of the input kind, as functions are known to be contravariant. When checking the dependent parts of \(\Pi\) and \(\Sigma\), it is important that our context holds that \(\alpha\) is the larger kind, as it will work for both comparands. Finally, we must check that certain subkinds are well-formed, as this won't necessarily fall out from proving other premises.

Rules 2.4.1 (Kinding, incomplete): \(\Gamma \vdash c:k\)

\[ \begin{prooftree} \AxiomC{$\Gamma(\alpha) = k$} \UnaryInfC{$\Gamma \vdash \alpha : k$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma, \alpha:k \vdash c:k'$} \AxiomC{$\Gamma \vdash k:\text{kind}$} \BinaryInfC{$\Gamma \vdash \lambda(\alpha:k).c : \Pi(\alpha:k).k'$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c_1:\Pi(\alpha:k).k'$} \AxiomC{$\Gamma \vdash c_2:k$} \BinaryInfC{$\Gamma \vdash c_1\ c_2:[c_2/\alpha]k'$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash c:\Sigma(\alpha:k_1).k_2$} \UnaryInfC{$\Gamma \vdash \pi_1c : k_1$} \end{prooftree}\qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c:\Sigma(\alpha:k_1).k_2$} \UnaryInfC{$\Gamma \vdash \pi_2c : [\pi_1c/\alpha]k_2$} \end{prooftree} \]

The major missing rule is the one kinding type-level tuples. There is one obvious candidate:

\[ \begin{prooftree} \AxiomC{$\Gamma \vdash c_1:k_1$} \AxiomC{$\Gamma \vdash c_2:[c_1/\alpha]k_2$} \AxiomC{$\Gamma, \alpha:k_1 \vdash k_2:\text{kind}$} \TrinaryInfC{$\Gamma \vdash \langle c_1,c_2 \rangle:\Sigma(\alpha:k_1).k_2$} \end{prooftree} \]

There is also the rule for non-dependent tuples:

\[ \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} \]

which clearly falls out from the first rule. It turns out, however, that these two formulations are actually equivalent (under subsumption). Suppose we are given \(\Gamma \vdash c_1:k_1\), \(\Gamma \vdash c_2:[c_1/alpha]k_2\) and that the kinds are well-formed. Then

• We have \(\Gamma \vdash c_1:S(c_1:k_1)\) by how we defined generalized singletons
• \(\Gamma \vdash \langle c_1, c_2 \rangle : S(c_1:k_1) \times [c_1/\alpha]k_2\) by the non-dependent product rule.
• \(\alpha\) is not free in \([c_1/\alpha]k_2\), so \(\Gamma, \alpha:S(c_1:k_1) \vdash [c_1/\alpha]k_2 \le k_2\).
• So \(\Gamma \vdash S(c_1:k_1) \times [c_1/\alpha]k_2 \le \Sigma(\alpha:k_1).k_2\).
• Then by subsumption, \(\Gamma \vdash \langle c_1, c_2 \rangle : \Sigma(\alpha:k_1). k_2\). It turns out that using the non-dependent product rule is ultimately much simpler, so we will use it over the dependent version.

We complete rules 2.4 (for now) with singletons, arrows and \(\forall\):

Rules 2.4.2 (Kinding continued, still incomplete):

\[ \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} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash c \equiv c': *$} \UnaryInfC{$\Gamma \vdash c : S(c')$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash \tau_1:*$} \AxiomC{$\Gamma \vdash \tau_2:*$} \BinaryInfC{$\Gamma \vdash \tau_1 \rightarrow \tau_2:*$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash k:\text{kind}$} \AxiomC{$\Gamma, \alpha:k \vdash \tau:*$} \BinaryInfC{$\Gamma \vdash \forall(\alpha:k).\tau : *$} \end{prooftree} \]

The rule for singletons should be unsurprising, and the rules for arrow and \(\forall\) types are unchanged from system \(F_\omega\).

At last, then, we come to constructor equivalence. The general theme will be to use dependent versions of the rules we had before.

Rules 2.5 (Constructor equivalence): \(\Gamma \vdash c \equiv c'\)

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$} \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 k_1 \equiv k_1' : \text{kind}$} \AxiomC{$\Gamma, \alpha:k_1 \vdash c \equiv c':k_2$} \BinaryInfC{$\Gamma \vdash \lambda(\alpha:k_1).c \equiv \lambda(\alpha:k_1').c': \Pi(\alpha:k_1).k_2$} \end{prooftree} \quad \begin{prooftree} \AxiomC{$\Gamma \vdash c_1 \equiv c_1' : \Pi(\alpha:k_1).k_2$} \AxiomC{$\Gamma \vdash c_2 \equiv c_2' : k_2$} \BinaryInfC{$\Gamma \vdash c_1\ c_2 \equiv c_1'\ c_2' : [c_2/\alpha]k_2$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash c_1 \equiv c_1' : k_1$} \AxiomC{$\Gamma \vdash c_2 \equiv c_2' : [c/\alpha]k_2$} \BinaryInfC{$\Gamma \vdash \langle c_1, c_2 \rangle \equiv \langle c_1', c_2' \rangle : \Sigma(\alpha:k_1).k_2$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash c \equiv c' : \Sigma(\alpha:k_1).k_2$} \UnaryInfC{$\Gamma \vdash \pi_1c \equiv \pi_1c':k_1$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c \equiv c' : \Sigma(\alpha:k_1).k_2$} \UnaryInfC{$\Gamma \vdash \pi_2c \equiv \pi_2c':[\pi_1c/\alpha]k_2$} \end{prooftree} \]

Types constructors: \[ \begin{prooftree} \AxiomC{$\Gamma \vdash c_1 \equiv c_1' : *$} \AxiomC{$\Gamma \vdash c_2 \equiv c_2' : *$} \BinaryInfC{$\Gamma \vdash c_1\rightarrow c_2 \equiv c_1' \rightarrow c_2':*$} \end{prooftree}\qquad \begin{prooftree} \AxiomC{$\Gamma \vdash k \equiv k' : \text{kind}$} \AxiomC{$\Gamma, \alpha:k \vdash c \equiv c' : *$} \BinaryInfC{$\Gamma \vdash \forall(\alpha:k).c\equiv\forall(\alpha:k').c':*$} \end{prooftree} \]

Beta-reduction: \[ \begin{prooftree} \AxiomC{$\Gamma \vdash c_1:k_1$} \AxiomC{$\Gamma, \alpha:k_1 \vdash c_2:k_2$} \BinaryInfC{$\Gamma \vdash (\lambda(\alpha:k_1).c_2)\ c_1 \equiv [c_1/\alpha]c_2 : [c_1/\alpha]k_2$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash c_1 : k_1$} \AxiomC{$\Gamma \vdash c_2 : k_2$} \BinaryInfC{$\Gamma \vdash \pi_1 \langle c_1, c_2 \rangle \equiv c_1$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash c_1 : k_1$} \AxiomC{$\Gamma \vdash c_2 : k_2$} \BinaryInfC{$\Gamma \vdash \pi_2 \langle c_1, c_2 \rangle \equiv c_2$} \end{prooftree} \]

Extensionality: \[ \begin{prooftree} \AxiomC{$\Gamma \vdash c:\Pi(\alpha:k_1).k_2'$} \AxiomC{$\Gamma \vdash c':\Pi(\alpha:k_1).k_2''$} \AxiomC{$\Gamma, \alpha:k_1 \vdash c\ \alpha \equiv c'\ \alpha : k_2$} \TrinaryInfC{$\Gamma \vdash c \equiv c' : \Pi(\alpha:k_1).k_2$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash \pi_1c \equiv \pi_1c' : k_1$} \AxiomC{$\Gamma \vdash \pi_2c \equiv \pi_2c' : [\pi_1c/\alpha]k_2$} \AxiomC{$\Gamma, \alpha:k_1 \vdash k_2:\text{kind}$} \TrinaryInfC{$\Gamma \vdash c \equiv c' : \Sigma(\alpha:k_2)$} \end{prooftree} \]

Finally, we may choose to include a singleton rule:

\[ \begin{prooftree} \alwaysDashedLine \AxiomC{$\Gamma \vdash c:S(c')$} \UnaryInfC{$\Gamma \vdash c \equiv c':S(c')$} \end{prooftree} \]

but it's unnecessary, as it arises inversion of the singleton rule from 2.4.2.

It turns out, however, that our formulation of constructor kinding isn't quite complete. Consider the following situation.

Recall that \(S(c:\Pi(\alpha:k_1).k_2 = \Pi(\alpha:k_1).S(c\ \alpha : k_2)\). Then consider the type constructor \(\lambda(\alpha:*).\texttt{int}\):

\[ \begin{aligned} \lambda(\alpha:*).\texttt{int} &: S(\lambda(\alpha:*).\texttt{int}:* \rightarrow *) \\ &= \Pi(\alpha:*).S((\lambda(\alpha:*).\texttt{int})\ \alpha : *) \\ &= \Pi(\alpha:*).S((\lambda(\alpha:*).\texttt{int})\ \alpha) \\ &= \Pi(\alpha:*).S(\texttt{int}) \end{aligned} \]

(where the \(=\) above are kind equality)

By this, we should be able to derive \(\lambda(\alpha:*).\texttt{int}: \Pi(\alpha:*).S(\texttt{int})\). This can be done easily:

\[ \begin{prooftree} \AxiomC{} \UnaryInfC{$\alpha:* \vdash \texttt{int} : S(\texttt{int})$} \UnaryInfC{$\cdot \vdash \lambda(\alpha:\texttt{int}).\texttt{int} : \Pi(\alpha:*).S(\texttt{int})$} \end{prooftree} \]

which should follow from our existing rules.

However, this doesn't generalize. Namely, we should be able to show that, if \(\beta:S(* \rightarrow *)\), then \(\beta:\Pi(\alpha:*).S(\beta\ \alpha)\). As our rules currently are, however, we can't do this -- our rules currently only allow type lambdas and beta- or pi-redexes to have \(\Pi\)-types, and the singular variable \(\beta\) is neither. A similar issue arises with product kinds. We can resolves this by giving up the structural-only property of the constructor kinding rules and adding extensionality there as well:

Rules 2.4.3 (Kinding finalized)

\[ \begin{prooftree} \AxiomC{$\Gamma \vdash c:\Pi(\alpha:k_1).k_2'$} \AxiomC{$\Gamma, \alpha:k_1 \vdash c\ \alpha:k_2$} \BinaryInfC{$\Gamma \vdash c:\Pi(\alpha:k_1).k_2$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash \pi_1c:k_1$} \AxiomC{$\Gamma \vdash \pi_2c:[\pi_1c/\alpha]k_2$} \AxiomC{$\Gamma, \alpha:k_1 \vdash k_2:\text{kind}$} \TrinaryInfC{$\Gamma \vdash c:\Sigma(\alpha:k_1).k_2$} \end{prooftree} \]

Remarks

• I'm a bit sketched on how the proof of non-dependent products implying dependent products works. The moral reason is that the dependent argument must have a fully instantiated kind, so it doesn't matter whether the actual sum kind is dependent, but the subtyping via the generalized singleton doesn't quite make sense to me. Maybe I'll do the full proof out later.

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).

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.

Binding

Up to now, when writing rules "on the whiteboard", we have been blase about our syntactic representation of variables and binding. In particular, all the rules given only make sense if we implicitly assume that all rules apply up to alpha equivalence, and that all substitutions are capture-avoiding. In doing so, however, we necessarily gloss over any details of what an actual program implementing these algorithms may need to ensure these invariants are upheld.

We now give some discussion on how these may be implemented in an actual compiler. In the structural code for this class, we will use a hybrid of the techniques discussed here -- terms will use explicit variables and constructors will use De Bruijin indices. Past this explanation, we will continue to use the notation for explicit variables everywhere, which should be implicitly converted to De Bruijin where appropriate.

Explicit Variables

Consider (syntactically) the lambda calculus whose terms consist of variables, lambda abstractions, and applications. Variables and bindings are "explicit", represented and differentiated with a literal string of characters (say \(x\)). This has the example of being extremely simple to read, and has comparatively few pitfalls to other approaches.

What would a substitution function on these terms look like? Certainly, substituting into a variable or an application is easy. What about the lambda case?

\[\require{bussproofs} \begin{aligned}[] [M/x]\lambda x.N &= \lambda x.N \hfill& \\ [M/x]\lambda y.N &= \lambda y.[M/x]N \hfill& (y \not\in FV(M)) \\ [M/x]\lambda y.N &= \lambda y'.[M/x][y/y']N \hfill& (y' \ne x, y \in FV(M), y' \not\in FV(M)) \end{aligned} \]

In the first case, we ignore the substitution -- the variable \(x\) is bound in the lambda, so any suboccurrences of \(x\) aren't free (and thus shouldn't be subbed). In the other two cases, we are forced to check whether \(y\) is free in the substitutee \(M\), traversing the entire term each time. Then, if it is free in \(M\), we also need to traverse the subterm \(N\) to alpha-vary it properly.

This is, as you may have surmised, not an ideal state of affairs. One alternative is to just always alpha-vary the bound term, giving us the clause

\[ \begin{aligned}[] [M/x]\lambda y.N &= \lambda y'.[M/x][y/y']N \hfill& (x \ne y, y' \ne x, y' \ne FV(M)) \end{aligned} \]

where we generate a fresh variable each time. This is marginally better for simplicity, but now requires us to traverse the subterm \(N\) every time.

De Bruijin Indices

Clearly, we need a better way. Another alternative we can use is De Bruijin indices, in which a variable is represented by the number of binders between the variable itself and its introduction. So the term \(\lambda x.x\ (\lambda y. x\ y)\) would be written as \(\lambda . 0\ (\lambda. 1\ 0)\).

Related is the idea of De Bruijin levels, which count the indices backwards, from the outermost binder. However, these are unwieldy and nobody uses them, so we won't either.

Our substitution function, then, will look like this (remember that \(i\) and \(j\) are natural numbers here):

\[ \begin{aligned}[] [M/i]i &= M \\ [M/i]j &= j-1 \hfill& (j > i) \\ [M/i]j &= j \hfill& (j \lt i) \\ [M/i](N_1\ N_2) &= [M/i]N_1\ ([M/i]N_2) \\ [M/i]\lambda.N &= \lambda.[M\uparrow^1_0/i+1]N \end{aligned} \]

where \(\uparrow\) is an operation that shifts the variables in a subterm (to be defined). If \(j \lt i\), on the other hand, we can leave it be, as there isn't an intermediate binding that has been removed.

In the \(j > i\) case, we need to lower the variable by 1, because if we're substituting for it, it means we've removed a binding site (namely, the binding \(i\)).

When going underneath a binder (in the \(\lambda\)-abstraction case), we need to adjust any variables in the substitutee \(M\) to account for the extra binder -- if \(M\) refers to some free variable at index \(0\), then that needs to become index \(1\) once we go underneath the lambda binder. This is where the \(\uparrow\) operation comes in:

\[ \begin{aligned}[] i \uparrow^j_k &= i + j \hfill& (i \ge k) \\ i \uparrow^j_k &= i \hfill& (\text{otherwise}) \\ (M\ N) \uparrow^j_k &= (M \uparrow^j_k)\ (N \uparrow^j_k) \\ (\lambda.M) \uparrow^j_k &= \lambda.(M \uparrow^j_{k+1}) \end{aligned} \]

Let's try this on some concrete examples. Consider the eta rule for \(\Pi\)-kinds:

\[ \begin{prooftree} \AxiomC{$\Gamma, \alpha:k_1 \vdash c\ \alpha:k_2$} \UnaryInfC{$\Gamma \vdash c : \Pi(\alpha:k_1).k_2$} \end{prooftree} \]

Under De Bruijin, this becomes

\[ \begin{prooftree} \AxiomC{$\Gamma, k_1 \vdash c\uparrow^1_0\ 0 : k_2$} \UnaryInfC{$\Gamma \vdash c : \Pi(k_1).k_2$} \end{prooftree} \]

In the premise, we need to upshift any variables in the constructor \(c\), because we're adding a new variable (namely, \(\alpha\)) without going underneath an explicit binding site.

What about application?

\[ \begin{prooftree} \AxiomC{$\Gamma \vdash c:\Pi(\alpha:k_1).k_2$} \AxiomC{$\Gamma \vdash c':k_1$} \BinaryInfC{$\Gamma \vdash c\ c' : [c'/\alpha]k_2$} \end{prooftree} \]

This becomes

\[ \begin{prooftree} \AxiomC{$\Gamma \vdash c:\Pi(k_1).k_2$} \AxiomC{$\Gamma \vdash c':k_1$} \BinaryInfC{$\Gamma \vdash c\ c' : [c'/0]k_2$} \end{prooftree} \]

Here, because of how we defined substitution, we can avoid needing to do the explicit downshift that comes from instantiating the \(\alpha\) binding.

Explicit substitutions

When working with such a representation, it can often be extremely unwieldy to need to use the above definition for every substitution. Instead, we can use a compositional representation acting on terms. Let \(\sigma\) be the syntactic class of substitutions, which are, spiritually, functions from term to term, applied as \(M[\sigma]\) (the reverse of the usual notation). Some presentations of this system may even add \(M[\sigma]\) to the grammar as a term itself (called a "closure", confusingly), but we will not, for simplicit. We have

\[ \begin{aligned} \sigma &:= \uparrow^i \mid M.\sigma \\ \end{aligned} \]

where \(M.\sigma\) is the substitution replacing variable \(0\) with \(M\) and performing \(\sigma\) to \(i-1\) for each other variable \(i\). We will also define the substitution \(id\) to be \(\uparrow^0\).

The substitution \([M_0/0, M_1/1, M_2/2]\), then, will be represented by the operation \(M_0.M_1.M_2.id\).

With substitutions now represented as first-class, it makes sense to define the composition of substitutions. Namely, we want \(\sigma \circ \sigma'\) to be the transformation such that \(M[\sigma \circ \sigma'] = (M[\sigma])[\sigma']\).

Our application rules become:

\[\begin{aligned} 0[M.\sigma] &= M \\ i+1[M.\sigma] &= i[\sigma] \\ i [\uparrow^j] &= i+j \\ (N\ P)[\sigma] &= (N[\sigma]\ P[\sigma]) \\ (\lambda.M)[\sigma] &= \lambda.(M[0.(\sigma \circ \uparrow^1)]) \end{aligned} \]

with composition defined as

\[\begin{aligned} (M.\sigma) \circ \sigma' &= (M[\sigma']) . (\sigma \circ \sigma') \\ \uparrow^i \circ \uparrow^j &= \uparrow^{i+j} \\ id \circ M.\sigma &= M.\sigma \\ \uparrow^{i+1} \circ M.\sigma &= \uparrow^i \circ \sigma \end{aligned} \]

Suppose, then, that we wanted to apply an operation \(\sigma\) to the second variable in our binding list. To do that with what we have, we'd need to leave all \(0\)s and \(1\)s untouched. We can do that with

\[ \sigma \rightsquigarrow 0.(\sigma \circ \uparrow) \rightsquigarrow 0.((0.(\sigma \circ \uparrow)) \circ \uparrow) \]

where \(\rightsquigarrow\) is a transformation shifting a substitution to act under one binding, and the last term is equal to

\[ 0.(0[\uparrow].(\sigma \circ \uparrow) \circ \uparrow) = 0.1.(\sigma \circ \uparrow^2) \]

This suggests a pattern:

\[ under_i(\sigma) = 0.1.\dots.i-1.\sigma \circ \uparrow^i \]

which is to apply the operation \(\sigma\) under \(i\) bindings.

A typical use case may look like

\[ 0.1.\dots.i-1.M_1[\uparrow^i].\dots.M_j[\uparrow^i].\uparrow^{i+k} \]

In the starter code, this pattern is implemented for us as the function

subst_term : nat -> term list -> nat -> subst

Remarks

• I always find it simplest to think of the variable \(0\) as being an index into the ordered context list. In this way, any time something is added to the context without an explicit binder, it makes sense to increment the internal vars.

Continuation Passing Style

The next language we'll be covering is IL-CPS, whose purpose is to make control flow explicit in the syntax of the language.

In particular, this language will have the following three properties:

1. No implicit control flow -- procedure calls, returns, exceptions, etc. are all represented as jumps.
2. All intermediate values are named.
3. Continuations are reified as 1st class values.

To explain the second condition, instead of compound expressions like x+y+z, in CPS form we would use something akin to let x' = x+y in x'+z.

There are some compilers whose CPS transformation pass only conforms to the first two conditions. This is known as "A-normal form", or "monadic form". Or, very creatively, "2/3rds CPS".

Type-directed Translation

As usual, before we get into a full discussion of CPS, we'll need to develop some more machinery.

Usually, language translations are "syntax-directed", a translation judgment defined inductively over the syntax tree. Between two types of lambda calculi, for example, we might define our translation like this:

\[\require{bussproofs} \begin{aligned} \overline{x} &= x \\ \overline{\lambda (x:\tau).e} &= \lambda(x:\overline{\tau}).\overline{e} \\ \overline{e_1\ e_2} &= \overline{e_1}\ \overline{e_2} \end{aligned} \]

where the the translation can be determined solely by looking at the particular syntactic form.

One problem: This doesn't always work.

For example, consider translating a language with booleans into System \(F_\omega\). Under a standard Church encoding, we'd translate the type bool as

\[ \overline{bool} = \forall(\alpha:*).(\alpha \rightarrow \alpha \rightarrow \alpha) \]

with the corresponding introduction forms

\[ \begin{aligned} \overline{true} &= \Lambda \alpha.\lambda(x:\alpha).\lambda(y:\alpha).x \\ \overline{false} &= \Lambda \alpha.\lambda(x:\alpha).\lambda(y:\alpha).y \\ \end{aligned} \]

A problem, however, comes when trying to translate the elimination form:

\[ \overline{if\ e_1\ then\ e_2\ else\ e_3} = \overline{e_1}[\tau]\ \overline{e_2} \ \overline{e_3} \]

What type should we use for \(\tau\)? It should be the type of \(e_1\) and \(e_2\), but without actually running a typechecker, we won't know what type that is! To deal with this, we can use a type-directed translation, which couples the translation step with the typechecking/type synthesis process.

Of course, there are really two typing judgments here, one for the source and one for the target language. These are usually notated

\[ \begin{aligned} \Gamma \vdash_S e:\tau \\ \Gamma \vdash_T e:\tau \end{aligned} \]

for source and target, respectively. However, we will elide the subscripts in cases where the context makes it clear, typically when we know what language the given term is in.

Our translation judgment, then, becomes

\[\Gamma \vdash_S e:\tau \rightsquigarrow e'\]

where \(e\) is in the source and \(e'\) is in the target language.

Note that we can actually use a syntax-directed translation of constructors, kinds and contexts. For a more complex constructor language, we may need to perform a kind-directed translation, but we will avoid that for reasons to be discussed.

A translation, then, should have the following regularity conditions:

1. \(\Gamma \vdash_S \tau: *\) if and only if \(\overline{\Gamma} \vdash_T \overline{\tau}: *\).
2. \(\Gamma \vdash_S e:\tau\) if and only if there exists some \(e'\) such that \(\Gamma \vdash_S e:\tau \rightsquigarrow e'\).
3. If \(\Gamma \vdash_S e:\tau \rightsquigarrow e'\), then \(\overline{\Gamma} \vdash_T e':\overline{\tau}\) (static correctness).

You might think that, since we have a notion of static correctness, we may also have some form of dynamic correctness to preserve. Loosely, this might be phrased as "If \(\Gamma \vdash e:\tau \rightsquigarrow e'\), then \(e\) and \(e'\) 'do the same thing'". However, it is actually quite difficult to even state this formally! Certainly, we can't state this without having some formal notion of dynamic behavior, which we won't be dealing with in this class. It turns out that these proofs are also quite involved, which is another reason we don't bother.

A type-directed translation rule will always follow the same form of the associated regular typing rule, where the premises are also a translation. The variable translation rule, for example might look like this:

\[ \begin{prooftree} \AxiomC{$\Gamma(x) = \tau$} \UnaryInfC{$\Gamma \vdash x:\tau \rightsquigarrow x$} \end{prooftree} \]

In general, it is best not to touch variable names. If we do start messing with variable names, we'll need to ensure freshness, perform substitutions on subterms, and so on -- not worth it at all.

Returning to the if-then-else example, we can now express the correct translation (assuming the usual rule for typing if-then-else):

\[ \begin{prooftree} \AxiomC{$\Gamma \vdash e_1:bool \rightsquigarrow e_1'$} \AxiomC{$\Gamma \vdash e_2:\tau \rightsquigarrow e_2'$} \AxiomC{$\Gamma \vdash e_3:\tau \rightsquigarrow e_3'$} \TrinaryInfC{$\Gamma \vdash if\ e_1\ then\ e_2\ else\ e_3:\tau \rightsquigarrow e_1'[\overline{\tau}]\ e_2'\ e_3'$} \end{prooftree} \]

Finally, note that these rules will need to be adjusted somewhat to work with the algorithmic type synthesis and type checking rules.

Although we have not given a full formal system, we can sketch out what a proof of the regularity conditions may look like:

1. Depends on the specifics of the kind system, but often follows via induction on the kinding judgment (in both directions).
2. The forward direction is fairly clear, as we design our rules to follow from the source typing judgment. The backwards direction is even easier, as we can simply delete the translations from every premise and conclusion to show what we need.
3. Was not given in lecture; can be proven relatively easily for yourself.

Coherence

An important property of translations in general is coherence, namely that translations are unique.

Suppose that \(\Gamma \vdash_S e:\tau\), and so \(\Gamma \vdash e:\tau \rightsquigarrow e'\). What if we also have \(\Gamma \vdash e:\tau \rightsquigarrow e''\)? In our cases, this will generally be impossible, as our translations are based on typing judgments and typing judgments are unique. In real languages, on the other hand, this is not necessarily the case. The statement of coherence, then, in this case, is that \(e' = e''\). It is very difficult to prove this, so we won't.

For example, what if we're in a language with subtyping? The typical subsumption rule,

\[ \begin{prooftree} \AxiomC{$\Gamma \vdash e:\tau$} \AxiomC{$\Gamma \vdash \tau' \le \tau$} \BinaryInfC{$\Gamma \vdash e:\tau'$} \end{prooftree} \]

actually translates to coercion code in a type-directed setting:

\[ \begin{prooftree} \AxiomC{$\Gamma \vdash e:\tau \rightsquigarrow e'$} \AxiomC{$\Gamma \vdash \tau' \le \tau \rightsquigarrow f$} \BinaryInfC{$\Gamma \vdash e:\tau' \rightsquigarrow f\ e'$} \end{prooftree} \]

where \(f\) is the function witnessing that \(\tau'\) subsumes \(\tau\). Of course, as SML lacks subtyping, we aren't going to bother.

This does, however, bring us back to why we don't perform a kind-directed translation for type constructors -- we do have subkinding! So designing a coherent system for that becomes much more difficult.

Remarks

• In lecture, Prof. Crary chose to use \(\overline{e}\) as the "output" of the translation judgment, where \(\overline{\cdot}\) here is not acting as an operator, just taking the symbol \(\overline{e}\) as a suggestive variable name. I have taken the liberty of rephrasing the rules to use something else for the sake of my own confusion.
• I did a few cases of the proof of the translation from IL-Direct to IL-CPS and it seems to be fairly straightforward. The third condition can be shown by induction over the translation rules, but is muddied by the presence of different syntactic classes.
• Later, there was some discussion about Kleene equivalence, but I zoned out and didn't catch a lot of it (it wasn't particularly relevant to this material). It is a weaker property than full dynamic equivalence; it holds when \(e_1\) halts iff \(e_2\) halts.

Introduction to Continuation Passing Style

Before we can discuss the translation, we must specify our source and target languages.

Source: IL-Direct

For the most part, the kinds and the non-\(\tau\) type constructors will be the same for the rest of the class. The types, on the other hand, will be changing quite frequently, as will the terms (obviously). In a real implementation, we'll also be adding some actual base types, like int, bool, exn, ref, etc.

Target: IL-CPS

Properly, we might notate \(\neg\tau\) as \(\tau \rightarrow answer\) or \(\tau \rightarrow 0\), to notate that lambdas (really, continuations) don't return. However, by marking it as \(\neg\tau\), some of the type relationships become more obvious. Similarly, the \(v\ v\) syntactic form is more of a jump than a function call.

If we had booleans (particularly if-then-else), we might add \(if\ v\ then\ e\ else\ e\) for this. Instead of nesting expressions, we need to bind them into values before they can be used. For this reason, this is a "monadic form".

Basic Principles

When translating kinds and contexts, we can largely do the obvious thing. With types, on the other hand, we have some work to do. We have

\[\require{bussproofs}\overline{\tau_1 \rightarrow \tau_2} = \neg(\overline{\tau_1} \times \neg \overline{\tau_2})\]

Intuitively, we can think of a function, in CPS, as a jump taking the standard parameter (\(\overline{\tau_1}\)) and also a continuation argument telling where to jump with the result (\(\neg\overline{\tau_2}\)). In the theory, the slick way to see it is that \(A \implies B\) is equivalent to \(\neg A \lor B\), which is in turn equivalent to \(\neg (A \land \neg B)\) by De Morgan's law. It turns out that programming in the presence of continuations actually encodes classical logic under Curry-Howard, where the proof of a proposition \(\tau\) can be contradicted with (thrown to) a continuation \(\neg \tau\), which diverges (produces \(\bot\)). Classical and constructive logic coincide on \(\Pi_2\) sentences, which are sentences of the form \(\forall \dots \forall . \exists \dots \exists . p\) (either of the quantifier prefix lists can be empty), where \(p\) is a decidable proposition.

By Curry-Howard, the translation \(M:A \rightsquigarrow \overline{M}: \overline{A}\) transforms the proof \(M\) to remove uses of double negation elimination (known in PL parlance as callcc). If \(A\) is \(\Pi_2\), we can extract a proof of \(A\) from a proof of \(\overline{A}\) in this way.

You may also notice that IL-CPS does not have \(\forall\) types, only \(\exists\). We use the translation

\[\overline{\forall(\alpha:k).\tau} = \neg(\exists(\alpha:\overline{k}).\neg \overline{\tau})\]

again using the classical tautology \(\forall x.p \Leftrightarrow \neg \exists x. (\neg p)\). Computationally, this transforms a function taking the constructor \(\alpha\) and returning a value into a continuation that takes an existential holding \(\alpha\) and an internal continuation taking the resulting \(\tau\) value. We don't actually want to have \(\forall(\alpha:k).\tau\) as a type in our CPS language. It is workable, but very strange -- some function calls become values, and so on. Doing this actually produces better code at the expense of some unfortunate semantics (for example, the value restriction resurfaces).

Some regularity conditions:

1. If \(\Gamma \vdash k:\text{kind}\), then \(\overline{\Gamma} \vdash \overline{k} :\text{kind}\)
2. If \(\Gamma \vdash c:k\), then \(\overline{\Gamma} \vdash \overline{c}:\overline{k}\)

A third property that's nice to have is that the translation commutes with substitution:

\[\overline{[c_1/\alpha]c_2} = [\overline{c_1}/\alpha]\overline{c_2}\]

which holds if we don't mess with the variables.

The translation judgment itself will need to be a little weird to accommodate the CPS property. Instead of using the typical \(\Gamma \vdash e:\tau \rightsquigarrow e'\), we're going to bind an explicit continuation argument \(\Gamma \vdash e:\tau \rightsquigarrow x.e'\), where \(x\) is a bound continuation of type \(\neg \overline\tau\). We can think of this translation as assuming a continuation to pass the "result" of evaluating the expression \(e\) to.

Properly, of course, continuation arguments are named \(k\) by convention. We already use \(k\) for kinds, but the two appear in different contexts, so there's no possibility of confusion.

Statics of IL-CPS

Because of the value-expression modality, we need to adjust our definition of static correctness:

• If \(\Gamma \vdash e:\tau \rightsquigarrow k.e'\) and \(\vdash \Gamma\ ok\), then \(\overline{\Gamma}, k:\neg \overline{\tau} \vdash e':0\)

The \(0\) in this expression typing judgment denotes that, in this language, expressions diverge -- they have type void, effectively. Values, of course, are typed as usual.

IL-CPS, then, is defined statically as follows:

\[ \begin{prooftree} \AxiomC{$\Gamma(x) = \tau$} \UnaryInfC{$\Gamma \vdash x:\tau$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash \tau:*$} \AxiomC{$\Gamma, x:\tau \vdash e:0$} \BinaryInfC{$\Gamma \vdash \lambda(x:\tau).e : \neg \tau$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash v_1:\tau_1$} \AxiomC{$\Gamma \vdash v_2:\tau_2$} \BinaryInfC{$\Gamma \vdash \langle v_1, v_2 \rangle : \tau_1 \times \tau_2$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash c:k$} \AxiomC{$\Gamma \vdash v:[c/\alpha]\tau$} \AxiomC{$\Gamma, \alpha:k \vdash \tau:*$} \TrinaryInfC{$\Gamma \vdash pack\ [c,v]\ in\ \exists(\alpha:k).\tau$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash v_1:\neg \tau$} \AxiomC{$\Gamma \vdash v_2:\tau$} \BinaryInfC{$\Gamma \vdash v_1\ v_2:0$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash v:\tau$} \AxiomC{$\Gamma, x:\tau \vdash e:0$} \BinaryInfC{$\Gamma \vdash let\ x=v\ in\ e:0$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash x:\tau_1 \times \tau_2$} \AxiomC{$\Gamma, x:\tau_1 \vdash e:0$} \BinaryInfC{$\Gamma \vdash let\ x=\pi_1v\ in\ e:0$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash x:\tau_1 \times \tau_2$} \AxiomC{$\Gamma, x:\tau_2 \vdash e:0$} \BinaryInfC{$\Gamma \vdash let\ x=\pi_2v\ in\ e:0$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash v:\exists(\alpha:k).\tau$} \AxiomC{$\Gamma,\alpha:k,x:\tau \vdash e:0$} \BinaryInfC{$\Gamma \vdash unpack\ [\alpha,x]=v\ in\ e:0$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{} \UnaryInfC{$\Gamma \vdash halt:0$} \end{prooftree} \]

Basic Translation

Our initial discussion of CPS transformation centers around "direct-style" code, which features no abnormal control flow operators (exceptions, continuations, etc).

We discussed this a bit briefly in the last section, but here are the collected type translation rules for IL-CPS:

\[\require{bussproofs} \begin{aligned} \overline{\alpha} &= \alpha \\ \overline{\tau_1 \times \tau_2} &= \neg(\overline{\tau_1} \times \overline{\tau_2}) \\ \overline{\tau_1 \rightarrow \tau_2} &= \neg(\overline{\tau_1} \times \neg \overline{\tau_2}) \\ \overline{\forall(\alpha:k).\tau} &= \neg(\exists(\alpha:\overline{k}). \neg\overline{\tau}) \end{aligned} \]

Rules 3.1 (CPS-conversion): \(\Gamma \vdash e:\tau \rightsquigarrow k.e'\)

\[ \begin{prooftree} \AxiomC{$\Gamma(x) = \tau$} \UnaryInfC{$\Gamma \vdash x:\tau \rightsquigarrow k.k\ x$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash e_1:\tau_1 \rightsquigarrow k_1.e_1'$} \AxiomC{$\Gamma \vdash e_2:\tau_2 \rightsquigarrow k_2.e_2'$} \BinaryInfC{$ \begin{aligned} \Gamma \vdash \langle e_1, e_2 \rangle :\tau_1 \times \tau_2 \rightsquigarrow k.& let\ k_1= \lambda(x_1:\overline{\tau_1}).\\ &\quad (let\ k_2=\lambda(x_2:\overline{\tau_2}).k \langle x_1, x_2 \rangle \ in\ e_2') \\ &in\ e_1' \end{aligned} $} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash e : \tau_1 \times \tau_2 \rightsquigarrow k.e'$} \UnaryInfC{$ \begin{aligned} \Gamma \vdash \pi_ie : \tau_i \rightsquigarrow k'.& let\ k=\lambda(x:\overline{\tau_1} \times \overline{\tau_2}). \\ &\quad (let\ y = \pi_ix\ in\ k'\ y) \\ &in\ e' \end{aligned} $} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash \tau:*$} \AxiomC{$\Gamma, x:\tau \vdash e:\tau' \rightsquigarrow k.e'$} \BinaryInfC{$ \begin{aligned} \Gamma \vdash \lambda(x:\tau).e: \tau \rightarrow \tau' \rightsquigarrow k'. &k' (\lambda(y:\overline{\tau} \times \neg\overline{\tau'}). \\ &\qquad let\ x=\pi_1y\ in \\ &\qquad let\ k=\pi_2y\ in\ e') \end{aligned} $} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash e_1:\tau_1 \rightarrow \tau_2 \rightsquigarrow k_1.e_1'$} \AxiomC{$\Gamma \vdash e_2:\tau_1 \rightsquigarrow k_2.e_2'$} \BinaryInfC{$ \begin{aligned} \Gamma \vdash e_1\ e_2:\tau' \rightsquigarrow k.&let\ k_1 = \lambda(x_1:\neg(\overline{\tau_1}\times \neg\overline{\tau_2})). \\ &\quad (let\ k_2 = \lambda(x_2:\tau_1).x_1\langle x_2,k \rangle\ in\ e_2') \\ &in\ e_1' \end{aligned} $} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash k: \text{kind}$} \AxiomC{$\Gamma, \alpha:k \vdash \tau:*$} \AxiomC{$\Gamma, \alpha:k \vdash e:\tau \rightsquigarrow k.e'$} \TrinaryInfC{$ \begin{aligned} \Gamma \vdash \Lambda(\alpha:k).e : \forall(\alpha:k).\tau \rightsquigarrow k'. &k'( \lambda(y:\exists(\alpha:\overline{k}).\neg \overline{\tau}).\\ &\quad unpack [\alpha,k] = y\ in\ e') \end{aligned} $} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash e:\forall(\alpha:k).\tau \rightsquigarrow k.e'$} \AxiomC{$\Gamma \vdash c:k$} \BinaryInfC{$ \begin{aligned} \Gamma \vdash e[c]:[c/\alpha]\tau \rightsquigarrow k'.& let\ k=\lambda(f:\neg(\exists(\alpha:\overline{k}).\neg\overline{\tau})). \\ &\quad f(pack\ [\overline{c},k']\ as\ \exists(\alpha:\overline{k}). \neg \overline{\tau}) \\ &in\ e' \end{aligned} $} \end{prooftree} \]

The important thing to keep in mind while devising these rules is that, when we recursively translate a sub-expression \(e\), we are given some bound term \(k.e'\), in which the bound \(k\) is a continuation taking the "result" of \(e'\) as input. When we use this result, then, \(k\) is free! To complete the translation, then, we have to re-bind \(k\) to be a continuation of the correct type (particularly, \(k\) has type \(\neg \overline\tau\) if \(e\) has type \(\tau\)).

Remarks

• I personally found it easier to chase types rather than try to reason through the control flow. The two main patterns I used for intuition are that \(let\ k=\dots\ in\ e\) is the translation of "evaluate \(e \rightsquigarrow k.e\)" and \(k\ v\) is the translation of "\(v\) is a value".

Other evaluation strategies

In this section, we discuss CPS conversion for a few other evaluation schemes.

Call by Name

The primary counterpart to so-called "strict" evaluation is "lazy" evaluation, otherwise known as "call by name" (as opposed to "call by value") semantics. The key difference, of course, is that sub-expressions aren't evaluated until they are eliminated, leading to things like function arguments being passed as thunks, and so on.

As the key idea behind CPS is to make ccontrol flow very explicit, it stands to reason that it doesn't matter whether IL-CPS is by name or by value, something that the expression-value divide enforces. The difference, then, is expressed in the translation from a call-by-name language to continuation passing style.

Conceptually, this works out with bound variables in contexts having a moral type of \(\neg \neg \tau\) (taking in the "what do I do next" continuation), rather than \(\tau\). The primary place this manifests is in the translation of contexts:

\[\require{bussproofs}\overline{\Gamma, x:\tau} = \overline{\Gamma}, x:\neg\neg\overline\tau\]

We also need to adjust our translation of function types to account for this:

\[\overline{\tau_1 \rightarrow \tau_2} = \neg(\neg \neg \overline{\tau_1} \times \neg \overline{\tau_2}) \]

Now, as it turns out, we can get away with only changing a few rules from their previous definitions:

Rules 3.2 (Call by name translation)

\[ \begin{prooftree} \AxiomC{$\Gamma(x) = \tau$} \UnaryInfC{$\Gamma \vdash x:\tau \rightsquigarrow x\ k$} \end{prooftree} \]

Remember that here, the translated \(x\) has type \(\neg\neg \tau\), so instead of passing the final value \(x\) to \(k\), we pass the continuation \(k\) to \(x\).

Rules 3.2 cont'd

\[ \begin{prooftree} \AxiomC{$\Gamma \vdash \tau_1:*$} \AxiomC{$\Gamma, x:\tau \vdash e:\tau_2 \rightarrow k.e'$} \BinaryInfC{$ \begin{aligned} \Gamma \vdash \lambda(x:\tau).e:\tau_1 \rightarrow \tau_2 \rightsquigarrow k'. k'(&\lambda(y:\neg\neg\overline{\tau_1} \times \neg\overline{\tau_2}).\\ &\quad let\ x=\pi_1y\ in \\ &\quad let\ k=\pi_2y\ in\ e') \end{aligned} $} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash e_1:\tau_1 \rightarrow \tau_2 \rightsquigarrow k_1.e_1'$} \AxiomC{$\Gamma \vdash e_2:\tau_1 \rightsquigarrow k_2.e_2'$} \BinaryInfC{$ \begin{aligned} \Gamma \vdash e_1\ e_2:\tau_2 \rightsquigarrow k.& let\ k_1 = \lambda(f:\neg(\neg \neg \overline{\tau_1}\times \neg\overline{\tau_2})). \\ &\quad f \langle (\lambda(k_2:\neg\overline{\tau_1}).e_2'), k\rangle \\ &in\ e_1' \end{aligned} $} \end{prooftree} \]

The function rule is actually almost completely the same, but is reproduced to demonstrate the type change. In the application rule, instead of evaluating the argument \(e_2'\), we reify it as a thunk to pass as the first argument to the resultant jump.

In fact, these are all the changes we need to change the previous translation into a call by name version! There are often other lazy constructs (such as lazy tuples), but we won't discuss them here.

Aside: Call by "need"

One issue with naive call by name is that, if a given input is used multiple times, it may need to be evaluated multiple times. These can be optimized out in some cases, but in the presence of effects this doesn't help in the general case. Instead, we can use some memoization to cache the results of computations after they've been used once. This is the evaluation strategy used by Haskell, which has the name "call by need".

Under the hood, this is used by storing a datatype UNFORCED of unit -> 'a | FORCED of 'a for the lazy thunks, and then internally using a ref to track them, replacing UNFORCED with FORCED when necessary. This, ironically, leads to Haskell being less naively parallelizable than ML, as there are now mutable data dependencies to worry about (in an ostensibly completely pure language). To get around this, GHC actually does some strictness analysis, compiling what code it can to a call-by-value language, then leaving the rest as call by need.

Call/cc

Scheme popularized the idea of reified first-class continuations with the callcc construct. For use of this concept, SMLNJ exposes two functions:

callcc: ('a cont -> 'a) -> 'a
throw: 'a cont * 'a -> 'b

Instead of using functions, however, we're going to make these primitive constructs in our source language, defined statically as:

\[ \begin{prooftree} \AxiomC{$\Gamma, x:\tau\ cont \vdash e:\tau$} \AxiomC{$\Gamma \vdash \tau:*$} \BinaryInfC{$\Gamma \vdash letcc\ x\ in\ e:\tau$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash e_1:\tau$} \AxiomC{$\Gamma \vdash e_2:\tau\ cont$} \AxiomC{$\Gamma \vdash \tau':*$} \TrinaryInfC{$\Gamma \vdash throw\ e_1\ to\ e_2:\tau'$} \end{prooftree} \]

Suggestively, the target language is continuation passing style for a reason, which suggests the translation of \(\tau\ cont\) to \(\neg \tau\). We can translate these two new constructs as

\[ \begin{prooftree} \AxiomC{$\Gamma, x:\tau\ cont \vdash e:\tau \rightsquigarrow k.e'$} \AxiomC{$\Gamma \vdash \tau:*$} \BinaryInfC{$\Gamma \vdash letcc\ x\ in\ e:\tau \rightsquigarrow k. let\ x=k\ in\ e'$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash e_1:\tau \rightsquigarrow k_1.e_1'$} \AxiomC{$\Gamma \vdash e_2:\tau\ cont \rightsquigarrow k_2.e_2'$} \AxiomC{$\Gamma \vdash \tau':*$} \TrinaryInfC{$ \begin{aligned} \Gamma \vdash throw\ e_1\ to\ e_2:\tau' \rightsquigarrow k.& let\ k_1=\lambda(x:\overline{\tau}).\\ &\quad let\ k_2=\lambda(f:\neg\overline{\tau}).f\ x\ in\ e_2'\\ &in\ e_1' \end{aligned} $} \end{prooftree} \]

Unsurprisingly, \(letcc\) involves capturing the current continuation, which is conveniently passed as the bound \(k\). For \(throw\), we evaluate both \(e_1\) and \(e_2\), and then pass the result of \(e_2\) to the continuation hidden in \(e_2\).

Remarks

• I'm not entirely sure what the issue is with refs in parallel for Haskell. Even if multiple threads try to write to the ref cell at once (assuming atomic reads and writes, of course), there would be no correctness issues, as both threads would be writing the same value anyway (in a pure language). Prof. Crary said that this kind of strategy causes issues with garbage collection but didn't go into detail.

Exception passing

A more involved form of advanced control flow is that of exceptions that automatically propagate up the call stack until being handled.

Aside: Typed exceptions

In ML, the type exn is special in that new variants can be added to it at runtime. This is the so-called extensible type, a dynamically-growing sum type.

This extensibility is actually entirely separate from the concept of exceptions as a control flow tool, despite the two being often conflated. To sidestep dealing with this issue, we will assume the existence of a type \(\tau_{ex}\), the type of exception objects. This type could be int, void, exn, or so on, it doesn't matter.

Syntax of exceptions

Statically, we will define exception handling as follows:

\[\require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma \vdash e_1:\tau$} \AxiomC{$\Gamma, x:\tau_{ex} \vdash e_2:\tau$} \BinaryInfC{$\Gamma \vdash try\ e_1\ with\ x.e_2:\tau$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash e:\tau_{ex}$} \AxiomC{$\Gamma \vdash \tau : *$} \BinaryInfC{$\Gamma \vdash raise\ e:\tau$} \end{prooftree} \]

Because every expression may now have a separate evaluation condition (namely, "raising an exception"), we also need to change some our translation strategy. Previously, we only bound the one continuation k for the singular exit condition. Now, we'll also have a continuation k_ex, which is called with the raised exception of a given expression. For the obvious reason, this style of evaluation is often described as "double-barrelled CPS".

We also need to adjust our type translation:

\[\overline{\tau_1 \rightarrow \tau_2} \rightsquigarrow \neg(\overline{\tau_1} \times \neg \overline{\tau_2} \times \neg \overline{\tau_{ex}})\]

The translation judgment, then, becomes

\[\Gamma \vdash e:\tau \rightsquigarrow k.k_{ex}.e'\]

with coherence condition

• If \(\Gamma \vdash e:\tau \rightsquigarrow k.k_{ex}.e'\), and \(\vdash \Gamma \ ok\), then \(\overline{\Gamma}, k:\neg \overline{\tau}, k_{ex}:\neg \overline{\tau_{ex}} \vdash e':0\)

In most cases, we will simply thread the same \(k_{ex}\) through the same translations developed in the previous section. For example, we might have

\[ \begin{prooftree} \AxiomC{$\Gamma \vdash e_1:\tau_1 \rightsquigarrow k_1.k_{ex}.e_1'$} \AxiomC{$\Gamma \vdash e_2:\tau_2 \rightsquigarrow k_2.k_{ex}.e_2'$} \BinaryInfC{$ \begin{aligned} \Gamma \vdash \langle e_1, e_2 \rangle :\tau_1 \times \tau_2 \rightsquigarrow k.k_{ex}.& let\ k_1= \lambda(x_1:\overline{\tau_1}).\\ &\quad (let\ k_2=\lambda(x_2:\overline{\tau_2}).k \langle x_1, x_2 \rangle \ in\ e_2') \\ &in\ e_1' \end{aligned} $} \end{prooftree} \]

where we use the same exception handler for the premises as the conclusion.

Rules 3.3 (Double-barrelled CPS, selected rules only): \(\Gamma \vdash e:\tau \rightsquigarrow k.k_{ex}.e'\)

\[ \begin{prooftree} \AxiomC{$\Gamma(x) = \tau$} \UnaryInfC{$\Gamma \vdash x:\tau \rightsquigarrow k.k_{ex}.k\ x$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash \tau:*$} \AxiomC{$\Gamma, x:\tau \vdash e:\tau' \rightsquigarrow k'.k_{ex}'.e'$} \BinaryInfC{$ \begin{aligned} \Gamma \vdash \lambda(x:\tau).e: \tau \rightarrow \tau' \rightsquigarrow k.k_{ex}. &k (\lambda (y:\overline{\tau} \times \neg\overline{\tau'} \times \neg\overline{\tau_{ex}}). \\ &\qquad let\ x=\pi_1y\ in \\ &\qquad let\ z=\pi_2y\ in \\ &\qquad let\ k'=\pi_1z\ in \\ &\qquad let\ k_{ex}'=\pi_2z\ in\ e') \end{aligned} $} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash e_1:\tau \rightarrow \tau' \rightsquigarrow k_1.k_{ex}.e_1'$} \AxiomC{$\Gamma \vdash e_2:\tau \rightarrow \tau' \rightsquigarrow k_2.k_{ex}.e_2'$} \BinaryInfC{$ \begin{aligned} \Gamma \vdash e_1\ e_2 : \tau' \rightsquigarrow k.k_{ex}. &let\ k_1' = \lambda(f:\neg(\overline{\tau} \times \neg\overline{\tau'} \times \neg\overline{\tau_{ex}})). \\ &\qquad (let\ k_2 = \lambda(x:\overline{\tau}).f \langle x, \langle k, k_{ex} \rangle \rangle\ in\ e_2') \\ &in\ e_1' \end{aligned} $} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash e:\tau \rightsquigarrow k.k_{ex}.e'$} \AxiomC{$\Gamma, x:\tau_{ex} \vdash e_{ex} : \tau \rightsquigarrow k.k_{ex}'.e_{ex}'$} \BinaryInfC{$ \begin{aligned} \Gamma \vdash try\ e\ with\ x.e_{ex}:\tau \rightsquigarrow k.k_{ex}'. let\ k_{ex}=\lambda(x:\overline{\tau_{ex}}).e_{ex}'\ in\ e' \end{aligned} $} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash \tau:*$} \AxiomC{$\Gamma \vdash e:\tau_{ex} \rightsquigarrow k.k_{ex}.e'$} \BinaryInfC{$\Gamma \vdash raise_\tau\ e:\tau \rightsquigarrow k'.k_{ex}.[k_{ex}/k]e'$} \end{prooftree} \]

Note that we are treating products as right-associative for the purpose of the \(\pi_1\) and \(\pi_2\) expressions. In the raise case, we can simply evaluate the exception expression \(e\), passing \(k_{ex}\) as its regular continuation. For try...catch, we need to replace the exception handler of \(e\) with a function that evaluates \(e_{ex}\), using an outer exception handler on the overall expression.

Remarks

• It's more explicit how the raise rule works if we instead translate to let k = (fn (x:t_ex) => k_ex x) in e'. This is eta-reduced in the rule given.

Miscellaneous Other Notes

Extensible Variants

To complete our discussion of ML-like languages, we need a theory of extensible variants. We will do this by adding a new type constructor \(\tau\ tag\), a reified type tag that will be used to differentiate dynamically-added variants. It, and the exn type, is defined by the rules

\[\require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma \vdash \tau:*$} \UnaryInfC{$\Gamma \vdash \tau\ tag:*$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash \tau:*$} \UnaryInfC{$\Gamma \vdash newtag[\tau]:\tau\ tag$} \end{prooftree} \qquad \begin{prooftree} \AxiomC{$\Gamma \vdash e_1:\tau\ tag$} \AxiomC{$\Gamma \vdash e_2:\tau$} \BinaryInfC{$\Gamma \vdash tag(e_1, e_2):exn$} \end{prooftree} \] \[ \begin{prooftree} \AxiomC{$\Gamma \vdash e_1:\tau\ tag$} \AxiomC{$\Gamma \vdash e_2:exn$} \AxiomC{$\Gamma, x:\tau \vdash e_3:\tau'$} \AxiomC{$\Gamma \vdash e_4:\tau'$} \QuaternaryInfC{$\Gamma \vdash iftag(e_1,e_2,x.e_3,e_4)$} \end{prooftree} \]

Evaluating iftag checks if the expression e_2 is tagged with e_1. If so, bind the captured \(\tau\) value to x in e_3, otherwise, evaluate e_4.

The initial continuation

One issue with our CPS-conversion translation is that we currently produce, as our final program, a strange expression \(k.k_{ex}.e\), with these bound \(k\) and \(k_{ex}\). At the top level, these are effectively free! To resolve this, we will define the judgment

\[\Gamma \vdash_{prod} e:\tau \rightsquigarrow e'\]

for use on the top level program. We can then define

\[ \begin{prooftree} \AxiomC{$\cdot \vdash e:\overline{\tau} \rightsquigarrow k.k_{ex}.e'$} \UnaryInfC{$ \begin{aligned} \cdot \vdash_{prod} e:\tau \rightsquigarrow &let\ k=\lambda(x:\overline{\tau}).halt\ in\\ &let\ k_{ex} = \lambda(x:\overline{\tau_{ex}}). (print\ \unicode{x201C}\text{uncaught exception}\unicode{x201D}; halt)\ in\\ &e' \end{aligned} $} \end{prooftree} \]

(where ; represents obvious sequencing)

Note that we simply throw the result of the entire program on the floor and halt. With this setup, a program's practical usage is in its IO behavior, not in the result of its evaluation. It is possible to set it up otherwise, but that requires more complicated translations at the top level.