Programming with algebraic effects and handlers
From MaRDI portal
Publication:478396
DOI10.1016/J.JLAMP.2014.02.001zbMATH Open1304.68025arXiv1203.1539OpenAlexW3103594074WikidataQ115902568 ScholiaQ115902568MaRDI QIDQ478396FDOQ478396
Authors: Andrej Bauer, Matija Pretnar 
Publication date: 3 December 2014
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Abstract: 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.
Full work available at URL: https://arxiv.org/abs/1203.1539
Recommendations
Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- A theory of type polymorphism in programming
- Modelling environments in call-by-value programming languages.
- Algebraic operations and generic effects
- Combining effects: sum and tensor
- Handlers of Algebraic Effects
- Title not available (Why is that?)
- A new approach to abstract syntax with variable binding
- Combining algebraic effects with continuations
- From comodels to coalgebras: state and arrays
- Title not available (Why is that?)
- Selection functions, bar recursion and backward induction
- Representing Control: a Study of the CPS Transformation
- Title not available (Why is that?)
- Tensors of comodels and models for operational semantics
- An introduction to algebraic effects and handlers (invited tutorial paper)
Cited In (48)
- Mac Lane's comparison theorem for the Kleisli construction formalized in Coq
- A Functional Abstraction of Typed Invocation Contexts
- Sound and complete type inference for closed effect rows
- Asymptotic speedup via effect handlers
- Title not available (Why is that?)
- Handlers in action
- Introducing \(\llparenthesis\lambda\rrparenthesis\), a \(\lambda \)-calculus for effectful computation
- When programs have to watch paint dry
- Shallow effect handlers
- Fusion for free. Efficient algebraic effect handlers
- Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala
- A type system for effect handlers and dynamic labels
- Runners in Action
- Structured handling of scoped effects
- Not by equations alone. Reasoning with extensible effects
- Continuity of Gödel's system T definable functionals via effectful forcing
- Signature restriction for polymorphic algebraic effects
- One-shot algebraic effects as coroutines
- Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics
- Modular verification of programs with effects and effect handlers in Coq
- Automated temporal verification for algebraic effects
- Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
- Applicative programming with effects
- An effect system for algebraic effects and handlers
- Introducing a calculus of effects and handlers for natural language semantics
- Handling algebraic effects
- Do be do be do
- Higher-order asynchronous effects
- Eff
- Understanding algebraic effect handlers via delimited control operators
- Efficient algebraic effect handlers for Prolog
- Validating Brouwer's continuity principle for numbers using named exceptions
- Interactive programming in Agda -- objects and graphical user interfaces
- Latent Effects for Reusable Language Components
- An introduction to algebraic effects and handlers (invited tutorial paper)
- Modular verification of programs with effects and effects handlers
- Explicit effect subtyping
- Handlers of Algebraic Effects
- Turing-Completeness Totally Free
- Title not available (Why is that?)
- Combining predicate transformer semantics for effects: a case study in parsing regular languages
- Continuation passing style for effect handlers
- Doo bee doo bee doo
- Effect handlers via generalised continuations
- Local algebraic effect theories
- An effect system for algebraic effects and handlers
- Programming and reasoning with algebraic effects and dependent types
- No value restriction is needed for algebraic effects and handlers
Uses Software
This page was built for publication: Programming with algebraic effects and handlers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q478396)
