PaperlayerView exact revision on arXiv

Source-linked AI summary

Programming with Algebraic Effects and Handlers

Andrej Bauer, Matija Pretnar

arXiv:1203.1539v1cs.PL

TL;DR

Eff explores a programming language based on algebraic computational effects and handlers, motivated by easier effect combination and new interactions between effects and handlers. It models effects algebraically, supports flexible delimited control, and demonstrates programming techniques including backtracking and selection functionals.

  • Problem

    An experiment in programming-language design is warranted because algebraic effects may combine more easily than monads and enable new interactions between effects and handlers.

  • Method

    Eff models computational effects as algebraic operations and handlers as homomorphisms, with ML-like type judgments that omit computational-effect information.

  • Results

    The authors report that the language-design experiment succeeded and demonstrate techniques including backtracking, selection functionals, and flexible delimited control.

  • Takeaways & Limitations

    Eff supports first-class effects and handlers that can combine existing effects and support programming techniques using delimited continuations.

  • Takeaways & Limitations

    Eff lacks a static effect system, and effect ordering can make simple changes in addition order materially affect behavior.

Abstract

from arXiv · show

Eff is a programming language based on the algebraic approach to computational effects, in which effects are viewed as algebraic operations and effect handlers as homomorphisms from free algebras. Eff supports first-class effects and handlers through which we may easily define new computational effects, seamlessly combine existing ones, and handle them in novel ways. We give a denotational semantics of eff and discuss a prototype implementation based on it. Through examples we demonstrate how the standard effects are treated in eff, and how eff supports programming techniques that use various forms of delimited continuations, such as backtracking, breadth-first search, selection functionals, cooperative multi-threading, and others.

Introduction

Eff explores programming with algebraic effects and handlers, treating effects as algebraic operations and handlers as homomorphisms. The paper presents the language, its semantics and implementation, and examples of standard effects and delimited-control techniques.

  • Motivation: Eff models computational effects as operations of an algebraic theory and effect handlers as homomorphisms induced by free algebras.The framework covers effects including input, output, state, exceptions, and non-determinism, as well as handlers for exceptions, stream redirection, transactions, and backtracking.
  • Motivation: Effects combine more easily than monads, motivating an experimental programming language based on algebraic effects and handlers.The paper presents this language experiment as a way to investigate the interaction between effects and handlers.
  • Paper scope: The paper develops eff’s syntax, constructs, type checking, domain-theoretic semantics, prototype implementation, and examples.Examples cover standard computational effects and their variations and combinations.
  • Implementation: Eff’s implementation is freely available online.The paper provides the implementation URL.

1 Syntax

Eff’s syntax distinguishes pure expressions from effectful computations in its core language, while concrete syntax permits them to be mixed. It provides constructs for conditionals, instances, handlers, and pattern matching.

  • Core syntax: Eff is statically typed and includes effect types and handler types in addition to standard types.The core presentation focuses on monomorphic types, while the full language also has polymorphism and type inference.
  • Expressions and computations: Expressions are inert and effect-free, whereas computations may diverge or cause computational effects.The concrete syntax hides this distinction and allows expressions and computations to be freely mixed.
  • Handlers: A handler is written with operation, value, and finally clauses.The handler syntax binds operation parameters and continuations in operation clauses.
  • Core constructs: The syntax includes conditionals, instance creation, handling constructs, and match forms for booleans, products, sums, and the empty type.Expressions introduce unit, product, sum, and function values.
  • Expressions and computations: Arithmetic expressions count as computations because arithmetic operators are built-in constants applied to their operands.This uniformly treats arithmetic operations, including potentially effectful operations such as division by zero.

2 Constructs specific to eff

Eff provides instances, operations, handlers, continuations, and resources as constructs for defining and controlling computational effects. Handlers interpret operations and can transform computations, while resources supply default behavior.

  • Instances and operations: A terminating computation evaluates either to a value or to an operation applied to a parameter.This provides the operational intuition for eff’s effect constructs.
  • Instances and operations: new E generates a fresh effect instance, while its extended form associates the instance with a resource defining default operation behavior.Examples include references and communication channels.
  • Instances and operations: An applied operation e # op e′ is computationally effectful, with behavior determined by enclosing handlers and the associated resource.The operation itself, before application, is a value and therefore effect-free.
  • Handlers: A handler processes a computation with value and operation clauses, binding the continuation when an operation is encountered.The continuation is delimited by the handling construct and is handled by the same handler.
  • Handlers: The finally clause wraps the handler’s result with an additional transformation.For state, this transformation applies the resulting function to the initial state.
  • Resources: Unhandled operations propagate outward and eventually receive behavior from their effect instance’s resource.A resource carries state and prescribes default operation behavior; its operation computation returns a value and a new state.

3 Type checking

Eff uses ML-like type checking without encoding computational effects in types. Its rules type expressions, computations, effect instances, operations, and handlers, including the transformations performed by handler clauses.

  • Typing discipline: Eff’s types do not capture information about computational effects.The language uses separate judgements for expressions and computations.
  • Typing discipline: Expression and computation judgements assign types within a context of variables and their associated types.The standard rules cover expressions, promotions, let statements, and elimination forms.
  • Instances: Instance creation checks the initial state type and requires each operation computation to return a result paired with a state.For an operation op_i : A_i → B_i, its computation has result type B_i × C when the instance state has type C.
  • Handlers: Handlers are typed as functions from computations of type A to computations of type C through an intermediate computation type B.The value and operation clauses produce B, while the finally clause transforms B into C.

4 Denotational semantics

The denotational semantics explains eff evaluation by interpreting expressions and computations in domains of values and results, with handlers transforming computations and resources carrying stateful operation behavior.

  • Semantic domains: A terminating computation is represented as either a value or an operation carrying an instance, operation, parameter, and continuation.Results include a bottom element for ill-formed values and runtime errors.
  • Semantic domains: The semantics interprets expressions as maps from environments to values and computations as maps from environments to results.The framework avoids fixing particular domains, requiring only properties that can be realized through domain equations or universal domains.
  • Handlers: Handlers interpret selected operations by applying their clauses to parameters and continuations, while forwarding unhandled operations through the handler.Value and finally clauses complete the transformation of handled computations.
  • Core constructs: Monadic-style binding sequences computation results by lifting a function over the result of the first computation.Recursive functions use a least fixed point to define their denotation.
  • Resources and evaluation: Resources extend effect instances with operation-dependent state transitions, and top-level evaluation threads this state through operations and continuations.The denotation of a top-level computation is evaluated from its result representation under an implicit resource state.

5 Implementation

The prototype interpreter follows the denotational semantics while adding practical language features, including Hindley–Milner inference, polymorphism, and syntax that hides expression–computation distinctions.

  • Prototype: The prototype’s main evaluation loop is essentially the same as the denotational semantics described for eff.It also adds recursive type definitions, for and while loops, and pattern matching.
  • Type inference: Hindley–Milner type inference with parametric polymorphism makes the implemented language usable without requiring explicit type annotations.The value restriction follows the distinction between expressions and computations.
  • Syntax and desugaring: Concrete syntax permits expressions and computations to be mixed, then separates them through desugaring.The desugaring phase inserts val and hoists computations into enclosing let statements.
  • Syntax and desugaring: Simultaneous let bindings avoid choosing an ordering for computations whose effects may interact.The prototype evaluates bindings in source order and can warn about potentially unexpected effect ordering.
  • Handler syntax: Inline syntax supports one-off handlers, with omitted val and finally clauses defaulting to identities.This reduces the notation needed for common handler applications.

6 Examples

Eff uses first-class effects and handlers to express nondeterminism, exceptions, and state, while allowing handlers to customize control flow and resource behavior.

  • Choice: Handlers for nondeterministic choice call continuations multiple times and combine the resulting values into lists.A choice handler can therefore enumerate all possible results rather than selecting one branch.
  • Choice: The computation with two choices produces [10;5;20;15] when both choices are handled by a list-collecting handler.Changing handler and operation order changes the nesting and arrangement of the resulting lists.
  • Exceptions: Eff exceptions use a raise operation with an empty result type, preventing the continuation from being restarted by an exception handler.An optionalizing handler converts a computation that may raise a specified exception into an optional result.
  • State: State is represented by lookup and update operations, and a state handler passes state through continuations to reproduce ML-style references.A custom handler can instead connect a reference to external persistent storage.
  • Resources: Resources allow handlers to define stateful operation behavior directly, extending effect instances with initial state and operation-dependent transitions.This resource mechanism is presented as a solution for controlling reference behavior beyond a handler’s lexical scope.

6.4 Transactions

Eff examples show transactional state, lazy evaluation, and testable input/output handlers, illustrating how handlers control state commitment, evaluation, and external interaction.

  • Transactions: Transactional state uses temporary state and commits it only when the handled computation terminates with a value.An exception therefore leaves the original reference unchanged.
  • Transactions: A transaction that raises exception e with parameter 69 does not change the value of reference r.The handler preserves updates temporarily until successful completion.
  • Lazy evaluation: Lazy resources evaluate a thunk on the first force operation, store the resulting value, and return it immediately on later forces.The resource state changes from Thunk t to Value v after the first evaluation.
  • Lazy evaluation: Deferred computations cannot trigger operations inside resources; doing so produces a runtime error.The paper notes that an effect system could prevent such deferred effectful computations statically.
  • Input and output: Input and output handlers can replace standard streams with list-based behavior, making interactive programs amenable to unit testing.The paper explicitly identifies both handlers as useful for unit testing.
  • Input and output: Intercepting writes makes the example produce (42, ["hello"; "world"]) without printing anything.The handler accumulates output in a list instead of sending it to standard output.

6.7 Ambivalent choice and backtracking

Eff’s ambivalent choice handler searches alternatives until the overall computation succeeds, while breadth-first handling schedules choice points through a stateful queue. Combining backtracking with state requires placing state handling inside the backtracking scope.

  • Ambivalent choice: The amb handler tries each choice through the continuation until one succeeds, yielding depth-first search for problems such as 8 queens.
  • Breadth-first search: A breadth-first handler stores continuation-and-argument pairs in a queue, enqueues new choice points, then activates dequeued points.
  • State and backtracking: In the 8 queens example, state handled outside amb is not restored during backtracking, so a placed queen is never removed and the search fails.
  • State and backtracking: Handling state inside amb restores the state during backtracking, and the revised program finds the same solution as the first version.
  • Choice recording: The handler can record choices and reuse them across repeated invocations, preserving consistent selections while searching for a successful result.
  • Selection functionals: Eff’s selection handler can implement Escardó’s selection functional by computing a basic neighborhood where the proposition is true and choosing a witness from it.
  • Selection functionals: Compared with the Haskell implementation, eff’s intensional search is more efficient but not extensional.

6.9 Probabilistic choice

Eff models probabilistic choice with handlers that process finite probability distributions and compute expected values or result distributions. The examples show that effect order, especially between state and probabilistic choice, can change correctness.

  • Probabilistic effects: Probabilistic choice selects list elements according to a probability distribution represented by weighted alternatives.
  • Probabilistic effects: The expected-value handler folds over alternatives, weighting each continuation result by its associated probability.
  • Probabilistic effects: Eff computes result distributions by scaling alternative distributions and combining entries with distribution-style folding.
  • Combining effects: A random walk example combines probabilistic choice with state, using left, stationary, and right steps with probabilities 2/10, 3/10, and 5/10.
  • Combining effects: The state handler must be enclosed by the distribution handler in the random-walk example, although the reverse order also works in the presented program.
  • Combining effects: Swapping the order of state lookup and probabilistic choice can prevent state restoration and produce the wrong answer.

6.10 Cooperative multithreading

Eff implements cooperative multithreading with first-class effects and handlers, using a recursive round-robin scheduler to manage continuations as threads. The examples also show that Eff directly supports delimited control and rejects unrestricted recursive self-application during type checking.

  • Cooperative multithreading: Cooperative multithreading runs several threads in parallel conceptually, while allowing only one thread to execute at a time.Threads are created with fork, relinquish control with yield, and are selected by a scheduler.
  • Cooperative multithreading: The example defines yield and fork as effect operations, then implements a round-robin scheduler as a handler.The scheduler maintains and activates suspended continuations represented as thunks.
  • Cooperative multithreading: Yield queues the current continuation and activates the first queued thread, while fork queues the current thread and activates a recursively handled new thread.The recursive handler ensures operations triggered by the new thread remain handled.
  • Cooperative multithreading: Threads can be combined with other effects, including shared or private state, exceptions, and nested multithreading.This demonstrates composition of cooperative threads with other effect handlers.
  • Delimited control: Eff implements standard delimited continuations by treating reset as a handler and shift as an operation.The shift handler wraps the captured continuation application in reset so nested shift operations remain handled.
  • Delimited control: The captured continuation in the example yields 2×(2×(2×7+1)+1)+1 = 63, while unrestricted self-application is rejected because α = α →β has no solved recursive type.Turning off type checking allows the self-application puzzle to print the same answer as in Scheme.

7 Discussion

The discussion concludes that Eff successfully realizes a language based on algebraic effects and handlers, while identifying open questions about effect analysis, program reasoning, and delimited control. These questions concern balancing effect-system complexity, handling effect instances in equational reasoning, and understanding non-algebraic continuations in an effectful setting.

  • Conclusion: Eff’s design goal was to provide a programming language based on the algebraic approach to computational effects and handlers, and the authors judge the experiment successful.They describe the experiment as holding many promises.
  • Open questions: An effect system is needed for static analysis of computational effects, but a useful design must balance expressivity against complexity.The authors identify this balance as an unresolved requirement.
  • Open questions: Reasoning about Eff programs remains an open issue because effect instances may complicate equational reasoning.The discussion points toward algebraically inspired reasoning while noting the complication introduced by instances.
  • Open questions: Eff provides flexible and clean delimited control even though continuations are non-algebraic and were not part of the original design agenda.The authors identify this as a surprising basis for investigating control operators in effectful settings.
Loading 1203.1539v1…