Introduction to Continuation Passing Style
Before we can discuss the translation, we must specify our source and target languages.
Source: IL-Direct
| Sort | ||
|---|---|---|
| Kinds | \(k:=\) | \(* \mid S(c) \mid \Pi(\alpha:k).k \mid \Sigma(\alpha:k).k\) |
| Tycons | \(c:=\) | \(\alpha \mid \lambda(\alpha:k).c \mid c\ c \mid \langle c, c\rangle \mid \pi_1c \mid \pi_2c\) |
| (Types) | \((\tau)\) | \(\phantom{\alpha} \mid \forall(\alpha:k).\tau \mid \tau \rightarrow \tau \mid \tau \times \tau\) |
| Terms | \(e:=\) | \(x \mid \Lambda(\alpha:k).e \mid e[c] \mid \lambda(x:\tau).e \mid e\ e\) |
| \(\phantom{x} \mid \langle e, e \rangle \mid \pi_1e \mid \pi_2e\) |
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
| Sort | ||
|---|---|---|
| Kinds | \(k:=\) | same |
| Tycons | \(c:=\) | same |
| (Types) | \((\tau)\) | \(\dots \mid \exists(\alpha:k).\tau \mid \neg\tau \mid \tau \times \tau\) |
| Values | \(v:=\) | \(x \mid \lambda(x:\tau).e \mid \langle v, v \rangle \mid pack\ [c,v]\ as\ \exists(\alpha:k).\tau\) |
| Expressions | \(e:=\) | \(let\ x=v\ in\ e \mid v\ v \mid let\ x = \pi_1v\ in\ e \mid let\ x = \pi_2v\ in\ e\) |
| \(\phantom{x} \mid unpack\ [\alpha,x] = v\ in\ e \mid halt\) |
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:
- If \(\Gamma \vdash k:\text{kind}\), then \(\overline{\Gamma} \vdash \overline{k} :\text{kind}\)
- 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} \]