Andrej Bauer: Effects in the real world
Attention: we meet at a non-standard time on Wednesday, 7. 10. 2020 at 16:00!
This seminar session is joint with OWLS seminar.
Joint work with Danel Ahman.
Abstract: In modern languages, computational effects are often structured using monads or algebraic effects and handlers. These mechanisms excel at implementation of computational effects within the language itself. For instance, the familiar implementation of mutable state in terms of state-passing functions requires no native state, and can be implemented either as a monad or using handlers. One is naturally drawn to using these techniques also for dealing with actual effects, such as manipulation of native memory and access to hardware. These are represented inside the language as algebraic operations or a monad, but treated specially by the language's top-level runtime, which invokes corresponding operating system functionality. While this approach works in practice, one wishes that the ingenuity of the language implementors were better supported by a more flexible methodology with a sound theoretical footing.
We address the issue by showing how to design a programming language based on runners of algebraic effects. We review runners, recast them as a programming construct, and present a calculus that captures the core ideas of programming with them. Through examples of runners we show how they capture both the interaction between the program and the external world, and encapsulation of programs in virtual environments that tightly control access to external resources and provide strong guarantees of proper resource finalization.
We accompanied our work with a prototype programming language Coop (https://github.com/andrejbauer/coop) and a Haskell library for runners (https://github.com/danelahman/haskell-coop).
References:
https://arxiv.org/abs/1910.11629
https://github.com/andrejbauer/coop
https://github.com/danelahman/haskell-coop
