Algebraic Effects and Handlers for Software Transactional Memory

Abstract

Algebraic effects and handlers has been a popular approach for modelling side-effects in functional programming languages. Focusing on composability and modularity, this approach separates the effectful syntax from its semantics, which helps programmers to create effect abstractions such that their implementation can be modified without changing the syntax. However, there exist mainstream functional programming languages, like Haskell, which lack built-in frameworks to accommodate specifying side-effects in this manner. In this paper, we provide an interface for Haskell's Software Transactional Memory (STM), a concurrency abstraction, in the framework of algebraic effects and handlers from prior literature. We embed our implementation into a simple concurrency model using higher-order effects, in order to demonstrate it is possible to define and execute effectful concurrent programs that obey the semantics of Haskell's STM. Furthermore, we prove that our implementation satisfies the necessary laws governing our interface, such that programmers can easily reason about programs using our STM model.