Computer Laboratory

Publications

" We present a general semantic account of Gifford-style type-and-effect systems. These type systems provide lightweight static analyses annotating program phrases with the sets of possible computational effects they may cause, such as memory access and modification, exception raising, and non-deterministic choice. The analyses are used, for example, to justify the program transformations typically used in optimising compilers, such as code reordering and inlining. Despite their existence for over two decades, there is no prior comprehensive theory of type-and-effect systems accounting for their syntax and semantics, and justifying their use in effect-dependent program transformation. We achieve this generality by recourse to the theory of algebraic effects, a development of Moggi’s monadic theory of computational effects that emphasises the operations causing the effects at hand and their equational theory. The key observation is that annotation effects can be identified with the effect operations. Our first main contribution is the uniform construction of semantic models for type-and-effect analysis by a process we call conservative restriction. Our construction requires an algebraic model of the unannotated programming language and a relevant notion of predicate. It then generates a model for Gifford-style type-and-effect analysis. This uniform construction subsumes existing ad-hoc models for type-and-effect systems, and is applicable in all cases in which the semantics can be given via enriched Lawvere theories. Our second main contribution is a demonstration that our theory accounts for the various aspects of Gifford-style effect systems. We begin with a version of Levy’s Call-by-push-value that includes algebraic effects. We add effect annotations, and design a general type-and-effect system for such call-by-push-value variants. The annotated language can be thought of as an intermediate representation used for program optimisation. We relate the unannotated semantics to the conservative restriction semantics, and establish the soundness of program transformations based on this effect analysis. We develop and classify a range of validated transformations, generalising many existing ones and adding some new ones. We also give modularly-checkable sufficient conditions for the validity of these optimisations. In the final part of this thesis, we demonstrate our theory by analysing a simple example language involving global state with multiple regions, exceptions, and non-determinism. We give decision procedures for the applicability of the various effect-dependent transformations, and establish their soundness and completeness.“”

“Plotkin and Pretnar’s handlers for algebraic effects occupy a sweet spot in the design space of abstractions for effectful computation. By separating effect signatures from their implementation, alge- braic effects provide a high degree of modularity, allowing pro- grammers to express effectful programs independently of the con- crete interpretation of their effects. A handler is an interpretation of the effects of an algebraic computation. The handler abstraction adapts well to multiple settings: pure or impure, strict or lazy, static types or dynamic types. This is a position paper whose main aim is to popularise the handler abstraction. We give a gentle introduction to its use, a col- lection of illustrative examples, and a straightforward operational semantics. We describe our Haskell implementation of handlers in detail, outline the ideas behind our OCaml, SML, and Racket implementations, and present experimental results comparing han- dlers with existing code.”"

" We present a general theory of Gifford-style type and effect annotations, where effect annotations are sets of effects. Generality is achieved by recourse to the theory of algebraic effects, a development of Moggi’s monadic theory of computational effects that emphasises the operations causing the effects at hand and their equational theory. The key observation is that annotation effects can be identified with operation symbols.

We develop an annotated version of Levy’s Call-by-Push-Value language with a kind of computations for every effect set; it can be thought of as a sequential, annotated intermediate language. We develop a range of validated optimisations (i.e., equivalences), generalising many existing ones and adding new ones. We classify these optimisations as structural, algebraic, or abstract: structural optimisations always hold; algebraic ones depend on the effect theory at hand; and abstract ones depend on the global nature of that theory (we give modularly-checkable sufficient conditions for their validity).“”

“We propose a probabilistic interpretation of a class of reversible communicating processes. The rate of forward and backward computing steps, instead of being given explicitly, is derived from a set of formal energy parameters. This is similar to the Metropolis-Hastings algorithm. We find a lower bound on energy costs which guarantees that a process converges to a probabilistic equilibrium state (a grand canonical ensemble in statistical physics terms). This implies that such processes hit a success state in finite average time, if there is one.”"

Talks

We present a theory of Gifford-style type-and-effect annotations, where effect annotations are sets of effects, such as memory accesses or exceptions. Our theory accounts for effect-dependent program transformations for functional-imperative languages, as used in optimizing compilers. Generality is achieved by recourse to the theory of algebraic effects, a development of Moggi’s monadic theory of computational effects that emphasizes the operations causing the effects at hand. The key observation is that annotation effects denote algebraic operations. After presenting our general type-and-effect system and its semantics, we validate and generalize existing optimizations and add new ones. Our theory also suggests a classification of these optimizations into three classes, structural, local, and global: structural optimizations always hold; local ones depend on the effect theory at hand; and global ones depend on the global nature of that theory, such as idempotency or absorption laws. We also give modularly-checkable necessary and sufficient conditions for validating the optimizations. Joint work with Gordon Plotkin.

We present a theory of Gifford-style type-and-effect annotations, where effect annotations are sets of effects, such as memory accesses or exceptions. Our theory accounts for effect-dependent program transformations for functional-imperative languages, as used in optimizing compilers. Generality is achieved by recourse to the theory of algebraic effects, a development of Moggi’s monadic theory of computational effects that emphasizes the operations causing the effects at hand. The key observation is that annotation effects denote algebraic operations. After presenting our general type-and-effect system and its semantics, we validate and generalize existing optimizations and add new ones. Our theory also suggests a classification of these optimizations into three classes, structural, local, and global: structural optimizations always hold; local ones depend on the effect theory at hand; and global ones depend on the global nature of that theory, such as idempotency or absorption laws. We also give modularly-checkable necessary and sufficient conditions for validating the optimizations. Joint work with Gordon Plotkin.

We present a general theory of Gifford-style type-and-effect annotations, where effect annotations are sets of effects, such as memory accesses or exceptions. Our theory accounts for effect-dependent program transformations for functional-imperative languages, as used in optimising compilers. Using our theory, we validate and generalise many existing optimisations and add new ones. Our general theory also suggests a classification of these optimisations into three classes, structural, local, and global. We also give modularly-checkable necessary and sufficient conditions for validating the optimisations.

Generality is achieved by recourse to the theory of algebraic effects, a development of Moggi’s monadic theory of computational effects that emphasises the operations causing the effects at hand. The universal algebraic perspective gives an elementary and concrete view on the monadic concepts. The key observation is that annotation effects can be identified with the algebraic operation symbols. We describe how the universal algebraic approach gives particularly simple characterisations of the optimisations: structural optimisations always hold; local ones depend on the effect theory at hand; and global ones depend on the global nature of that theory, such as idempotency or absorption laws. Time permitting, we outline how the theory generalises to more sophisticated notions of universal algebra via enriched Lawvere theories and factorisation systems.

Joint work with Gordon Plotkin.

A brief introduction to programming language semantics. We will covere key aspects of the operational and denotational approaches, including type soundness, denotational soundness, adequacy. I will present a logical relations proof, and show how category theory allows to restructure it as a model in a suitable category of predicates.

We present operational semantics for effect handlers. Introduced by Plotkin and Pretnar, effect handlers form the basis of Bauer and Pretnar’s Eff programming language. Our talk outlines three contributions. * We propose the first small-step structural operational semantics for a higher-order programming language with effect handlers, and a sound type and effect system. * We exhibit two alternative effect handler implementation techniques using free monads, and using composable continuations.

  • We show that Filinski’s monadic reflection is subsumed by effect handlers.

We present a small-step operational semantics for a simplified Call-by-Push-Value variant of Bauer and Pretnar’s Eff programming language. Eff incorporates functional and imperative features by adapting Plotkin and Pretnar’s effect handlers as a programming paradigm.

This is preliminary work with Sam Lindley and Nicolas Oury.

We present a general theory of Gifford-style type and effect annotations, where effect annotations are sets of effects. Generality is achieved by recourse to the theory of algebraic effects, a development of Moggi’s monadic theory of computational effects that emphasises the operations causing the effects at hand and their equational theory. The key observation is that annotation effects can be identified with operation symbols.

We develop an annotated imperative and functional language with a kind of computations for every effect set; it can be thought of as a sequential, annotated intermediate language. We develop a range of validated optimisations (i.e., equivalences), generalizing many existing ones and adding new ones. We classify these optimisations as structural, algebraic, or abstract: structural optimisations always hold; algebraic ones depend on the effect theory at hand; and abstract ones depend on the global nature of that theory (we give modularly-checkable sufficient conditions for their validity). Joint work with Gordon Plotkin, to appear in POPL’12.

We present a general theory of Gifford-style type and effect annotations, where effect annotations are sets of effects. Generality is achieved by recourse to the theory of algebraic effects, a development of Moggi’s monadic theory of computational effects that emphasises the operations causing the effects at hand and their equational theory. The key observation is that annotation effects can be identified with operation symbols.

We develop an annotated version of Levy’s Call-by-Push-Value language with a kind of computations for every effect set; it can be thought of as a sequential, annotated intermediate language. We develop a range of validated optimisations (i.e., equivalences), generalising many existing ones and adding new ones. We classify these optimisations as structural, algebraic, or abstract: structural optimisations always hold; algebraic ones depend on the effect theory at hand; and abstract ones depend on the global nature of that theory (we give modularly-checkable sufficient conditions for their validity).

Joint work with Gordon Plotkin.

We present a general theory of Gifford-style type and effect annotations, where effect annotations are sets of effects. Generality is achieved by recourse to the theory of algebraic effects, a development of Moggi’s monadic theory of computational effects that emphasises the operations causing the effects at hand and their equational theory. The key observation is that annotation effects can be identified with operation symbols. We develop an annotated imperative and functional language with a kind of computations for every effect set; it can be thought of as a sequential, annotated intermediate language. We develop a range of validated optimisations (i.e., equivalences), generalising many existing ones and adding new ones. We classify these optimisations as structural, algebraic, or abstract: structural optimisations always hold; algebraic ones depend on the effect theory at hand; and abstract ones depend on the global nature of that theory (we give modularly-checkable sufficient conditions for their validity).

Joint work with Gordon Plotkin, to appear in POPL’12.

Defining the formal meaning of programming languages has been investigated for nearly half a century. The foundational questions in the field have impact on programming language theoreticians, designers and implementors. In this quasi-historical session, we’ll review the goals underlining semantics, and how operational and denotational methods have been devised to investigate them. The review will be followed by a short discussion about the current state of the theory, tools and methodologies available. Was it a big waste of time?

We propose a semantic foundation for optimisations based on type and effect analysis. We present a multiple-effect CBPV-based calculus whose denotational semantics is based on an effect-indexed structure of adjunctions. When the underlying set of effects is specified by an algebraic theory, we take effects to be given by sets of operations. The required adjunction structure can then be obtained via a uniform process of conservative restriction of the theory. The calculus and its semantics is then extended by a straightforward generalisation of Pretnar and Plotkin’s effect handlers to arbitrary, non-algebraic, inter-effect handlers.

The modular composition of effects then boils down to ex- tension conservativeness, and we show that some common ways to compose arbitrary effects by sums and tensors are indeed conservative. In particular we obtain conservative extension results for both the sum of a monad and a free monad, and also for a unification of three common instances of the tensor of theories that is obtained using monoid actions. This unification includes the usual reader, state and writer monads and monad transformers.

We use our calculus and its semantics to provide general effect- dependent optimisations. We exemplify the machinery developed by deriving a language with state, IO and exceptions, and their handlers. Many of the already known effect-dependent optimisations are then particular cases of our general ones. We have thus demonstrated the possibility of a general theory of effect optimisations based on the algebraic theory of effects.

Joint work with Gordon Plotkin.

There is a conceptual connection between the State, Reader and Writer monads. However, the State and Reader monads only require a type, whereas the Writer monad requires a monoid. I will introduce and use Plotkin’s and Power’s algebraic theory of effects to formalise this connection using the notions of monoid actions and conservative restriction. This work results in a generalised notion of the State and Reader monads and monad transformers for an arbitrary monoid action. This is joint work with Gordon Plotkin.

At the end of last year, a prominent Category Theorist revealed a well kept secret on the categories mailing list. I will present a brief overview of the various threads that erupted from this revelation, and how they are relevant to Your Research (TM).

Reports