Can you regain the Church-Rosser property in languages with continuations?

Question

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.

Answer 1

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