Programming contextual computations

Abstract

Modern computer programs are executed in a variety of different contexts: on servers, handheld devices, graphics cards, and across distributed environments, to name a few. Understanding a program’s contextual requirements is therefore vital for its correct execution. This dissertation studies contextual computations, ranging from application-level notions of context to lower-level notions of context prevalent in common programming tasks. It makes contributions in three areas: mathematically structuring contextual computations, analysing contextual program properties, and designing languages to facilitate contextual programming. Firstly, existing work which mathematically structures contextual computations using comonads (in programming and semantics) is analysed and extended. Comonads are shown to exhibit a shape preservation property which restricts their applicability to a subset of contextual computations. Subsequently, novel generalisations of comonads are developed, including the notion of an indexed comonad, relaxing shape-preservation restrictions. Secondly, a general class of static analyses called coeffect systems is introduced to describe the propagation of contextual requirements throughout a program. Indexed comonads, with some additional structure, are shown to provide a semantics for languages whose contextual properties are captured by a coeffect analysis. Finally, language constructs are presented to ease the programming of contextual computations. The benefits of these language features, the mathematical structuring, and coeffect systems are demonstrated by a language for container programming which guarantees optimisations and safety invariants.