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