PaperlayerView exact revision on arXiv

Source-linked AI summary

An Effect System for Algebraic Effects and Handlers

Andrej Bauer, Matija Pretnar

arXiv:1306.6316v3cs.PLcs.LO

TL;DR

Core Eff needs an expressive effect system for a language with first-class algebraic effects and handlers. The paper defines that system and gives operational and denotational semantics; it proves safety and adequacy, then derives state equations including commutativity for non-interfering references.

  • Problem

    Eff’s first-class algebraic effects and handlers call for an effect system that balances simplicity with expressiveness.

    Source: §1 · p. 1

  • Method

    The paper defines an expressive effect system for core Eff, proves operational safety, and gives a domain-theoretic denotational semantics using Pitts’s theory of minimal invariant relations.

    Source: §1 · p. 2, §5 · p. 12

  • Results

    The operational semantics is proved safe with respect to the effect system, and the denotational semantics is proved adequate.

    Source: §1 · p. 2, §5.5 · p. 21

  • Takeaways & Limitations

    The resulting reasoning tools derive the usual equations for mutable state, including a commutativity law for computations using non-interfering references.

    Source: §1 · p. 2

    Core Eff omits dynamic creation of instances because it significantly complicates the effect system and semantics.

    Source: §9 · p. 28

Abstract

from arXiv · show

We present an effect system for core Eff, a simplified variant of Eff, which is an ML-style programming language with first-class algebraic effects and handlers. We define an expressive effect system and prove safety of operational semantics with respect to it. Then we give a domain-theoretic denotational semantics of core Eff, using Pitts's theory of minimal invariant relations, and prove it adequate. We use this fact to develop tools for finding useful contextual equivalences, including an induction principle. To demonstrate their usefulness, we use these tools to derive the usual equations for mutable state, including a general commutativity law for computations using non-interfering references. We have formalized the effect system, the operational semantics, and the safety theorem in Twelf.

1. Introduction

The paper develops an expressive effect system for core Eff and establishes safety and adequate denotational semantics. It then uses these results to derive contextual reasoning tools and equations for mutable state, including commutativity for computations using non-interfering references.

1. Introduction

  • The descriptive effect system tracks possible computational effects, and its non-monotonicity recognizes effects removed by handlers.A computation using mutable state can be determined pure when a handler handles away lookups and updates.Source: §1 · p. 1
  • Core Eff retains first-class handlers and instances while omitting dynamic instance creation.The paper presents it as a fragment retaining Eff’s essential features.Source: §1 · p. 2
  • The paper gives small-step and big-step operational semantics for core Eff and proves their safety with respect to the effect system.Source: §1 · p. 2
  • Using domain theory and Pitts’s theory of minimal invariant relations, the paper gives core Eff a denotational semantics and proves adequacy.Source: §1 · p. 2
  • The paper develops observational equivalences and an induction principle, then derives the standard equations for mutable state, including a commutativity law for non-interfering references.Source: §1 · p. 2
  • The effect system, operational semantics, and safety theorem are formalized in Twelf.Source: §1 · p. 2

2. Core Eff

Core Eff keeps first-class handlers and instances and accesses computational effects through operations. Its type system distinguishes pure expressions from computations that may call specified operations.

2. Core Eff

  • Core Eff retains first-class handlers and instances but omits dynamic creation of instances, which complicates the effect system and semantics.The language is restricted to a fragment with the features considered essential for conceptual analysis.Source: §2 · p. 2

2.1. Effects and types.

  • Effects are accessed through operations, and each effect has a fixed set of instances in core Eff.The paper notes that full Eff permits dynamic instance creation, but core Eff assumes a fixed set.Source: §2 · p. 2, §2.1 · p. 3

2.2. Terms.

  • Handlers are programmer-written, with a value case and operation cases; both handlers and instances are first-class values.Source: §2 · p. 2, §2.2 · p. 4

2.1. Effects and types.

  • A dirty type pairs a pure type with the finite set of operations that may be called during evaluation.Each listed operation must be well-formed for its instance and effect.Source: §2.1 · p. 3

3. Operational semantics

Core Eff represents operation calls with delimited continuations and handlers that can process matching operations. It defines both small-step and big-step semantics, which agree on evaluation results.

3. Operational semantics

  • An operation call carries an instance, operation, parameter, and delimited continuation; generic effects and let bindings express such calls in examples.Source: §3 · p. 4

3.1. Small-step semantics.

  • The small-step semantics reduces computations one step at a time, propagating unmatched operations and applying matching handler clauses to the operation parameter and continuation.The handler wraps itself around the continuation so later operations are handled as well.Source: §3.1 · pp. 5–6, §3 · p. 5

3.2. Big-step semantics.

  • The big-step and small-step semantics agree: a computation evaluates to a result under one exactly when it reaches that result under the other.Source: §3.2 · p. 8

4. An effect system

The effect system uses subtyping to preserve useful effect information and defines typing rules with operational safety guarantees. It also erases effect details into skeletal types while retaining type structure and uniqueness.

4.1. Subtyping.

  • Subtyping lets a pure function such as ignore join a conditional branch with a writing function without losing its empty-dirt type.Structural subtyping also helps distinguish which effect instances a handler handles.Source: §4.1 · pp. 8–9
  • Subtyping helps infer handler behavior: a precise instance type can show that a handler handles an operation, whereas a union of instances cannot guarantee which one is handled.Without subtyping, the example requires both instances to have the less precise union type.Source: §4.1 · pp. 8–9

4.2. Typing rules.

  • Handler typing checks that its value and operation cases share an outgoing type, and that effects are handled or remain in the output dirt.Operation-call dirt also accounts for possible operations in the continuation.Source: §4.2 · p. 9
  • A terminating computation of type A ! ∆ returns a value of type A or calls an operation in ∆; with empty dirt, it returns a pure value without operations.Progress and preservation support these safety guarantees.Source: §4.2 · pp. 9–10

4.3. Skeletal types.

  • Skeletal types erase effect information while preserving the underlying type structure; computations differing only in effects share a skeleton, and skeletal typing is unique in a given context.Expressions likewise retain the same skeletal type when their pure types differ only in effect information.Source: §4.3 · pp. 11–12

5. Denotational semantics

This section develops a domain-theoretic denotation for core Eff using minimal invariant constructions, establishes coherence across typing derivations, and relates it to operational semantics through soundness and adequacy. It extends adequacy from closed unit computations to operation observations and termination, showing that non-bottom denotations correspond to terminating computations.

5.1. Computation domains.

  • The computation domain is a minimal solution of a recursive domain equation, with recursion and induction principles for defining maps and proving admissible predicates.Its elements can be viewed as possibly non-well-founded trees; induction proceeds from bottom, value leaves, and operation nodes.Source: §5.1 · pp. 12–13

5.2. Semantics of skeletal types.

  • Skeletal types receive predomain meanings for pure types and domain meanings for dirty types, with recursive computation equations solved minimally.The computation-domain equations can be circular because they refer to operation argument and continuation types.Source: §5.2 · p. 13

5.3. Semantics of expressions and computations.

  • Typing contexts are interpreted as products of predomains, and judgments as continuous maps, with handler meanings defined recursively on computation domains.The expression and computation meanings are defined by induction on typing derivations.Source: §5.3 · p. 14
  • All derivations of a typing judgment give the same meaning because the semantics factors through unique skeletal derivations.The semantic rules ignore effect information and subsumption rules when factoring through skeletal derivations.Source: §5.2 · p. 13, §5.3 · p. 15

5.4. Semantics of effects.

  • Pitts's theorem [14] supplies an induction principle for effect-sensitive meanings, and the effect semantics fits together with the semantics of expressions and computations.The induction principle applies to admissible predicates on computation meanings, closed under the value and operation cases.Source: §5.4 · pp. 16–17

5.5. Soundness and adequacy.

  • Soundness and adequacy relate the operational and denotational semantics, with formal approximation relations and a fundamental lemma supporting the adequacy proof.The approximation relation for computations is defined recursively, and the fundamental lemma connects denotations of typed terms to their substitutions.Source: §5.5 · pp. 17–19
  • If a computation denotes an operation, it evaluates to that operation with an argument and continuation whose denotations match.The operation must belong to the computation’s effect set.Source: §5.5 · p. 21
  • Whenever a computation’s denotation is not bottom, the computation evaluates to some result.Source: §5.5 · p. 21

6. Equational reasoning

The section develops equational reasoning through contextual and denotational equivalence, then gives an induction principle for proving equivalences across effects. Denotational equality implies contextual equivalence, and the resulting principles validate program equations and support proofs tailored to particular effects.

6.1. Contextual and denotational equivalence.

  • Denotationally equal expressions and computations are contextually equivalent, connecting an easier-to-handle semantic equality to interchangeability in program contexts.The proof uses compositionality, soundness, and adequacy.Source: §6.1 · pp. 21–22
  • Denotational equivalence is a congruence, is preserved by well-typed substitutions, and validates β-rules for conditionals, matching, and operation handling.The rules include moving a let binding into an operation continuation.Source: §6.1 · p. 22
  • The equivalences also validate recursive-function unfolding and η-rules for values, functions, and let bindings, with suitable types required for the η-rules.The let η-rule is proved by induction in the next section.Source: §6.1 · p. 22
  • Let sequencing is equivalent to handling its computation with a value clause, and let associativity holds when the moved variable is not free in the final computation.The associativity equation is attributed to.Source: §6.1 · p. 22

6.2. An induction principle for effects.

  • The induction principle supports equivalence proofs for selected effects, avoiding consideration of operations irrelevant to the chosen handlers.For arbitrary computations, the proof checks nontermination, returned values, and each operation, then uses a continuation induction hypothesis.Source: §6.2 · p. 23
  • The principle proves the let η-rule by cases on nontermination, returned values, and operations; the operation case uses a β-rule and the induction hypothesis.A non-trivial application is presented in Section 7.2.Source: §6.2 · p. 23

7. Example: mutable references

The mutable-reference example shows how handlers implement state and how the effect system tracks which operations remain. The paper derives state equations and a commutativity law for computations using non-interfering references.

7. Example: mutable references

  • Handling a reference wraps a computation as a function expecting the current state, and applying it to an initial state yields a computation of type B ! ∆.When the computation's only effects are lookups and updates of that reference, the resulting computation is pure.Source: §7 · p. 24
  • A weaker reference type such as ref{ι1,ι2} prevents the system from deducing anything useful about the handled computation.The example also warns that state must be initialized at the correct point.Source: §7 · pp. 24–25

7.1. Reasoning about references.

  • The paper derives the seven standard equations for state, covering the combinations of lookup and update.These equations support stepwise simplification and mimic the usual coalgebraic operational semantics for state.Source: §7.1 · pp. 25–26
  • For different reference instances, lookup and update operations can be commuted, and the symmetric equations permit either nesting order for their handlers.The equations support moving operations across inner handlers that do not handle the relevant reference.Source: §7.1 · pp. 25–26

7.2. Commutativity of non-interfering computations.

  • Computations using only non-interfering references can be transposed, or run in parallel.The law exchanges the order of c1 and c2 while retaining their respective handlers and initial states.Source: §7.2 · p. 27
  • The general commutativity proof proceeds by induction on one computation, with the lookup and update cases handled by the induction hypothesis.The paper notes that the update proof is similar to the lookup proof.Source: §7.2 · p. 27

8. Formalization in Twelf

The authors formalized core Eff, its effect system, and the safety theorems in Twelf. The accompanying code is compatible with Twelf 1.7.1.

8. Formalization in Twelf

  • Core Eff, the effect system, and the safety theorems were formalized in Twelf, with code compatible with Twelf version 1.7.1.The files are enclosed with the paper or available from the cited repository.Source: §8 · p. 28

9. Discussion

The discussion identifies dynamic instance creation and non-termination as boundaries of the current effect system. It also notes prior exploration of effect inference and an available early prototype.

9. Discussion

  • Core Eff omits dynamic creation of instances with the new construct, which causes significant complications in both the effect system and semantics.The authors suggest nominal logic and nominal domain theory as one possible treatment.Source: §9 · p. 28
  • Non-termination is not reflected in the effect system, and adding a divergence effect would likely become uninformative because it could never be handled away.The authors suggest separating general recursive definitions from structural recursive definitions as a potential remedy.Source: §9 · p. 28
  • A realistic implementation would need to infer computational effects; this possibility was explored by the second author and an early prototype is available in Eff.The passage identifies the prototype as an early implementation.Source: §9 · p. 28
Loading 1306.6316v3…