A new draft paper, Resource-dependent Algebraic Effects, is available. Abstract:
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
effectshave been limited to simple state transitions which are known at compile-time. In this paper, I show how
effectscan 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.
I’ve just submitted this, although constructive comments and suggestions are still of course very welcome!