In languages with algebraic effects (resp. monads), the usual way of modelling interactions with the external world is to define a dedicated effect (resp. monad) and then treat it specially in the compiler, such as the RandomInt effect in the Eff language and the IO monad in Haskell. This however has various drawbacks. For instance, such languages often lack enforcement mechanisms to ensure that a program does not write to an already closed file. And what is even worse, in languages with algebraic effects, where all effects can be handled, it is very easy to accidentally cause one's program not to even reach file closing, by discarding a continuation somewhere in the handler.

In this talk, I will present our ongoing work on using comodels of algebraic effects as a programming abstraction for (i) modelling the external world and interactions with it, (ii) ensuring the linearity of these interactions, and (iii) controlling which capabilities of the external world different parts of programs have access to. Regarding (ii), the novel aspect of our work is that we do not ensure linearity of these interactions by the means of a linear type system, but instead we leave the external world implicit and interact with it through a combination of algebraic operations and (under the hood) a linear state-passing translation analogous to that of Møgelberg and Staton. Regarding (i) and (ii), we do not limit the programmer to a single external world, but instead allow them to modularly build their own intermediate external worlds. In addition, in the talk I will also discuss two natural ways how a comodel (i.e., the external world) can communicate information back to the program being run using this comodel.

(This is joint work with Andrej Bauer)