ABSTRACT. Algebraic effects let programmers declare the syntax of operations which can be used to write and compose effectful programs. Such programs can be run by applying effect handlers that give programmers control over when and how many times to call continuations of operations. Embedding algebraic effects and handlers in an existing language provides a lightweight and powerful approach to programming with effects. Such embeddings typically use host language functions to represent continuations of programs. While host language functions offer an ergonomic interface for programming with and handling effects, they also hinder programmers wishing to define custom optimizations for effectful programs. Specifically, optimizations that statically analyze and transform variable bindings cannot be defined, as that would require meta-programming facilities for host language functions. This paper presents a solution to this problem by embedding algebraic effects as intrinsically typed, De Bruijn-indexed syntax. Working in Agda, we demonstrate how this provides a safe-by-construction approach to programming with effects that is almost as ergonomic as the traditional embedding, but which additionally supports optimizations that inspect and transform variable binding.

ABSTRACT. This work studies semiarrows: profunctors that carry both a monoid structure under the Day convolution (parallel composition with unit) and a semigroup structure under profunctor composition (sequential composition without identity), linked by an interchange law and a unit interaction law. The term and definition were introduced in the author's doctoral thesis, generalising monoidal profunctors and arrows. We construct the free semiarrow over an arbitrary base profunctor~$p$, presented as a GADT |FreeSemi p| with five constructors corresponding to the semiarrow operations. We give the interpretation function |interpretSync|, which, given a natural transformation from~$p$ to any target semiarrow~$q$, produces the unique semiarrow homomorphism extending the natural transformation. As a running example we develop an arithmetic-circuit DSL over a prime field. Primitive gates form a GADT; |FreeSemi RelGate| is the resulting circuit term algebra for constraint checking. Because no |arr| combinator is available, every fan-out and structural routing must appear explicitly, making every circuit term inspectable. We present an interpretation of the R1CS cost model via |interpretSync|.

ABSTRACT. Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories. We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with Π-, Σ-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger, and we recognize this structure in many intensional models of Martin-Löf type theory. This talk is based on a recently published paper and its ongoing continuation.

ABSTRACT. We propose abstractions for exploiting symmetries in programming and reasoning based on the mathematical proof principle "without-loss-of-generality" (wlog). We decompose such arguments into three components. The first component makes the symmetry explicit by defining appropriate groups and their action on the input/assumptions and output/conclusions. The second component explicates how to canonise the input, by choosing appropriate symmetries for each input. The third component is a core function/proof that transforms canonical inputs into outputs. The proposed wlog construct combines these components: given an input, calculate its canonising symmetry, use the symmetry to canonise the input, apply the core function to the canonical input, and apply the inverse symmetry to the output. Here we develop the mathematical foundations for these abstractions. We illustrate the approach on running examples: sliding-tile merges in 2048, binary-tree insertion, and Schur's inequality as a mathematical instance of WLOG. We extend the framework to algebraic datatypes using initial algebra semantics, showing how a G-symmetry strength on a functor lifts group actions to inductive types and that the unique fold into an equivariant algebra is itself equivariant, allowing us to avoid using general recursion to define a symmetric version of tree insertion. Finally, we develop the theory of equivariant canonisers and explore the cases when the WLOG construction is guaranteed to produce an equivariant function.

ABSTRACT. I will present a recent result giving a very simple characterization of the Giry monad on (standard Borel) measurable spaces in terms of a (initial) universal property. In addition, I'll present some ongoing work on adapting this result to categories more suited for functional programming, such as elementary toposes.

ABSTRACT. Equality saturation is a powerful technique for program optimisation and reasoning, driven by the use of equivalence classes of terms under rewrite rules. These equivalence classes lie at the root of data structures called equality graphs (e-graphs). Despite their numerous advantages, until recently e-graphs lacked native support for variable binding, limiting their applicability to programming languages. We propose to address this problem from a categorical perspective by extending the interpretation of e-graphs as string diagrams, namely morphisms in symmetric monoidal semilattice-enriched categories which we additionally equip with a monoidal closed structure. We further define a concrete representation using hierarchical hypergraphs, and introduce a corresponding double-pushout (DPO) rewriting system. Finally, we establish the equivalence between term rewriting and DPO rewriting, with the combinatorial model inherently absorbing the equations of the symmetric monoidal structure. Our approach, specifically designed for lambda calculi, is compared and contrasted with slotted e-graphs --- an alternative method for incorporating variable binding within e-graphs.

ABSTRACT. Cons-lists are fundamental to functional programming, and are well-understood as initial algebras, and as a concrete construction of free monoids. In category theory, such list objects can be axiomatised internal to any monoidal category, with nil and cons maps, and a recursion mechanism. When strengthened to support parametrised recursion, they can be shown to give the free monoid construction. We study a small variant on parametrised list objects called parametrised symmetric list objects, in a symmetric monoidal category, where the two frontmost elements are allowed to be permuted. We show that this gives a construction of free commutative monoids, and develop some related theory.

ABSTRACT. We discuss the concurrent monads of Rivas and Jaskelioff, a structure axiomatizing effectful notions of computation supporting not only sequential, but also parallel composition. We have previously analyzed accessible concurrent monads on given monoidal ordered category as lax duoid objects in a certain duoidal ordered category. Here we explain the different perspective that concurrent are monads in a certain 2-category and what this entails.