Liberating effects with rows and handlers

D. Hillerström, S. Lindley

Research output: Chapter in Book/Report/Conference proceedingConference contribution

22 Citations (Scopus)

Abstract

Algebraic effects and effect handlers provide a modular abstraction for effectful programming. They support user-defined effects, as in Haskell, in conjunction with direct-style effectful programming, as in ML. They also present a structured interface to programming with delimited continuations. In order to be modular, it is necessary for an effect type system to support extensible effects. Row polymorphism is a natural abstraction for modelling extensibility at the level of types. In this paper we argue that the abstraction required to implement extensible effects and their handlers is exactly row polymorphism. We use the Links functional web programming language as a platform to substantiate this claim. Links is a natural starting point as it uses row polymorphism for polymorphic variants, records, and its built-in effect types. It also has infrastructure for manipulating continuations. Through a small extension to Links we smoothly add support for effect handlers, making essential use of rows in the frontend and first-class continuations in the backend. We demonstrate the usability of our implementation by modelling the mathematical game of Nim as an abstract computation. We interpret this abstract computation in a variety of ways, illustrating how rows and handlers support modularity and smooth composition of effectful computations. We present a core calculus of row-polymorphic effects and handlers based on a variant of A-normal form used in the intermediate representation of Links. We give an operational semantics for the calculus and a novel generalisation of the CEK machine that implements the operational semantics, and prove that the two coincide. © TyDe 2016 - Proceedings of the 1st International Workshop on Type-Driven Development, co-located with ICFP 2016. All rights reserved.
Original languageEnglish
Title of host publicationTyDe 2016: Proceedings of the 1st International Workshop on Type-Driven Development
PublisherAssociation for Computing Machinery
Pages15-27
Number of pages13
ISBN (Print)9781450344357
DOIs
Publication statusPublished - 18 Sep 2016

Keywords

  • Abstract machine semantics
  • Algebraic effects
  • Delimited control
  • Effect handlers
  • Effect typing
  • Operational semantics
  • Abstracting
  • Algebra
  • Calculations
  • Computer programming languages
  • Semantics
  • Abstract machines
  • Functional programming

Fingerprint Dive into the research topics of 'Liberating effects with rows and handlers'. Together they form a unique fingerprint.

  • Cite this

    Hillerström, D., & Lindley, S. (2016). Liberating effects with rows and handlers. In TyDe 2016: Proceedings of the 1st International Workshop on Type-Driven Development (pp. 15-27). Association for Computing Machinery. https://doi.org/10.1145/2976022.2976033