<p>Is there somewhere a precise but hopefully readable account of how the CPS (=continuation-passing-style) transformation applies to the <em>typed</em> lambda-calculus?  (Say, simply-typed with product and sum types, but let's not get too picky here.)</p>
<p>In other words, this should describe how the transformation applies to types as well as terms.</p>
<p>To describe a little what is causing me some confusion, the CPS transformation I have in mind is as follows for the <em>untyped</em> case (many sources give this, so I suppose it works):</p>
<p><span class="math-container">$$
\begin{aligned}
v^{\mathrm{cps}} &amp;= \lambda k. kv\quad \text{for $v$ variable} \\
(\lambda v.t)^{\mathrm{cps}} &amp;= \lambda k.k(\lambda v.t^{\mathrm{cps}})\\
(fx)^{\mathrm{cps}} &amp;= \lambda k. f^{\mathrm{cps}}(\lambda f_0. (x^{\mathrm{cps}} (\lambda x_0. f_0 x_0 k)))
\end{aligned}
$$</span></p>
<p>But as such this presents a typing problem: the first line implies that <span class="math-container">$v^{\mathrm{cps}}$</span> should have type <span class="math-container">$(A\to R)\to R$</span>, where <span class="math-container">$R$</span> is the return type of continuations, for any variable <span class="math-container">$v$</span> of type <span class="math-container">$A$</span> so also for any <em>term</em> of type <span class="math-container">$A$</span> if the transformation is to depend only on the term, but now in the second line <span class="math-container">$\lambda v.t^{\mathrm{cps}}$</span> has type <span class="math-container">$A \to (B\to R) \to R$</span> if <span class="math-container">$v$</span> has type <span class="math-container">$A$</span> and <span class="math-container">$t$</span> has type <span class="math-container">$B$</span>, and there is simply no way to get a <span class="math-container">$((A\to B)\to R) \to R$</span> from an <span class="math-container">$A \to (B\to R) \to R$</span>.</p>
<p>At the level of types, I would have expected to get something like the Glivenko (“one <span class="math-container">$\neg\neg$</span> in front of the whole formula”), Gödel-Gentzen (“<span class="math-container">$\neg\neg$</span> in front of atoms and disjunctions”) or more likely Kolmogorov translation (“<span class="math-container">$\neg\neg$</span> in front of every connector”) of intuitionistic propositional logic (perhaps with <span class="math-container">$\neg A$</span> replaced with <span class="math-container">$\mathop{\sim}A := A\to R$</span>), but while the first line makes sense for Glivenko the other translations would require the translation of a <em>term</em> to depend on the <em>type</em> of the term, which I couldn't find a way to work out.</p>
<hr />
<p><strong>Edit:</strong> After further thought, I <em>think</em> the following works:</p>
<ul>
<li><p>Fix a type <span class="math-container">$R$</span> (return values of continuations).  For short, let <span class="math-container">$\mathop{\sim}A$</span> denote <span class="math-container">$A\to R$</span>.  Note that there is an obvious function <span class="math-container">$A \to \mathop{\sim}\mathop{\sim}A$</span> (namely <span class="math-container">$\lambda x.\lambda k.kx$</span>).</p>
</li>
<li><p>Define a type <span class="math-container">$T^\diamond$</span> by induction on the type <span class="math-container">$T$</span> as follows <span class="math-container">$A^\diamond := A$</span> for atomic <span class="math-container">$A$</span>, <span class="math-container">$(A\circ B)^\diamond := (A^\diamond) \circ (B^\diamond)$</span> for <span class="math-container">$\circ \in \{\times, +\}$</span> but <span class="math-container">$(A\to B)^\diamond := (A^\diamond) \to \mathop{\sim}\mathop{\sim} (B^\diamond)$</span>.</p>
</li>
<li><p>Define <span class="math-container">$T^{\mathrm{cps}} := \mathop{\sim}\mathop{\sim} (T^\diamond)$</span>.  Then <span class="math-container">$t^{\mathrm{cps}}$</span> has type <span class="math-container">$T^{\mathrm{cps}}$</span> if <span class="math-container">$t$</span> has type <span class="math-container">$T$</span>, and free variables of type <span class="math-container">$V$</span> inside <span class="math-container">$t$</span> now become of type <span class="math-container">$V^\diamond$</span> inside <span class="math-container">$t^{\mathrm{cps}}$</span>.</p>
</li>
</ul>
<p>(So the error above is to assume that <span class="math-container">$v$</span> has the same type in <span class="math-container">$t$</span> and in <span class="math-container">$t^{\mathrm{cps}}$</span> in the second line.)</p>
<p>But I'm not sure I didn't mess this up, and even if I didn't, surely someone must have written in with appropriate details somewhere before: where?</p>

CC BY-SA 4.0
2023-12-13T23:27:16.793Z
Does this help any? https://link.springer.com/article/10.1007/BF01019463
cody
CC BY-SA 4.0
2023-12-13T23:38:47.923Z
@cody Yes, thanks! As well as the (slightly simpler) [paper by Meyer and Wand](https://doi.org/10.1007/3-540-15648-8_17) they cite. Apparently what I had guessed was correct. (But it's nice to have a confirmation, and also nice to know about call-by-name CPS as well.)
Gro-Tsen
<type-theory><pl.programming-languages><curry-howard><continuations>
Description of the CPS transformation for the typed lambda-calculus
Gro-Tsen
# Description of the CPS transformation for the typed lambda-calculus

(Asked by: username_0 on 2023-12-13)

Is there somewhere a precise but hopefully readable account of how the CPS (=continuation-passing-style) transformation applies to the *typed* lambda-calculus? (Say, simply-typed with product and sum types, but let's not get too picky here.)

In other words, this should describe how the transformation applies to types as well as terms.

To describe a little what is causing me some confusion, the CPS transformation I have in mind is as follows for the *untyped* case (many sources give this, so I suppose it works):

$$
\begin{aligned}
v^{\mathrm{cps}} &= \lambda k. kv\quad \text{for $v$ variable} \\
(\lambda v.t)^{\mathrm{cps}} &= \lambda k.k(\lambda v.t^{\mathrm{cps}})\\
(fx)^{\mathrm{cps}} &= \lambda k. f^{\mathrm{cps}}(\lambda f\_0. (x^{\mathrm{cps}} (\lambda x\_0. f\_0 x\_0 k)))
\end{aligned}
$$

But as such this presents a typing problem: the first line implies that $v^{\mathrm{cps}}$ should have type $(A\to R)\to R$, where $R$ is the return type of continuations, for any variable $v$ of type $A$ so also for any *term* of type $A$ if the transformation is to depend only on the term, but now in the second line $\lambda v.t^{\mathrm{cps}}$ has type $A \to (B\to R) \to R$ if $v$ has type $A$ and $t$ has type $B$, and there is simply no way to get a $((A\to B)\to R) \to R$ from an $A \to (B\to R) \to R$.

At the level of types, I would have expected to get something like the Glivenko (“one $\neg\neg$ in front of the whole formula”), Gödel-Gentzen (“$\neg\neg$ in front of atoms and disjunctions”) or more likely Kolmogorov translation (“$\neg\neg$ in front of every connector”) of intuitionistic propositional logic (perhaps with $\neg A$ replaced with $\mathop{\sim}A := A\to R$), but while the first line makes sense for Glivenko the other translations would require the translation of a *term* to depend on the *type* of the term, which I couldn't find a way to work out.

---

**Edit:** After further thought, I *think* the following works:

* Fix a type $R$ (return values of continuations). For short, let $\mathop{\sim}A$ denote $A\to R$. Note that there is an obvious function $A \to \mathop{\sim}\mathop{\sim}A$ (namely $\lambda x.\lambda k.kx$).
* Define a type $T^\diamond$ by induction on the type $T$ as follows $A^\diamond := A$ for atomic $A$, $(A\circ B)^\diamond := (A^\diamond) \circ (B^\diamond)$ for $\circ \in \{\times, +\}$ but $(A\to B)^\diamond := (A^\diamond) \to \mathop{\sim}\mathop{\sim} (B^\diamond)$.
* Define $T^{\mathrm{cps}} := \mathop{\sim}\mathop{\sim} (T^\diamond)$. Then $t^{\mathrm{cps}}$ has type $T^{\mathrm{cps}}$ if $t$ has type $T$, and free variables of type $V$ inside $t$ now become of type $V^\diamond$ inside $t^{\mathrm{cps}}$.

(So the error above is to assume that $v$ has the same type in $t$ and in $t^{\mathrm{cps}}$ in the second line.)

But I'm not sure I didn't mess this up, and even if I didn't, surely someone must have written in with appropriate details somewhere before: where?

**Tags:** type-theory, pl.programming-languages, curry-howard, continuations

> **Comments:**
> **username_1**: Does this help any? https://link.springer.com/article/10.1007/BF01019463  
> **username_0**: @username_1 Yes, thanks! As well as the (slightly simpler) [paper by Meyer and Wand](https://doi.org/10.1007/3-540-15648-8_17) they cite. Apparently what I had guessed was correct. (But it's nice to have a confirmation, and also nice to know about call-by-name CPS as well.)  

---

## 0 answers

