Danel Ahman: When programs have to watch paint dry
In this talk I will present some ongoing work on programming language design for modelling resources. A great amount of work on resources has focussed on their spatial properties, e.g., that certain resources must not be arbitrarily discarded or duplicated, or that programs have to obey a certain memory layout. In contrast, in our work we focus on temporal aspects of resources, e.g., as in asynchronous programming (where promise types are used to denote that an asynchronously computed value will be available at some later time point) or in manufacturing processes (where programs sometimes literally need to watch paint dry). Our goal is to develop general and mathematically natural programming language support for modelling such situations, while giving strong guarantees about when resources become available and can be used.
Our work draws inspiration from the recent investigations of Clouston and others on Fitch-style natural deduction and type systems for modal logics. In these proof systems the introduction and elimination rules for modalities are formulated with respect to modality-like operators on contexts of hypotheses (which are left adjoints to the modalities on formulae). In this talk, I will present a temporal variant of such modal type systems that naturally provides (i) a means for statically witnessing that certain values are available to a program only after some amount of execution time, and (ii) a means for guaranteeing that programs cannot try to use such values before at least the specified amount of time has passed. Importantly, the programs do not have to sit idly when waiting for (ii), but can meanwhile instead perform other (time-consuming) tasks, which we model by including algebraic effects (and effect handlers) with prescribed execution times. I will illustrate how the programs execute through the equational theory of the language. Finally, I will also present and discuss some details of the (currently work in progress) denotational semantics of the language based on graded monads and comonads, and adjunctions between them.
(This is joint work with Juhan-Peep Ernits from the Tallinn University of Technology.)
