Safe mutation with algebraic effects

Abstract

It can be difficult to write safe concurrent programs which use shared mutable state. Subtle mistakes can lead to data races that manifest as unexpected program behaviour. The prevailing approaches to solving this dilemma are to either eschew mutable state altogether, or design bespoke languages that prevent data races by design. This article introduces a third approach by showing how safe mutation can be integrated into a mainstream functional programming language with algebraic effects. This article produces a framework that tracks the use of mutable state and guarantees data race freedom at compile time.