<p>A simple fix is to add call-by-value let-expressions<span class="math-container">$$\text{let } x := t\text{ in }u$$</span>that evaluate <span class="math-container">$t$</span> to a value and then substitute it for <span class="math-container">$x$</span>. Having these in the language allows to restrict <span class="math-container">$+$</span> to values (of integer type, so either variables or integer constants) without any loss of expressivity. Indeed, the now-forbidden terms <span class="math-container">$t_1+t_2$</span> can be expressed as <span class="math-container">$$\text{let } x_1 = t_1\text{ in let }x_2 = t_2\text{ in }x_1 + x_2$$</span> or as <span class="math-container">$$\text{let } x_2 = t_2\text{ in let }x_1 = t_1\text{ in }x_1 + x_2$$</span>This forces the programmer to choose between the left-to-right and right-to-left evaluation orders, and hence between the values <span class="math-container">$2$</span> and <span class="math-container">$3$</span> in your example.</p>
<p>This requirement of making evaluation order more explicit happens more generally for many kinds of (side-)effects, e.g. <span class="math-container">$(\text{print}("a");1)+(\text{print}("b");2)$</span> prints either <span class="math-container">$ab$</span> or <span class="math-container">$ba$</span> depending on the chosen expansion of <span class="math-container">$+$</span>. It also happens when one tries to combine call-by-name constructions with call-by-value ones, see Levy's Call-by-Push-Value.</p>
<p>In Curien and Herbelin's <span class="math-container">$\overline{\lambda}\mu\tilde{\mu}$</span> calculus (in the paper &quot;The Duality of Computation&quot;) that exhibits a duality between expressions and continuations, one can extend the let-extension trick above to continuations by using the dual of let, which yields a fairly elegant and well-behaved calculus that can be found in Munch-Maccagnoni's PhD thesis (and subsequent papers).</p>

CC BY-SA 4.0
2023-08-11T16:09:53.063Z
It's a little unclear from the original question if forcing a CBV evaluation order is deemed acceptable.
Martin Berger
CC BY-SA 4.0
2023-08-11T16:31:15.647Z
The original question is indeed unclear from the assumption "Church-Rosser property (evaluation order is irrelevant)". Making the evaluation order relevant is one general method of recovering confluence, see e.g. Danos, Joinet & Schellinx "A new deconstructive logic: Linear logic" https://doi.org/10.2307/2275572.
gadmm
CC BY-SA 4.0
2023-08-11T06:37:38.913Z
2023-08-11T06:37:38.913Z
xavierm02
<p>I'm aware that if you naively add continuations to a language, the Church-Rosser property no longer holds. For example, suppose we have some variant of the STLC with basic arithmetic and integer types. Then, add <span class="math-container">$\text{letcont }u.e$</span> (which binds the current continuation to <span class="math-container">$u$</span> in <span class="math-container">$e$</span>) and <span class="math-container">$\text{throw}_Y(e,e')$</span>, which invokes continuation <span class="math-container">$e$</span> with argument <span class="math-container">$e'$</span>. These would have typing rules:</p>
<p><span class="math-container">$$
\frac{\Gamma,u:\lnot X\vdash e : X}{\Gamma \vdash \text{letcont }(u:\lnot X.e) : X}
$$</span>
and</p>
<p><span class="math-container">$$
\frac{\Gamma \vdash e : \lnot X\qquad\Gamma\vdash e': X}
{\Gamma \vdash \text{throw}_Y (e,e') : Y}
$$</span></p>
<p>Then, you have expression
<span class="math-container">$$
\text{letcont }(u:\lnot Int).(\text{throw}_{Int}(u, 2) + 
\text{throw}_{Int}(u,3))
$$</span>
Of type <span class="math-container">$Int$</span>. If we assume a a left-to-right evaluation order (in the <span class="math-container">$+$</span>), then <span class="math-container">$\text{throw}_{Int}(u,2)$</span> is evaluated first, and so the entire expression evaluates to 2. However, if we evaluate right-to-left, then the opposite occurs, and we get 3.</p>
<p>So, my question is this: is is possible to design a language with both the Curch-Rosser property (evaluation order is irrelevant) and continuations.</p>
<p>Note: I'm not particularly bothered by what the final solution looks like (what type system, what semantics, using delimited continuations etc.). I'm mostly just interested in if it is <em>doable</em> at all. My gut tells me that using types to place constraints on the use of continuations might work (e.g. linear/affine types), but I'm not particularly familiar with those type systems &amp; how they work.</p>
<p>Edit: added more detail to the question.</p>

CC BY-SA 4.0
2023-07-26T15:36:53.727Z
What do you mean by "could evaluate to either 3 or 4"? What are the reduction rules in your language?
Andrej Bauer
<type-theory><pl.programming-languages><continuations>
Can you regain the Church-Rosser property in languages with continuations?
idka
# Can you regain the Church-Rosser property in languages with continuations?

(Asked by: username_0 on 2023-07-26)

I'm aware that if you naively add continuations to a language, the Church-Rosser property no longer holds. For example, suppose we have some variant of the STLC with basic arithmetic and integer types. Then, add $\text{letcont }u.e$ (which binds the current continuation to $u$ in $e$) and $\text{throw}\_Y(e,e')$, which invokes continuation $e$ with argument $e'$. These would have typing rules:

$$
\frac{\Gamma,u:\lnot X\vdash e : X}{\Gamma \vdash \text{letcont }(u:\lnot X.e) : X}
$$
and

$$
\frac{\Gamma \vdash e : \lnot X\qquad\Gamma\vdash e': X}
{\Gamma \vdash \text{throw}\_Y (e,e') : Y}
$$

Then, you have expression
$$
\text{letcont }(u:\lnot Int).(\text{throw}\_{Int}(u, 2) +
\text{throw}\_{Int}(u,3))
$$
Of type $Int$. If we assume a a left-to-right evaluation order (in the $+$), then $\text{throw}\_{Int}(u,2)$ is evaluated first, and so the entire expression evaluates to 2. However, if we evaluate right-to-left, then the opposite occurs, and we get 3.

So, my question is this: is is possible to design a language with both the Curch-Rosser property (evaluation order is irrelevant) and continuations.

Note: I'm not particularly bothered by what the final solution looks like (what type system, what semantics, using delimited continuations etc.). I'm mostly just interested in if it is *doable* at all. My gut tells me that using types to place constraints on the use of continuations might work (e.g. linear/affine types), but I'm not particularly familiar with those type systems & how they work.

Edit: added more detail to the question.

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

> **Comments:**
> **username_1**: What do you mean by "could evaluate to either 3 or 4"? What are the reduction rules in your language?  

---

## 1 answers

### Answer by username_2 on 2023-08-11. Score: 2 | Accepted answer

A simple fix is to add call-by-value let-expressions$$\text{let } x := t\text{ in }u$$that evaluate $t$ to a value and then substitute it for $x$. Having these in the language allows to restrict $+$ to values (of integer type, so either variables or integer constants) without any loss of expressivity. Indeed, the now-forbidden terms $t\_1+t\_2$ can be expressed as $$\text{let } x\_1 = t\_1\text{ in let }x\_2 = t\_2\text{ in }x\_1 + x\_2$$ or as $$\text{let } x\_2 = t\_2\text{ in let }x\_1 = t\_1\text{ in }x\_1 + x\_2$$This forces the programmer to choose between the left-to-right and right-to-left evaluation orders, and hence between the values $2$ and $3$ in your example.

This requirement of making evaluation order more explicit happens more generally for many kinds of (side-)effects, e.g. $(\text{print}("a");1)+(\text{print}("b");2)$ prints either $ab$ or $ba$ depending on the chosen expansion of $+$. It also happens when one tries to combine call-by-name constructions with call-by-value ones, see Levy's Call-by-Push-Value.

In Curien and Herbelin's $\overline{\lambda}\mu\tilde{\mu}$ calculus (in the paper "The Duality of Computation") that exhibits a duality between expressions and continuations, one can extend the let-extension trick above to continuations by using the dual of let, which yields a fairly elegant and well-behaved calculus that can be found in Munch-Maccagnoni's PhD thesis (and subsequent papers).

> **Comments:**
> **username_3**: It's a little unclear from the original question if forcing a CBV evaluation order is deemed acceptable.  
> **username_4**: The original question is indeed unclear from the assumption "Church-Rosser property (evaluation order is irrelevant)". Making the evaluation order relevant is one general method of recovering confluence, see e.g. Danos, Joinet & Schellinx "A new deconstructive logic: Linear logic" https://doi.org/10.2307/2275572.  

---

