Index

I am currently a PhD student at Tallinn University of Technology under the supervision of Paweł Sobociński; my main interests are category theory and functional programming. I have studied lenses in functional programming and developed a theory of incomplete string diagrams that allows us to reason with many constructions in applied category theory in a formal and purely diagrammatic way.

# Publications

The Produoidal Algebra of Process Decomposition ( pdf) In peer-review (2023).
Joint with Matt Earnshaw and James Hefford

Abstract. We introduce the normal produoidal category of monoidal contexts over an arbitrary monoidal category. In the same sense that a monoidal morphism represents a process, a monoidal context represents an incomplete process: a piece of a decomposition, possibly containing missing parts. We characterize monoidal contexts in terms of universal properties. In particular, symmetric monoidal contexts coincide with monoidal lenses, endowing them with a novel universal property. We apply this algebraic structure to the analysis of multi-party interaction protocols in arbitrary theories of processes.

Slides: Ottawa Logic Seminar.

monoidal-contexts-sample

Evidential Decision Theory via Partial Markov Categories (pdf)
In peer-review (2023).
Joint with Elena Di Lavore

Abstract. We introduce partial Markov categories. In the same way that Markov categories encode stochastic processes, partial Markov categories encode stochastic processes with constraints, observations and updates. In particular, we prove a synthetic Bayes theorem; we use it to define a syntactic partial theory of observations on any Markov category, whose normalisations can be computed in the original Markov category. Finally, we formalise Evidential Decision Theory in terms of partial Markov categories, and provide implemented examples.

Slides: NWPT 22. calculemus-wishlist

Monoidal Streams for Dataflow Programming (pdf, cite)
IEEE Symposium on Logic in Computer Science (LiCS, 2022), Kleene Award.
Joint with Elena Di Lavore and Giovanni de Felice.

Abstract. We introduce monoidal streams: a generalization of causal stream functions to monoidal categories. In the same way that streams provide semantics to dataflow programming with pure functions, monoidal streams provide semantics to dataflow programming with theories of processes represented by a symmetric monoidal category. At the same time, monoidal streams form a feedback monoidal category, which can be used to interpret signal flow graphs. As an example, we study a stochastic dataflow language.

Slides: LiCS'22, Intercats Seminar (Topos Institute), TallCat Seminar, NWPT'21 (Reykjavik).

parallel-composition-of-monoidal-streams

Span(Graph): a Canonical Feedback Algebra of Open Transition Systems (pdf)
Software and Systems Modeling (SOSYM, 2022).
Joint with Elena Di Lavore, Alessandro Gianola, Nicoletta Sabadini and Paweł Sobociński.

Abstract. We show that Span(Graph), an algebra for open transition systems introduced by Katis, Sabadini and Walters, satisfies a universal property. By itself, this is a justification of the canonicity of this model of concurrency. However, the universal property is itself of interest, being a formal demonstration of the relationship between feedback and state. Indeed, feedback categories, also originally proposed by Katis, Sabadini and Walters, are a weakening of traced monoidal categories, with various applications in computer science. A state bootstrapping technique, which has appeared in several different contexts, yields free such categories. We show that Span(Graph) arises in this way, being the free feedback category over Span(Set). Given that the latter can be seen as an algebra of predicates, the algebra of open transition systems thus arises - roughly speaking - as the result of bootstrapping state to that algebra. Finally, we generalize feedback categories endowing state spaces with extra structure: this extends the framework from mere transition systems to automata with initial and final states.

span-graph-gears

Promonads and String Diagrams for Effectful Categories (pdf, cite)
Applied Category Theory (ACT, 2022).

Abstract. Premonoidal and Freyd categories are both generalized by non-cartesian Freyd categories: effectful categories. We construct string diagrams for effectful categories in terms of the string diagrams for a monoidal category with a freely added object. We show that effectful categories are pseudomonoids in a monoidal bicategory of promonads with a suitable tensor product.

premonoidal-program

A Canonical Algebra of Open Transition Systems (pdf, cite)
Formal Aspects of Component Software (FACS, 2021)
Joint with Elena Di Lavore, Alessandro Gianola, Nicoletta Sabadini and Paweł Sobociński.

Abstract. Feedback and state are closely interrelated concepts. Categories with feedback, originally proposed by Katis, Sabadini and Walters, are a weakening of the notion of traced monoidal categories, with several pertinent applications in computer science. The construction of the free such categories has appeared in several different contexts, and can be considered as state bootstrapping. We show that a categorical algebra for open transition systems, Span(Graph)∗, also due to Katis, Sabadini and Walters, is the free category with feedback over Span(Set). Intuitively, this algebra of transition systems is obtained by adding state to an algebra of predicates, and therefore Span(Graph)∗ is, in this sense, the canonical such algebra.

feedback-drawings

Cornering Optics (pdf, cite)
Applied Category Theory (ACT, 2022)
Joint with Chad Nester and Guillaume Boisseau.

Abstract. We show that the category of optics in a monoidal category arises naturally from the free cornering of that category. Further, we show that the free cornering of a monoidal category is a natural setting in which to work with comb diagrams over that category. The free cornering admits an intuitive graphical calculus, which in light of our work may be used to reason about optics and comb diagrams.

free-cornering-encodes-combs

Open Diagrams via Coend Calculus (pdf, cite)
Applied Category Theory (ACT, 2021)

Abstract. Morphisms in a monoidal category are usually interpreted as processes, and graphically depicted as square boxes. In practice, we are faced with the problem of interpreting what non-square boxes ought to represent in terms of the monoidal category and, more importantly, how should they be composed. Examples of this situation include lenses or learners. We propose a description of these non-square boxes, which we call open diagrams, using the monoidal bicategory of profunctors. A graphical coend calculus can then be used to reason about open diagrams and their compositions.

graphical-coend-calculus-example

Profunctor Optics: a Categorical Update ( pdf )
In peer-review (2022).
Joint with Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregian,
Bartosz Milewski and Emily Pillmore.

Abstract. Optics are bidirectional data accessors that capture data transformation patterns such as accessing subfields or iterating over containers. Profunctor optics are a particular choice of representation supporting modularity, meaning that we can construct accessors for complex structures by combining simpler ones. Profunctor optics have previously been studied only in an unenriched and non-mixed setting, in which both directions of access are modelled in the same category. However, functional programming languages are arguably better described by enriched categories; and we have found that some structures in the literature are actually mixed optics, with access directions modelled in different categories. Our work generalizes a classic result by Pastro and Street on Tambara theory and uses it to describe mixed V-enriched profunctor optics and to endow them with V-category structure. We provide some original families of optics and derivations, including an elementary one for traversals. Finally, we discuss a Haskell implementation.

lens-drawings

Mikrokosmos: an Educational Lambda Interpreter ( pdf )
Journal of Open Source Education (JOSE, 2018)
Under the supervision of Pedro García-Sánchez.

Abstract. Mikrokosmos is an educational untyped and simply typed lambda-calculus interpreter. For students, it is a tool to learn lambda-calculus and intuitionistic logic by coding. For educators, it is a didactic resource, grounded in the theoretical implementation of a functional programming language, so that they can integrate it with other learning materials.

mikrokosmos-derivation