Programming and Reasoning with Algebraic Effects and Dependent Types
📜 Abstract
One often cited benefit of pure functional programming is that pure code is easier to test and reason about, both formally and informally. However, real programs have side-effects including state management, exceptions and interactions with the outside world. Haskell solves this problem using monads to capture details of possibly side-effecting computations — it provides monads for capturing State, I/O, exceptions, non-determinism, libraries for practical purposes such as CGI and parsing, and many others, as well as monad transformers for combining multiple effects. Unfortunately, useful as monads are, they do not compose very well. Monad transformers can quickly become unwieldy when there are lots of effects to manage, leading to a temptation in larger programs to combine everything into one coarse-grained state and exception monad. In this paper I describe an alternative approach based on handling algebraic effects, implemented in the IDRIS programming language. I show how to describe side effecting computations, how to write programs which compose multiple fine-grained effects, and how, using dependent types, we can use this approach to reason about states in effectful programs.
✨ Summary
Summary
The paper presents Effects, an embedded domain-specific language in Idris for programming with algebraic effects and handlers. It addresses limitations of monad-transformer stacks, particularly the dependence on transformer order, explicit lifting, and difficulty reusing computations that require only a subset of available effects. Effects are represented as a typed list of permitted resources, while EffM additionally tracks transitions between input and output effect resources.
The implementation uses dependent types to verify that invoked effects are available, automatically construct proofs of effect-list membership and sublist relationships, and track resource-state changes during execution. Handlers interpret algebraic operations in different computation contexts, allowing the same effectful program to be executed in contexts such as IO, Maybe, Either, or a pure simulation context. The paper demonstrates state, exceptions, console I/O, random-number generation, file protocols, and nondeterminism. File operations illustrate the central resource-tracking idea: the type system can require a file to be opened before reading and ensure that it is closed before a computation returns.
A larger example gives a dependently typed interpreter for a small imperative language. Its indexed syntax guarantees that variables are used with appropriate types, while the state effect tracks the type-indexed variable environment. The paper also identifies limitations: algebraic effects do not express every monadic computation, the initial interpreter has runtime overhead, state is reset across nondeterministic branches, and effect subprograms must preserve effect ordering unless an explicit permutation operation is used. (web.archive.org)
Influence
The work directly motivated subsequent development by Brady. Resource-dependent algebraic effects extends the approach from statically known resource transitions to transitions determined at runtime, applying the technique to file APIs and interactive games. (research-portal.st-andrews.ac.uk) The Idris Effects documentation presents the library as a practical continuation of this work and uses it to teach programming and reasoning about side-effecting programs. (docs.idris-lang.org)
The resource-dependent-effects approach was also applied to type-safe web programming, including CGI, database, and session resources, with static protocols intended to improve correctness and security. (researchgate.net) More broadly, the paper became part of the research lineage discussed in later work and community efforts concerning algebraic effect handlers. A 2018 Dagstuhl report describes subsequent research languages and libraries for OCaml, Haskell, Clojure, Scala, and other mainstream ecosystems, while identifying mainstream adoption and efficient implementation as ongoing goals. (drops.dagstuhl.de) The available evidence supports concrete influence on Idris libraries, resource-dependent effect research, and the broader effect-handler research program; it does not establish that this specific paper alone led to a particular commercial product adoption.