Resource-dependent algebraic effects

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

19 Citations (Scopus)


There has been significant interest in recent months in finding new ways to implement composable and modular effectful programs using handlers of algebraic effects. In my own previous work, I have shown how an algebraic effect system (called effects) can be embedded directly in a dependently typed host language. Using dependent types ought to allow precise reasoning about programs; however, the reasoning capabilities of effects have been limited to simple state transitions which are known at compile-time. In this paper, I show how effects can be extended to support reasoning in the presence of run-time state transitions, where the result may depend on run-time information about resource usage (e.g. whether opening a file succeeded). I show how this can be used to build expressive APIs, and to specify and verify the behaviour of interactive, stateful programs. I illustrate the technique using a file handling API, and an interactive game.
Original languageEnglish
Title of host publicationTrends in Functional Programming
Subtitle of host publication15th International Symposium, TFP 2014, Soesterberg, The Netherlands, May 26-28, 2014. Revised Selected Papers
EditorsJurriaan Hage, Jay McCarthy
Place of PublicationCham
ISBN (Electronic)9783319146751
ISBN (Print)9783319146744
Publication statusPublished - 2014
EventTrends in Functional Programming, 15th International Symposium - Soesterberg, Netherlands
Duration: 26 May 201428 May 2014
Conference number: 15

Publication series

NameLecture Notes in Computer Science (including book subseries Theoretical Computer Science and General Issues)
Volume8843 (LNCS)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceTrends in Functional Programming, 15th International Symposium
Abbreviated titleTFP 2014


  • Dependent type
  • Functional programming
  • Game state
  • Game rule
  • Syntactic sugar


Dive into the research topics of 'Resource-dependent algebraic effects'. Together they form a unique fingerprint.

Cite this