" We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languages for building Bayesian models of the kinds used in computational statistics and machine learning. Among them are untyped languages, similar to Church and WebPPL, because our semantics allows recursive mixed-variance datatypes. Our semantics justifies important program equivalences including commutativity.
Our new semantic model is based on `quasi-Borel predomains’. These are a mixture of chain-complete partial orders (cpos) and quasi-Borel spaces. Quasi-Borel spaces are a recent model of probability theory that focuses on sets of admissible random elements. Probability is traditionally treated in cpo models using probabilistic powerdomains, but these are not known to be commutative on any class of cpos with higher order functions. By contrast, quasi-Borel predomains do support both a commutative probabilistic powerdomain and higher-order functions. As we show, quasi-Borel predomains form both a model of Fiore’s axiomatic domain theory and a model of Kock’s synthetic measure theory. "
“Partially-static data structures are a well-known technique for improving binding times. However, they are often defined in an ad-hoc manner, without a unifying framework to ensure full use of the equations associated with each operation. We present a foundational view of partially-static data structures as free extensions of algebras for suitable equational theories, i.e. the coproduct of an algebra and a free algebra in the category of algebras and their homomorphisms. By precalculating these free extensions, we construct a high-level library of partially static data representations for common algebraic structures. We demonstrate our library with common use-cases from the literature: string and list manipulation, linear algebra, and numerical simplification.”
“We present an architectural design of a library for Bayesian modelling and inference in modern functional programming languages. The novel aspect of our approach are modular correct-by-construction implementations of existing state-of-the-art inference algorithms. Our design relies on three inherently functional features: higher-order functions, inductive data-types, and support for either type-classes or an expressive module system. We provide a performant Haskell implementation of this architecture, demonstrating that high-level and modular probabilistic programming can be added as a library in sufficiently expressive languages. We review the core abstractions in this architecture: inference representations, inference transformations, and inference representation transformers. We then implement concrete instances of these abstractions, counterparts to particle filters and Metropolis-Hastings samplers, which form the basic building blocks of our library. By composing these building blocks we obtain state-of-the-art inference algorithms: Resample-Move Sequential Monte Carlo, Particle Marginal Metropolis-Hastings, and Sequential Monte Carlo squared. We evaluate our implementation against existing probabilistic programming systems and find it is already com- petitively performant, although we conjecture that existing functional programming optimisation techniques could reduce the overhead associated with the abstractions we use. We show that our modular design enables deterministic testing of inherently stochastic Monte Carlo algorithms. Finally, we demonstrate using OCaml that an expressive module system can also implement our design.”
“Type-and-effect systems incorporate information about the computational effects, e.g., state mutation, probabilistic choice, or I/O, a program phrase may invoke alongside its return value. A semantics for type-and-effect systems involves a parameterised family of monads whose size is exponential in the number of effects. We derive such refined semantics from a single monad over a category, a choice of algebraic operations for this monad, and a suitable factorisation system over this category. We relate the derived semantics to the original semantics using fibrations for logical relations. Our proof uses a folklore technique for lifting monads with operations.”
“We present a modular semantic account of Bayesian inference algorithms for probabilistic programming languages, as used in data science and machine learning. Sophisticated inference algorithms are often explained in terms of composition of smaller parts. However, neither their theoretical justification nor their implementation reflects this modularity. We show how to conceptualise and analyse such inference algorithms as manipulating intermediate representations of probabilistic programs using higher-order functions and inductive types, and their denotational semantics.
Semantic accounts of continuous distributions use measurable spaces. However, our use of higher-order functions presents a substantial technical difficulty: it is impossible to define a measurable space structure over the collection of measurable functions between arbitrary measurable spaces that is compatible with standard operations on those functions, such as function application. We overcome this difficulty using quasi-Borel spaces, a recently proposed mathematical structure that supports both function spaces and continuous distributions.
We define a class of semantic structures for representing probabilistic programs, and semantic validity criteria for transformations of these representations in terms of distribution preservation. We develop a collection of building blocks for composing representations. We use these building blocks to validate common inference algorithms such as Sequential Monte Carlo and Markov Chain Monte Carlo. To emphasize the connection between the semantic manipulation and its traditional measure theoretic origins, we use Kock’s synthetic measure theory. We demonstrate its usefulness by proving a quasi-Borel counterpart to the Metropolis-Hastings-Green theorem.”
“We compare the expressive power of three programming abstractions for user-defined computational effects: Bauer and Pretnar’s effect handlers, Filinski’s monadic reflection, and delimited control without answer-type-modification. This comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features.
We present three calculi, one per abstraction, extending Levy’s call-by-push-value. For each calculus, we present syntax, operational semantics, a natural type-and-effect system, and, for effect handlers and monadic reflection, a set-theoretic denotational semantics. We establish their basic meta-theoretic properties: safety, termination, and, where applicable, soundness and adequacy. Using Felleisen’s notion of a macro translation, we show that these abstractions can macro-express each other, and show which translations preserve typeability. We use the adequate finitary set-theoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macro-expressed while preserving typeability either by monadic reflection or by delimited control. We supplement our development with a mechanised Abella formalisation.”
“Higher-order probabilistic programming languages allow programmers to write sophisticated models in machine learning and statistics in a succinct and structured way, but step outside the standard measure-theoretic formalization of probability theory. Programs may use both higher-order functions and continuous distributions, or even define a probability distribution on functions. But standard probability theory cannot support higher-order functions, that is, the category of measurable spaces is not cartesian closed.
Here we introduce quasi-Borel spaces. We show that these spaces: form a new formalization of probability theory replacing measurable spaces; form a cartesian closed category and so support higher-order functions; form an extensional category and so support good proof principles for equational reasoning; and support continuous probability distributions. We demonstrate the use of quasi-Borel spaces for higher-order functions and probability by: showing that a well-known construction of probability theory involving random functions gains a cleaner expression; and generalizing de Finetti’s theorem, that is a crucial theorem in probability theory, to quasi-Borel spaces.”
“We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the heaps. We derive a monad for full ground references supporting effect masking by applying a state monad transformer to the encapsulation monad. To evaluate the monad, we present a denotational semantics for a call-by-value calculus with full ground references, and validate associated code transformations.”
“We present a straightforward, sound, Hindley-Milner polymorphic type system for algebraic effects and handlers in a call-by-value calculus, which, to our surprise, allows type variable generalisation of arbitrary computations, and not just values. We first recall that the soundness of unrestricted call-by-value Hindley-Milner polymorphism is known to fail in the presence of computational effects such as reference cells and continuations, and that many programming examples can be recast to use effect handlers instead of these effects. After presenting the calculus and its soundness proof, formalised in Twelf, we analyse the expressive power of effect handlers with respect to state effects. We conjecture handlers alone cannot express reference cells, but show they can simulate dynamically scoped state, establishing that dynamic binding also does not need a value restriction.”
“The process of inverting Markov kernels relates to the important subject of Bayesian modelling and learning. In fact, Bayesian update is exactly kernel inversion. In this paper, we investigate how and when Markov kernels (aka stochastic relations, or probabilistic mappings, or simply kernels) can be inverted. We address the question both directly on the category of measurable spaces, and indirectly by interpreting kernels as Markov operators:
For the direct option, we introduce a typed version of the category of Markov kernels and use the so-called ‘disintegration of measures’. Here, one has to specialise to measurable spaces borne from a simple class of topological spaces -e.g. Polish spaces (other choices are possible). Our method and result greatly simplify a recent development in Ref. [4].
For the operator option, we use a cone version of the category of Markov operators (kernels seen as predicate transformers). That is to say, our linear operators are not just continuous, but are required to satisfy the stronger condition of being ω-chain-continuous. Prior work shows that one obtains an adjunction in the form of a pair of contravariant and inverse functors between the categories of L_{1}- and L_{∞}-cones [3]. Inversion, seen through the operator prism, is just adjunction. No topological assumption is needed.
We show that both categories (Markov kernels and ω-chain-continuous Markov operators) are related by a family of contravariant functors T_{p} for 1 ≤ p ≤ ∞. The T_{p}’s are Kleisli extensions of (duals of) conditional expectation functors introduced in Ref. [3].
With this bridge in place, we can prove that both notions of inversion agree when both defined: if f is a kernel, and f^{†} its direct inverse, then T_{∞}(f)^{†} = T_{1}(f^{†}).
“We study the semantic foundation of expressive probabilistic programming languages, that support higher-order functions, continuous distributions, and soft constraints (such as Anglican, Church, and Venture). We define a metalanguage (an idealised version of Anglican) for probabilistic computation with the above features, develop both operational and denotational semantics, and prove soundness, adequacy, and termination. They involve measure theory, stochastic labelled transition systems, and functor categories, but admit intuitive computational readings, one of which views sampled random variables as dynamically allocated read-only variables. We apply our semantics to validate nontrivial equations underlying the correctness of certain compiler optimisations and inference algorithms such as sequential Monte Carlo simulation. The language enables defining probability distributions on higher-order functions, and we study their properties.”
“We discuss two inference patterns for inferring the coevolution of two characters based on their properties at a single point in time and determine when developmental interactions can be used to deduce evolutionary order. We discuss the use of the inference patterns we present in the biological literature and assess the arguments’ validity, the degree of support they give to the evolutionary conclusion, how they can be corroborated with empirical evidence, and to what extent they suggest new empirically addressable questions. We suggest that the developmental argument is uniquely applicable to cognitive-cultural coevolution.”
“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.”
“Characterising colimiting omega-cocones of projection pairs in terms of least upper bounds of their embeddings and projections is important to the solution of recursive domain equations. We present a universal characterisation of this local property as omega-cocontinuity of locally continuous functors. We present a straightforward proof using the enriched Yoneda embedding. The proof can be generalised to Cattani and Fiore’s notion of locality for adjoint pairs.”
Talk given at the 7th ACM SIGPLAN Workshop on Higher-Order Programming with Effects, 23 September, 2018.
We describe ongoing work investigating a convenient category of predomains and a probabilistic powerdomain construction suitable for statistical probabilistic programming semantics, as used in statistical modelling and machine learning. Our goal is to give adequate semantics to a probabilistic higher-order language with recursive types, and includes types for powers of real numbers and arbitrary measurable functions between them.
Specifically, we provide (1) a cartesian closed category; (2) whose objects are (pre)-domains; and (3) a commutative monad for continuous probabilistic choice and Bayesian conditioning. Jones and Plotkin have shown that conditions (2)–(3) hold when one restricts attention to continuous domains, and Jung and Tix have proposed to search for a suitable category of continuous domains possessing all three properties (1)–(3), a question that remains open to date.
We propose an alternative direction, considering spaces with separate, but compatible, measure-theoretic and domain-theoretic structures. On the domain-theoretic side, we require posets with suprema of countably increasing chains (omega-cpos). On the measure-theoretic side, we require a quasi-Borel space (qbs) structure, a recently introduced algebraic structure suitable for modelling higher-order probability theory. There are three equivalent characterisations of this category given by: imposing an order-theoretic separatedness condition on countable-product-preserving omega-cpo-valued contra-variant functors; internal omega-cpos in the quasi-topos of quasi-Borel spaces; and an essentially algebraic presentation. The category of these omega-qbses validates Fiore and Plotkin’s axiomatic domain theory, yielding semantics for recursive types. We construct a commutative powerdomain construction by factorising the Lebesgue integral from the space of random elements to the space of countably additive linear integration operators.
Talk given at the invited talk, International Workshop on Domain Theorey and its Applications, 08 July, 2018.
I will describe ongoing work investigating a convenient category of pre-domains and a probabilistic powerdomain construction suitable for statistical probabilistic programming semantics, as used in statistical modelling and machine learning. Specifically, we provide (1) a cartesian closed category; (2) whose objects are (pre)-domains; and (3) a commutative monad for probabilistic choice and Bayesian conditioning. Jones and Plotkin have shown that conditions (2)–(3) hold when one restricts attention to continuous domains, and Jung and Tix have proposed to search for a suitable category of continuous domains possessing all three properties (1)–(3), a question that remains open to date.
I propose an alternative direction, considering spaces with separate, but compatible, measure-theoretic and domain-theoretic structures. On the domain-theoretic side, we require posets with suprema of countably increasing chains (omega-cpos). On the measure-theoretic side, we require a quasi-Borel space (qbs) structure, a recently introduced algebraic structure suitable for modelling higher-order probability theory. There are three equivalent characterisations of this category given by: imposing an order-theoretic separatedness condition on countable-preserving omega-cpo-valued presheaves; internal omega-cpos in the quasi-topos of quasi-Borel spaces; and an essentially algebraic presentation. The category of these omega-qbses validates Fiore and Plotkin’s axiomatic domain theory, yielding semantics for recursive types. To conclude, I will describe a commutative powerdomain construction given by factorising the Lebesgue integral from the space of random elements to the space of sigma-linear integration operators
Talk given at the Theoretische Informatik Seminar, Department of Computer Science, Faculty of Engineering, Friedrich-Alexander-Universität Erlangen-Nürnberg, 25 June, 2018.
I will describe how to build a monad on a functor category to model dynamic allocation of potentially cyclic memory cells. In particular I’ll explain how to tackle the challenge of ‘effect masking’ which means roughly that ‘if you don’t need to know about memory access then you can’t detect it.’, and use this monad to give a denotational account of an ML-like language with reference cells, and validate associated program transformations.
I will explain the main insight behind our construction: identifying the collection of stores as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the stores. I will then obtain the full ground storage monad by applying a state monad transformer to the encapsulation monad.
A brief overview of probabilistic programming for statistical modelling and machine learning. Report on recent advances in the modular validation of similarly modular implementations of generic Bayesian inference algorithms such as Sequential Monte Carlo and Trace Markov Chain Monte Carlo. Report on ongoing work on a Haskell implementation of these ideas and its performance evaluation with respect to existing probabilistic programming systems.
Joint with Adam Ścibior, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Zoubin Ghahramani, Sean K. Moss, and Chris Heunen.
I will present a semantic account of Bayesian inference algorithms for probabilistic programming languages, as used in Bayesian data science and machine learning. Sophisticated inference algorithms are often explained in terms of composition of smaller parts. However, neither their theoretical justification nor their implementation reflect this modularity. I will show how to conceptualise and analyse such inference algorithms as manipulating intermediate representations of probabilistic programs using higher-order functions and inductive types, and their denotational semantics.
Semantic accounts of continuous distributions use measurable spaces. However, this use of higher-order functions presents a substantial technical difficulty: it is impossible to define a measurable space structure over the collection of measurable functions between arbitrary measurable spaces that is compatible with standard operations on those functions, such as application. I will explain how to overcome this difficulty using quasi-Borel spaces, a recently proposed mathematical structure that supports both function spaces and continuous distributions. To make the semantic manipulation closer to its traditional measure theoretic origins, I will review and use Kock’s synthetic measure theory. This notation was useful for proving a quasi-Borel counterpart to the Metropolis-Hastings-Green theorem.
Joint with Adam Ścibior, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Zoubin Ghahramani, Sean K. Moss, and Chris Heunen.
I will present a semantic account of Bayesian inference algorithms for probabilistic programming languages, as used in Bayesian data science and machine learning. Sophisticated inference algorithms are often explained in terms of composition of smaller parts. However, neither their theoretical justification nor their implementation reflect this modularity. I will show how to conceptualise and analyse such inference algorithms as manipulating intermediate representations of probabilistic programs using higher-order functions and inductive types, and their denotational semantics.
Semantic accounts of continuous distributions use measurable spaces. However, this use of higher-order functions presents a substantial technical difficulty: it is impossible to define a measurable space structure over the collection of measurable functions between arbitrary measurable spaces that is compatible with standard operations on those functions, such as application. I will explain how to overcome this difficulty using quasi-Borel spaces, a recently proposed mathematical structure that supports both function spaces and continuous distributions. To make the semantic manipulation closer to its traditional measure theoretic origins, I will review and use Kock’s synthetic measure theory. This notation was useful for proving a quasi-Borel counterpart to the Metropolis-Hastings-Green theorem.
Joint with Adam Ścibior, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Zoubin Ghahramani, Sean K. Moss, and Chris Heunen.
We compare the expressive power of three programming abstractions for user-defined computational effects: Bauer and Pretnar’s effect handlers, Filinski’s monadic reflection, and delimited control without answer-type-modification. This comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features.
We present three calculi, one per abstraction, extending Levy’s call-by-push-value. For each calculus, we present syntax, operational semantics, a natural type-and-effect system, and, for effect handlers and monadic reflection, a set-theoretic denotational semantics. We establish their basic meta-theoretic properties: safety, termination, and, where applicable, soundness and adequacy. Using Felleisen’s notion of a macro translation, we show that these abstractions can macro-express each other, and show which translations preserve typeability. We use the adequate finitary set-theoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macro-expressed while preserving typeability either by monadic reflection or by delimited control. We supplement our development with a mechanised Abella formalisation.
I will present a semantic account of Bayesian inference algorithms for probabilistic programming languages, as used in Bayesian data science and machine learning. Sophisticated inference algorithms are often explained in terms of composition of smaller parts. However, neither their theoretical justification nor their implementation reflects this modularity. I will show how to conceptualise and analyse such inference algorithms as manipulating intermediate representations of probabilistic programs using higher-order functions and inductive types, and their denotational semantics.
Semantic accounts of continuous distributions use measurable spaces. However, this use of higher-order functions presents a substantial technical difficulty: it is impossible to define a measurable space structure over the collection of measurable functions between arbitrary measurable spaces that is compatible with standard operations on those functions, such as application. I will explain how to overcome this difficulty using quasi-Borel spaces, a recently proposed mathematical structure that supports both function spaces and continuous distributions.
More specifically, I will define a semantic class of structures for representing probabilistic programs, and semantic validity criteria for transformations of these representations in terms of distribution preservation. I will review a collection of building blocks for composing representations, and show how to use these building blocks to validate common inference algorithms such as Sequential Monte Carlo and Markov Chain Monte Carlo. To make the semantic manipulation closer to its traditional measure theoretic origins, I will review and use Kock’s synthetic measure theory. This notation was useful for proving a quasi-Borel counterpart to the Metropolis-Hastings-Green theorem, which I will also describe.
Joint with Adam Ścibior, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Zoubin Ghahramani, Sean K. Moss, and Chris Heunen.
We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the heaps. We derive a monad for full ground references supporting effect masking by applying a state monad transformer to the encapsulation monad. To evaluate the monad, we present a denotational semantics for a call-by-value calculus with full ground references, and validate associated code transformations.
Higher-order probabilistic programming languages allow programmers to write sophisticated models in machine learning and statistics in a succinct and structured way, but step outside the standard measure-theoretic formalization of probability theory. Programs may use both higher-order functions and continuous distributions, or even define a probability distribution on functions. But standard probability theory cannot support higher-order functions, that is, the category of measurable spaces is not cartesian closed.
Here we introduce quasi-Borel spaces. We show that these spaces: form a new formalization of probability theory replacing measurable spaces; form a cartesian closed category and so support higher-order functions; form an extensional category and so support good proof principles for equational reasoning; and support continuous probability distributions. We demonstrate the use of quasi-Borel spaces for higher-order functions and probability by: showing that a well-known construction of probability theory involving random functions gains a cleaner expression; and generalizing de Finetti’s theorem, that is a crucial theorem in probability theory, to quasi-Borel spaces.
Talk given at the University of Oxford Department of Computer Science Quantum Group Workshop, 13 May, 2017.
I will explain what quasi-Borel spaces are, and outline how we’ve been using them as a convenient alternative to measurable spaces in probability theory and probabilistic programming that has well-behaved higher-order, logical, and algebraic structure.
(Joint work with Chris Heunen, Adam Scibior, Sam Staton, Matthijs Vakar, and Hongseok Yang.)
I will describe how to build a monad on a functor category to model dynamic allocation of potentially cyclic memory cells. In particular I’ll explain how to tackle the challenge of ‘effect masking’ which means roughly that ‘if you don’t need to know about memory access then you can’t detect it.’, and use this monad to give a denotational account of an ML-like language with reference cells, and validate associated program transformations.
I will explain the main insight behind our construction: identifying the collection of stores as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the stores. I will then obtain the full ground storage monad by applying a state monad transformer to the encapsulation monad.
The talk is based on work with: Paul B. Levy, Sean K. Moss, and Sam Staton (http://arxiv.org/abs/1702.04908).
We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the heaps. We derive a monad for full ground references supporting effect masking by applying a state monad transformer to the encapsulation monad. To evaluate the monad, we present a denotational semantics for a call-by-value calculus with full ground references, and validate associated code transformations.
Joint work with: Paul B. Levy, Sean K. Moss, and Sam Staton.
We compare the expressive power of three programming abstractions for user-defined computational effects: Bauer and Pretnar’s effect handlers, Filinski’s monadic reflection, and delimited control. This comparison allows a precise discussion about the relative merits of each programming abstraction.
We present three calculi, one per abstraction, extending Levy’s call-by-push-value. These comprise syntax, operational semantics, a natural type-and-effect system, and, for handlers and reflection, a set-theoretic denotational semantics. We establish their basic meta-theoretic properties: adequacy, soundness, and strong normalisation. Using Felleisen’s notion of a macro translation, we show that these abstractions can macro-express each other, and show which translations preserve typeability. We use the adequate finitary set-theoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macro-expressed while preserving typeability either by monadic reflection or by delimited control. We supplement our development with a mechanised Abella formalisation.
Joint work with Yannick Forster, Sam Lindley, and Matija Pretnar.
We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the heaps. We derive a monad for full ground references supporting effect masking by applying a state monad transformer to the encapsulation monad. To evaluate the monad, we present a denotational semantics for a call-by-value calculus with full ground references, and validate associated code transformations.
Joint work with: Paul B. Levy, Sean Moss, and Sam Staton.
Talk given at the 4th South of England Regional Programming Language Seminar (S-REPLS4), Imperial College London, 27 September, 2016.
Monads are the de-facto mechanism for adding user-defined computational effects to programming languages. Support for monads has been developed in general-purpose statically-typed functional programming languages such as Haskell and OCaml, proof assistants such as Coq, and other verification tools such as F-star. Algebraic effects and handlers are a recently developed programming abstraction that allows programmers to define and program with custom effects using a specific delimited-control structure. This control structure has straightforward type-system, computational intuition, operational and denotational semantics, and reasoning principles.
Our goal is to compare the expressive power of programming constructs facilitating user-defined effects. We consider a calculus of effect handlers, Filinski’s calculus of monadic reflection, which encapsulate user-defined monads as a programmable abstraction, and a calculus of the standard delimited control operators shift-zero and reset. We compare the calculi using Felleisen’s notion of macro translations. When we ignore the natural type systems associated with each calculus, each pair of abstractions is macro inter-translateable, but this translation does not preserve typability. We present preliminary results regarding the non-existence of typability-preserving macro-translations, and extensions to the type system that preserve typability.
Joint work with Yannick Forster, Sam Lindley, and Matija Pretnar.
Talk given at the HOPE’16 Workshop, 18 September, 2016.
We present ongoing work developing a straightforward denotational semantics for reference cells of arbitrary types based on sets- with-structure and structure-preserving functions. We start with full ground references — which can refer to ground values and (recursively) ground references — where types denotes set-valued presheaves. By considering stores as mixed-variance set-valued functors (i.e., profunctors), we obtain two monads for full ground state which can interpret alloction, dereference, and mutation of full ground references, while validating the usual equations. We use this structure to give a denotational semantics to a monadic metalanguage with a special construct for effect masking similar to Haskell’s runST. Time permitting, we speculate how to extend this approach, using an appropriate recursive domain equation, to account for ML-like general reference cells.
We present a straightforward, sound Hindley-Milner polymorphic type system for algebraic effects and handlers in a call-by-value calculus, which allows type variable generalisation of arbitrary computations, not just values. This result is surprising. On the one hand, the soundness of unrestricted call-by-value Hindley-Milner polymorphism is known to fail in the presence of computational effects such as reference cells and continuations. On the other hand, many programming examples can be recast to use effect handlers instead of these effects. Analysing the expressive power of effect handlers with respect to state effects, we claim handlers cannot express reference cells, and show they can simulate dynamically scoped state. Time permitting, we will discuss the denotational soundness theorem that led to this work.
Talk given at the 4th ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE’15), 30 August, 2015.
Hindley-Milner let-polymorphism in the presence of computational effects, notably local state mixed with type recursion, requires restriction to achieve type soundness. Existing solutions either restrict generalisation over type variables, excluding opportunities for sound polymorphism, or use types that expose the effectful nature of the implementation. Our goal is to analyse the problem and existing solutions denotationally, with the hope that such models will provide new insights.
We present an intrinsically-typed (Church-style) zeroth-order calculus of let-polymorphism. We define a fibrational denotational semantics to the pure calculus, drawing on ideas from models of the polymorphic lambda calculus, modifying Seeley’s PL categories to use Ulmer’s relative adjunctions. We outline ongoing and future work how to extend the pure semantics to include higher-order functions and relative monads, and to incorporating local state and recursive types into models by recursive domain equations. We conclude by speculating how to use these postulated models to analyse the value restriction and other solutions.
Talk given at the Domains XI Workshop, 09 September, 2014.
Characterising colimiting omega-cocones of projection pairs in terms of least upper bounds of their embeddings and projections is important to the solution of recursive domain equations. We present a universal characterisation of this local property as omega-cocontinuity of locally continuous functors. We present a straightforward proof using the enriched Yoneda embedding. The proof can be generalised to Cattani and Fiore’s notion of locality for adjoint pairs.
Purely functional languages use sequences of monad transformers called monad stacks to incorporate computational effects modularly. The current practice is to intuitively find the appropriate stack for a given task using intractable brute force and heuristics. We investigate a systematic alternative. By restricting attention to algebraic stack combinations, we provide a linear-time algorithm for generating all the appropriate monad stacks, or decide no such stack exist. Our approach is based on Hyland, Plotkin, and Power’s algebraic analysis of monad transformers, who propose a graph-theoretical solution to this problem. We extend their analysis with a straightforward connection to series-parallel graphs, and demonstrate a web-tool for generating monad stacks from a graph denoting the commutative interaction of effects.
Purely functional languages, e.g. Haskell, incorporate computational effects modularly using sequences of monad transformers, termed monad stacks. The current practice is to find the appropriate stack for a given task intuitively. By restricting attention to algebraic stack combinations, we provide a linear-time algorithm for generating all the appropriate monad stacks, or decide no such stacks exist. Our approach is based on Hyland, Plotkin, and Power’s algebraic analysis of monad transformers, who propose a graph-theoretical solution to this problem. We extend their analysis with a straightforward connection to the modular decomposition of a graph and to cographs, a.k.a. series-parallel graphs. We present an accessible and self-contained account of this monad-stack generation problem, and, more generally, of the decomposition of a combined algebraic theory into sums and tensors, and its algorithmic solution. We provide a web-tool implementing this algorithm intended for semantic investigations of effect combinations and for monad stack generation.
Haskell incorporates computational effects modularly using sequences of monad transformers, termed monad stacks. The current practice is to find the appropriate stack for a given task using intractable brute force and heuristics. By restricting attention to algebraic stack combinations, we provide a linear-time algorithm for generating all the appropriate monad stacks, or decide no such stacks exist. Our approach is based on Hyland, Plotkin, and Power’s algebraic analysis of monad transformers, who propose a graph-theoretical solution to this problem. We extend their analysis with a straightforward connection to the modular decomposition of a graph and to cographs, a.k.a. series-parallel graphs. We present an accessible and self-contained account of this monad-stack generation problem, and, more generally, of the decomposition of a combined algebraic theory into sums and tensors, and its algorithmic solution. We provide a web-tool implementing this algorithm intended for semantic investigations of effect combinations and for monad stack generation.
Haskell incorporates computational effects modularly using sequences of monad transformers, termed monad stacks. The current practice is to find the appropriate stack for a given task using intractable brute force and heuristics. By restricting attention to algebraic stack combinations, we provide a linear-time algorithm for generating all the appropriate monad stacks, or decide no such stacks exist. Our approach is based on Hyland, Plotkin, and Power’s algebraic analysis of monad transformers, who propose a graph-theoretical solution to this problem. We extend their analysis with a straightforward connection to the modular decomposition of a graph and to cographs, a.k.a. series-parallel graphs. We present an accessible and self-contained account of this monad-stack generation problem, and, more generally, of the decomposition of a combined algebraic theory into sums and tensors, and its algorithmic solution. We provide a web-tool implementing this algorithm intended for semantic investigations of effect combinations and for monad stack generation.
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.
Talk given at the 1st join category theory and computer science seminar, University of Cambridge, 18 November, 2012.
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).
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.
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).