Danel Ahman: Comodels as a gateway for interacting with the external world
Datum objave: 19. 3. 2019
Seminar za temelje matematike in teoretično računalništvo
Četrtek, 21. 3. 2019, od 11h do 13h, učilnica 3.07, Jadranska 21
Abstract: As much as we might try to convince ourselves, functional programming is rarely completely pure as one often cannot escape having to interact with the external world, e.g., by needing to write the results of one's program to a terminal window or a file, or perhaps also consult an external source of randomness for making nondeterministic and probabilistic choices. In this work we are exploring programming abstractions for orchestrating such interactions in a principled way.
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. The common denominator here is the lack of linearity guaranteed by these languages.
In this talk, I will present some of our initial findings on the use of 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 similar 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 the talk I will demonstrate these ideas through small programming examples, and if time permits, also comment on the opportunities and challenges involved in combining such use of comodels with effect handlers.
This is a joint (very much in progress) work with Andrej Bauer.
