7
$\begingroup$

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.

$\endgroup$
1
  • 3
    $\begingroup$ What do you mean by "could evaluate to either 3 or 4"? What are the reduction rules in your language? $\endgroup$ Jul 26, 2023 at 15:36

1 Answer 1

2
$\begingroup$

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

$\endgroup$
2
  • 1
    $\begingroup$ It's a little unclear from the original question if forcing a CBV evaluation order is deemed acceptable. $\endgroup$ Aug 11, 2023 at 16:09
  • 1
    $\begingroup$ 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" doi.org/10.2307/2275572. $\endgroup$
    – gadmm
    Aug 11, 2023 at 16:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.