PaperlayerView exact revision on arXiv

Source-linked AI summary

Expressive power of one-shot control operators and coroutines

Kentaro Kobayashi, Yukiyoshi Kameyama

arXiv:2609.06443v1cs.PLcs.LO

TL;DR

The paper addresses the limited theoretical understanding of one-shot control operators and the difficulty of establishing correct expressiveness results. It rigorously compares one-shot effect handlers, one-shot delimited-control operators, and asymmetric coroutines using macro-expressibility, proving translations toward coroutines but not the converse. The results also identify why an earlier translation fails and how reference cells repair it, while showing that macro-expressibility may be too strict for some comparisons.

  • Problem

    The theoretical foundation and expressiveness relationships of one-shot control operators remain insufficiently studied, with prior results sometimes lacking correctness proofs or being incorrect.

  • Method

    The paper systematically compares one-shot effect handlers, one-shot delimited-control operators, and coroutines using macro-expressibility, with refined translations and correctness proofs.

  • Results

    One-shot delimited-control operators and one-shot effect handlers can be macro-expressed by asymmetric coroutines, but asymmetric coroutines cannot be macro-expressed by either.

  • Takeaways & Limitations

    Correctly relating one-shot control operators requires tracking continuation validity with reference cells and stores, while macro-expressibility's locality can block translations of global effects.

  • Takeaways & Limitations

    The authors suggest macro-expressibility is too strict as a comparison measure and leave relaxed locality conditions for future work.

Abstract

from arXiv · show

Control operators, such as exceptions and effect handlers, provide a means of representing computational effects in programs abstractly and modularly. While most theoretical studies have focused on multi-shot control operators, one-shot control operators---which restrict the use of captured continuations to at most once---are gaining attention for their balance between expressiveness and efficiency. This study aims to fill the gap. We present a mathematically rigorous comparison of the expressive power among one-shot control operators, including effect handlers, delimited continuations, and even asymmetric coroutines. Following previous studies on multi-shot control operators, we adopt Felleisen's macro-expressiveness as our measure of expressiveness. We verify the folklore that one-shot effect handlers and one-shot delimited-control operators can be macro-expressed by asymmetric coroutines, but not vice versa. We explain why a previous informal argument fails, and how to revise it to make a valid macro-translation. This is the extended version of a paper presented at APLAS 2025.

1 Introduction

Control operators represent computational effects, with growing interest in effect handlers alongside established exceptions, coroutines, and delimited control. One-shot variants restrict captured continuations to at most one use and are motivated by efficiency, verification, and connections to dynamic-language control operators.

  • Control operators represent computational effects abstractly and modularly, including exceptions, coroutines, delimited control, and effect handlers.
  • One-shot control operators restrict each captured continuation to at most one use.
  • One-shot variants can avoid stack copying, potentially reduce verification complexity, and connect continuation-based operators with intrinsically one-shot operators in dynamic languages.

DRAFT PAPER UNDER REVIEW

This paper provides a systematic, rigorous comparison of three one-shot control facilities using macro-expressibility. It proves that asymmetric coroutines express one-shot delimited control and effect handlers, while the converse translations do not hold, and repairs a failed translation argument.

  • Motivation: One-shot control operators require separate theoretical treatment because one-shotness is dynamic, complicating semantics and precise reasoning.Prior expressiveness results were sometimes unproved or incorrect.
  • Proof strategy and revision: A naïve translation from one-shot delimited continuations to coroutines fails to preserve semantics, so the paper analyzes its failure and proves a refined translation correct.The paper also adds key definitions, proof cases, and a new inexpressibility result completing the comparison.
  • Scope and framework: The paper systematically compares one-shot effect handlers, one-shot delimited-control operators, and asymmetric coroutines using macro-expressibility.It presents this as the first systematic rigorous study of one-shot control-operator expressiveness.
  • Expressiveness results: One-shot delimited-control operators can be macro-expressed by asymmetric coroutines.The extended version introduces a simpler translation that permits a more concise correctness proof.
  • Expressiveness results: One-shot effect handlers can also be macro-expressed by asymmetric coroutines.This result is part of the paper’s three stated contributions.
  • Expressiveness results: Asymmetric coroutines cannot be macro-expressed by either one-shot delimited-control operators or one-shot effect handlers.This establishes the non-converse directions in the comparison.

2 Core calculus and macro-expressibility

The paper establishes MAM as a common call-by-push-value core and uses macro-expressibility to compare language extensions while preserving core syntax and termination.

  • Core calculus MAM: MAM separates values from computations and serves as the common core calculus for extensions.It subsumes call-by-value and call-by-name evaluation strategies.
  • Core calculus MAM: MAM programs are computations, whose deterministic evaluation returns a value when evaluation terminates successfully.The semantics use evaluation contexts to locate redexes and beta-reduction rules to reduce them.
  • Macro-expressibility: Macro-expressibility compares extensions through compositional translations that preserve MAM constructors and encode added constructors using fixed target abstractions.A strong translation also preserves program termination in both directions.
  • Macro-expressibility: A macro-translation maps each source extension construct to a target syntactic abstraction while preserving the behavior of translated programs.For every source program, evaluation is defined exactly when evaluation of its translation is defined.
  • Macro-expressibility: Weak macro-translation relaxes the termination condition from an if-and-only-if requirement to only the forward implication.Sequencing illustrates macro-expressibility by translating M; N into let _ = φ(M) in φ(N).

3 One-shot delimited continuations as asymmetric coroutines

This section formalizes one-shot delimited continuations and asymmetric coroutines, then develops and proves a refined macro-translation between them. The refinement uses reference cells to preserve one-shot validity and establishes semantic preservation and strong macro-expressibility.

  • 3.1 The calculus for one-shot delimited continuations: DELone restricts each captured continuation to one invocation and dynamically records continuation validity in a store.A nil store entry denotes an already-invoked continuation rather than an undefined label.
  • 3.2 The calculus for asymmetric coroutines: AC models coroutines with labeled computations, creation, resumption, and yielding, using coroutines that can suspend and later resume.Its syntax and operational semantics are defined as an extension of the core calculus.
  • 3.3 Naïve translation: The intuitive translation maps dollar, shift0, and throw to create, yield, and resume, but it fails to preserve semantics because coroutine validity alternates.A second continuation label mapped to the same coroutine can suspend it and illegitimately reactivate an earlier continuation.
  • 3.4 Refined translation: The refined translation maps each continuation label to a distinct reference cell containing either a valid coroutine label or an invalid marker.Distinct cells separate continuations backed by one coroutine, while invalid cells never regain validity.
  • 3.4 Refined translation: The correctness proof relates stores as well as computations because continuation validity resides in reference cells rather than in the realizing coroutine.The simulation theorem supports preservation of defined evaluation and strong macro-expressibility from DELone to AC.

4 One-shot effect handlers as asymmetric coroutines

The paper proves that one-shot effect handlers are macro-expressible in asymmetric coroutines, via a semantics-preserving translation through one-shot delimited control. The construction addresses failures in naïve translations by explicitly representing continuation validity and using two successive shift0 operations.

  • Translation: The EFFone-to-DELone translation handles a computation with a handler using nested dollar terms and a dispatcher derived from the handler clauses.The outer dollar delimits the translated computation, while the inner dollar delimits the handled computation and applies it to the operational dispatcher.
  • Translation: A continuation label is represented by a genuine DELone continuation label rather than a thunk, requiring two successive shift0 operations for strong macro-translation.A thunk-based representation would preserve only weak macro-expressibility because forcing a captured continuation could behave differently in EFFone and its translation.
  • Correctness: The correctness proof relates EFFone and DELone computations together with their stores, label maps, coherence conditions, and invariant conditions.The simulation tracks which continuations remain valid and how each EFFone continuation corresponds to a pair of DELone continuations.
  • Correctness: The translation preserves defined evaluation: an EFFone program evaluates if and only if its DELone translation evaluates.This preservation result yields the macro-expressibility theorem for EFFone in DELone.
  • Expressibility results: One-shot effect handlers are macro-expressible in one-shot delimited control and therefore in asymmetric coroutines.The first result is established by a translation from EFFone to DELone, followed by the previously developed DELone-to-AC result.
  • Expressibility results: Assuming shift0 is available among the effect operations, DELone is also macro-expressible in EFFone.Thus the two one-shot calculi are macro-expressively equivalent under the stated assumption.

5 One-shot effect handlers cannot macro-express asymmetric coroutines

The paper shows that effect handlers and one-shot delimited control cannot macro-express asymmetric coroutines, while asymmetric coroutines can express reference cells that DELone cannot. The separation relies on macro-expressibility’s local, homomorphic translation requirement and on the stronger state-changing behavior of reference cells.

  • Reference-cell separation: DELone cannot macro-express reference cells because its continuation stores can invalidate entries but cannot replace the content of a valid entry.The reference-cell counterexample distinguishes an initial value from a later updated value, behavior unavailable through the relevant DELone store operations.
  • Reference-cell separation: Asymmetric coroutines can macro-express reference cells, but DELone cannot weakly macro-express reference cells.The proof uses a reference-cell program whose second read observes an updated value, whereas DELone stores cannot replace the content of a valid entry.
  • Reference-cell separation: Because EFFone is macro-expressible in DELone, EFFone also cannot weakly macro-express asymmetric coroutines.The result follows by composing a hypothetical translation from AC to DELone with the established translation from EFFone to DELone.
  • Scope of the separation: Macro-expressibility prevents a translation from introducing a global handler, so effect handlers cannot macro-express global effects such as reference cells.This explains why general programming intuition about effect handlers expressing computational effects does not apply to this stricter notion of local, homomorphic translation.
  • Reverse separation: There is no weak macro-translation from DELone to REF, and consequently none from EFFone or AC to REF.The argument uses the absence of control effects in REF and macro-expressibility transitivity.
  • Reverse separation: In REF, computations inside a let frame cannot escape that frame to terminate successfully, unlike computations in DELone.This control-effect difference lets DELone distinguish computations that REF contexts cannot distinguish.

6 Related work

Prior work largely studied multi-shot control operators, while this paper systematically compares one-shot operators without mutable state. It also situates the comparison within macro-expressiveness and identifies limitations in earlier claims and translations.

  • Felleisen’s macro-expressibility provides the framework for rigorous comparisons among extensions of a common base calculus.
  • Earlier expressive-power studies mainly analyzed multi-shot control operators, leaving one-shot operators comparatively underexplored.
  • The paper is presented as the first systematic comparison of the relative expressive power of one-shot control operators.
  • Unlike earlier work involving mutable state, this study uses a base calculus without mutable states to isolate each control operator’s expressive power.
  • Earlier claims about one-shot yield and coroutine expressiveness lacked formal justification, motivating the paper’s rigorous treatment.

7 Conclusion

The paper establishes a one-way macro-expressibility hierarchy among one-shot control facilities and repairs a flawed informal translation argument. It further identifies scope boundaries and open directions involving relaxed translations and typing.

  • One-shot delimited-control operators and one-shot effect handlers can be macro-expressed by asymmetric coroutines.
  • The converse direction fails because reference cells are not macro-expressible in terms of effect handlers.
  • Reference cells were introduced into the construction to manage continuation validity, correcting a gap in the earlier argument.
  • The authors conjecture that relaxing macro-translation locality could allow EFFone to macro-express REF and AC.
  • Whether the untyped macro-expressibility results carry over to typed one-shot control operators remains open.
  • A systematic type-system design for the more general asymmetric coroutines studied here remains to be investigated.

A Supplementary proofs for Section 3

The supplementary material formalizes well-formedness, label mappings, coherence, invariants, and simulation relations for DELone and asymmetric coroutines. These definitions support preservation and translation reasoning.

  • Well-formedness: DELone and asymmetric-coroutine configurations are assigned explicit well-formedness conditions tracking labels, stores, and active continuations.
  • Preservation: Well-formedness is preserved by reductions in both calculi, supporting the subsequent simulation proofs.
  • Runtime correspondence: The supplementary development defines label maps that represent source continuation labels using reference cells and coroutine labels.
  • Runtime correspondence: Store-map coherence and invariant conditions relate source continuation validity to target reference-cell contents and coroutine labels.
  • Simulation: A core and simulation relation connects DELone configurations with asymmetric-coroutine configurations under well-formedness, coherence, and invariant side conditions.
  • Proof organization: The proof development canonicalizes target configurations before simulation, which simplifies the argument.

A.2 Proof

The proof establishes substitution and contextual properties for the DELone-to-coroutine relation, then derives simulation and initial correspondence. Structural induction handles ordinary contexts while specialized clauses handle dollar and yield constructs.

  • Substitution: Substitution preserves the core relation between DELone terms and asymmetric-coroutine terms.
  • Context decomposition: Pure-context reasoning decomposes related configurations into corresponding source and target contexts and computations.
  • Simulation: The reduction lemmas establish the DELone-to-coroutine simulation steps under the defined relation and side conditions.
  • Context decomposition: The proof treats dollar frames separately because their target form contains an active labeled computation.
  • Value translation: The value lemmas show that the runtime translation is homomorphic on ordinary constructors and maps source continuation labels to target labels.
  • Simulation: Corollary A.25 gives initial simulation for every DELone program from the empty stores and empty label map.

A.2.3 Simulation

The simulation proof establishes that each DELone reduction can be matched by an AC computation while preserving the source–target relation and its invariants. The argument handles ordinary reductions, control operations, errors, and contextual frames by case analysis.

  • Contextual cases: Pure-frame cases preserve the simulation because the induction hypothesis supplies the inner reduction and the same pure frame can be rebuilt.Source and target well-formedness are preserved, while coherence and invariants do not depend on the outer pure frame.
  • Contextual cases: In throw cases, the resumed coroutine differs from the outer coroutine, so the outer frame’s store conditions remain unchanged.The argument rules out equality of the two coroutine labels using the outer-frame side condition.
  • Contextual cases: In shift cases, freshness and well-formedness ensure that the newly created label and store update belong to an inner coroutine rather than the outer one.Consequently, both outer-frame side conditions are preserved when the inner dollar frame is rebuilt.
  • Simulation: Theorem A.28 states that every DELone step from related configurations has a corresponding AC configuration related to the source reduct.The proof uses case analysis on the source reduction rule and maintains well-formedness, coherence, and invariant conditions.
  • Stuck states: The simulation also covers stuck configurations: a stuck DELone configuration has an AC configuration that reduces to a stuck state.This is stated by Corollary A.32 after applying the simulation theorem to the source reduction sequence.

A.2.5 Strong macro-expressibility

This section proves strong macro-expressibility by showing that the translation preserves evaluation semantics in both directions. The result is then stated as a strong macro-translation from DELone to AC.

  • Semantic preservation: EvalDELone (M) is defined if and only if EvalAC for every translated DELone program.The proof considers successful evaluation and the three undefined cases: divergence, errors, and stuck configurations.
  • Undefined evaluations: The proof transfers source divergence, errors, and stuck states to corresponding non-successful target behavior.Determinism of AC prevents a target that reaches an error or stuck configuration from also terminating successfully.
  • Translation: The translation is homomorphic on MAM constructors and maps each DELone-specific constructor through a fixed syntactic abstraction.Theorem A.35 supplies semantic preservation, completing the strong macro-translation argument.
  • EFFone to DELone: The translation from EFFone to DELone is developed using label maps that track each source continuation label’s pair of target labels.Coherence and invariant conditions formalize the correspondence between source and target stores and continuations.

B.2 From DELone to EFFone

The DELone-to-EFFone proof defines a runtime correspondence between configurations and shows that every DELone step is simulated by EFFone. This yields preservation of evaluation semantics, including unsuccessful outcomes.

  • Simulation relation: The simulation relation requires translated computations, well-formed configurations, a label-map domain condition, and invariant correspondence between stores.The relation explicitly connects DELone continuation labels with EFFone labels and stored continuations.
  • Simulation: Proposition B.23 states that every DELone reduction from related configurations is matched by one or more EFFone reductions to a related configuration.The proof decomposes the translated computation into a corresponding evaluation context and redex.
  • Unsuccessful evaluations: DELone divergence is transferred to EFFone through repeated application of the simulation proposition.Because EFFone reduction is deterministic, the resulting infinite reduction sequence establishes divergence.
  • Unsuccessful evaluations: A DELone computation that gets stuck is translated to an EFFone computation that also gets stuck.The proof checks representative stuck-term forms by induction on the computation structure.
  • Semantic preservation: Corollary B.28 concludes that EvalDELone (M) is defined if and only if EvalEFFone for the translated computation.The converse direction handles divergence, stuckness, and failure separately.

C Supplementary proofs for Section 5.1

The supplementary proofs establish reachability and renaming properties for DELone stores and reductions. These results support reasoning about fresh labels, invalidation, and permutation-equivalent computations.

  • Reachability: Reach(E, θ) is defined as the smallest store-label set containing labels in E and labels reachable through non-nil store entries.This inductive characterization supports subsequent reachability-preservation arguments.
  • Reachability: Invalidating a store label cannot add reachable labels: Reach(M, θ′) remains a subset of Reach(M, θ0).The proof handles labels occurring directly in the term and labels reached through non-nil store entries.
  • Permutations: A finite permutation renames continuation labels while fixing a chosen subset of labels.Its action is defined on values, computations, and stores, enabling reduction arguments modulo fresh-name changes.
  • Permutation invariance: Reduction sequences can be transported through finite permutations that preserve a fixed label subset.The construction maintains renamed computations, stores, and fresh-label sets inductively across MAM, return, shift, and throw cases.
  • Permutation invariance: The inductive renaming proof preserves the step structure for ordinary rules and extends or invalidates renamed labels for shift and throw.At the end of the sequence, the returned value is the correspondingly renamed source value.

C.1.2 Proof of Theorem 5.1

The proof establishes a translation from REF to AC that preserves definedness, divergence, and stuckness, while a separate argument rules out a weak macro-translation from REF to DELone.

  • Separation result: REF cannot be weakly macro-translated to DELone.The contradiction uses a REF program whose two gets observe different stored injections, whereas the translated DELone form cannot preserve that distinction.
  • Translation and invariant: The REF-to-AC translation maps reference cells to coroutine labels and relates source and target configurations through an injective label map and store invariant.The relation preserves translated terms, domains, and corresponding stored values.
  • Translation and invariant: Simulation shows that every REF reduction step is matched by one or more AC steps while preserving the configuration relation.The proof extends the translation to contexts and establishes decomposition and substitution properties needed for simulation.
  • Semantic preservation: REF divergence and stuckness are preserved by the AC simulation, so undefined source evaluations cannot become successful target evaluations.The argument separately handles infinite reductions and configurations with no applicable reduction rule.
  • Semantic preservation: EvalREF(M) is defined if and only if EvalAC(⟦M⟧) is defined.The reverse direction uses the two possible undefined cases for REF: divergence or getting stuck.

D Supplementary proofs for Section 5.2

The supplementary proofs establish observational equivalence for REF thunks and use it to show that DELone cannot be weakly macro-translated to REF.

  • REF contextual properties: A REF configuration diverging in any evaluation context causes every enclosing evaluation context to diverge as well.This contextual divergence property supports the thunk-equivalence argument.
  • REF contextual properties: Forcing a thunk containing a computation leads to divergence or a stuck configuration rather than successful termination.The result follows from the behavior of let _ = M in Ω in REF.
  • REF contextual properties: REF thunks {L[M]} and {L[N]} are observationally equivalent for arbitrary computations M and N.Any context expecting a value terminates successfully with one thunk exactly when it does with the other.
  • REF contextual properties: The relation used for thunk equivalence preserves constructors, substitution, evaluation-context decomposition, and corresponding reduction rules.These properties yield a lock-step simulation except when forcing a thunk exposes a computation that cannot terminate successfully.
  • Separation result: DELone has two computations whose contexts distinguish their results, contradicting the observational equivalence that any translation into REF would impose.The evaluations produce injL1 V1 and injL2 V2, respectively.
Loading 2609.06443v1…