SPLS online — 20th October 2021 (10:00–17:00)

We tend to speak of the (possibly empty) list monad and the nonempty list monad, meaning the free monoid monad and the free semigroup monad, as if those were the only monad structures on the list and nonempty list endofunctors (on Set). But they are not! It may at first seem hard to construct other list and nonempty list monads, but at a closer look it turns out that examples abound. There are infinitely many list monads with the singleton function as the unit that admit a presentation with one nullary and one binary operation, and infinitely many nonempty list monads with singleton as the unit and a presentation with one binary operation; some multiplications not only delete, but even duplicate and permute elements. There are list and nonempty list monads with singleton as the unit that have no finite presentation. There are nonempty list monads whose unit is the doubleton function. You cannot tell if a nonempty list monad presented to you as a blackbox is the free semigroup monad by testing the unit and multiplication on finitely many inputs. Etc. We are far from having classified all list monads or all nonempty list monads, but these are cool combinatorial problems.

This is joint work with Dylan McDermott and Maciej Piróg.

In this talk I will discuss the design and status of the "typed continuations" proposal for Wasm.

Non-local control flow features provide the ability to suspend the current execution context and later resume it. Many industrial-strength programming languages feature a wealth of non-local control flow features such as async/await, coroutines, generators/iterators, effect handlers, call/cc, and so forth. For some programming languages non-local control flow is central to their identity, meaning that they rely on non-local control flow for efficiency, e.g. to support massively scalable concurrency.

Currently, Wasm lacks support for implementing such features directly and efficiently without a circuitous global transformation of source programs on the producer side. One possible strategy is to add special support for each individual non-local control flow feature to Wasm, but strategy does not scale to the next 700 non-local control flow features. Instead, the goal of this proposal is to introduce a unified structured mechanism based Plotkin and Pretnar's effect handlers which is sufficiently general to cover present use-cases as well as being forwards compatible with future use-cases, whilst admitting efficient implementations.

Proposal repository https://github.com/effect-handlers/wasm-spec .

Refactoring is the process of changing the structure of a program without changing its behaviour, and is a common practice aimed at making a program more understandable, accessible, or amenable to further alterations to a program's design. Refactorings can be applied manually, which is both a tedious and error-prone process, or via automated refactoring tools, which can both simplify the workflow and guard against common human mistakes, such as overlooking one file within hundreds. Unfortunately, automated tools have their own mode of failure: i.e. changing the behaviour of the code silently in unexpected ways. As refactoring tools grow in power and are applied to ever larger codebases, the key correctness criteria that they indeed do not change program behaviour becomes crucial.

Most available refactoring tools do not come with any correctness promises. With common refactoring tools such as Eclipse for Java having well-reported bugs. Indeed, any correctness guarantees of such tools is usually in writing: either by test cases or by hand-written or mechanised correctness proofs.

In this talk I will demonstrate a different approach: producing a proof of correctness together with the refactoring, where I use Idris to provide a verified refactoring tool for a subset of Haskell 98. Dependent types provides an implementation of a formally verified semantics of the refactorings and give soundness proofs as part of the refactoring implementations themselves.

I will present PART, a Proof Carrying Refactoring Tool for Haskell 98 programs implemented in Idris. I will also give a verified static semantics for a subset of Haskell 98, and a renaming refactoring over that subset. I will conclude with a soundness proof of our renaming implementation.

(joint work with Guillaume Allais, Edwin Brady, Nathan Corbyn, and Jeremy Yallop)

I'll present an extensible, mathematically-structured algebraic simplification library design. We structure the library using universal algebraic concepts: a free algebra; and a free extension --- frex --- of an algebra by a set of variables. The latter concept, the frex, generalises the `ring of polynomials over a ring' to that of `an algebra of polynomials over an algebra`.

The library's dependently-typed API guarantees that the simplification modules in the library, even user-defined ones, are terminating, sound, and complete with respect to a well-specified class of equations. Our design is modular in two axes. First, simplification modules share thousands of lines of infrastructure code dealing with term-representation, pretty-printing, certification, and macros/reflection. Second, more advanced simplification modules can reuse existing simplification modules. We demonstrate this design by developing three monoid simplification modules: ordinary, commutative, and involutive monoids. We implemented this design in the new Idris2 dependently-typed programming language, and in Agda. I will demonstrate the Idris2 implementation.

I will present some work in progress towards programming with overconnected data structures. Graphs, for example, can be represented as decorated trees: their spanning tree together with some additional edges. The structures of our current interest are planar graphs, where no edges cross. For implementing operations like navigating to a different place within a graph, we use some well known techniques on the underlying tree, while ensuring that the decoration stays in place. More interesting questions include the choice of spanning tree, re-rooting a tree and views from different positions.

This is joint work with Conor McBride.

This paper defines the ΔQ𝑆𝐷 language that embodies the main concepts of the ΔQ framework for distributed systems design. The ΔQ framework has been developed over three decades to design large distributed systems with predictable behaviour under high applied load. The framework specifies system designs at different levels of refinement and tracks and predicts their performance envelope as a function of load. System designers can thereby determine whether the system is likely to perform satisfactorily before the system is actually built. This is a critical property for real-world systems: they are expected to perform well in exactly those cases when it is difficult to ensure adequate performance, such as telephony systems during natural catastrophes.

The ΔQ𝑆𝐷 language defines a system as a formal structure (called an “outcome diagram”) that makes explicit how all system behaviours relate to each other. The system’s design is then a sequence of refinement steps starting from a system with wholly unspecified structure and ending with a system with completely specified structure. We give the language semantics that allows computation of the predicted system performance at any step in the refinement process. In future work we intend to incorporate ΔQ𝑆𝐷 in software tools and to use it to provide formal proofs that a partially specified design’s performance is adequate or inadequate. This will make it a practical and useful tool for system designers.

In the last 5 years the pressing need to ensure the safety of AI systems has led to the development of a plethora of different tools targeting the problem of how to constrain the relationship between a neural network's inputs and outputs. This includes: training it to obey the relationship, verifying the relationship holds or finding counterexamples, and verifying larger systems that make use of the network. In this talk I will describe how our proposed DSL Vehicle, aims to bridge the gaps between all these different tools and provide a single high-level human readable interface for embedding and monitoring the properties of a network all the way through its lifecycle.

Parametrised optics form the backbone of categorical cybernetics [1], an area of study focused on interactive, controlled systems. The central mathematical innovation is acknowledging the Para construction as the way to talk about controlled-controller relations in cybernetic systems while retaining a straightforward graphical calculus and mathematical theory. Applications of this framework include open games (compositional game theory [1, 2]) and open learners (compositional machine learning [1, 3]).

In this presentation we show how common client-server relationships (such as CRUD/RESTful APIs) can be treated in the same fashion. We propose parametrised lenses as an expressive primitive for a server library, allowing programmer to write and extend clients and servers without the hassle associated with it. The talk will feature both a categorical and theoretic analysis and a walkthrough of an Idris implementation of a RESTful server library.

This presentation is a follow up from the existing talk “Optics for servers” [4]

References:
[1] Capucci, Gavranovic, Hedges, Rischel, Towards foundations of categorical cybernetics , 2021
[2] Capucci, Ghani, Ledent, Forsber, Translating Extensive Form Games to Open Games with Agency , 2021
[3] Cruttwell, Gavranovic, Ghani, Wilson, Zanasi, Categorical Foundations of Gradient-Based Learning , 2021
[4] Optics for servers: https://www.youtube.com/watch?v=4xpbYPa1lTc