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.
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.
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).
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.
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.
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.
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.
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.
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.
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.
# Preprints
- Coinductive Streams in Monoidal Categories, joint with Elena Di Lavore and Giovanni de Felice.
- Comb Diagrams for Discrete-Time Feedback.
# Selected Talks
- From theories to categories at the Lawvere Memorial Meeting, Tallinn.
- String diagrams of string diagrams at TallCat group meetings, Tallinn.
- Evidential Decision Theory via Partial Markov Categories at NWPT'22, Bergen.
- Notes on A Graphical View at TallCat Seminar, Tallinn.
- Promonads and String Diagrams for Effectful Categories at ACT'22, Strathclyde
- Notes on Compositional Markov Processes at the ACT'22 Adjoint School, Strathclyde.
- Monoidal Profunctors at Compositional Methods Retreat, Raudsilla.
- A Canonical Algebra of Transition Systems at ACT'21, Cambridge.
- A Canonical Algebra of Transition Systems at FACS'21, Grenoble.
- Picturing Multivariable Adjunctions at TallCat Seminar, Tallinn.
- Lesson on Monoidal Categories at the Category Theory course, Tallinn.
- Open Diagrams via Coend Calculus at ACT'20, MIT.
- Profunctor Optics: a Categorical Update at ACT'20, MIT.
- Profunctor Optics: a Categorical Update at NWPT'19, Tallinn.
- Profunctor Optics: a Categorical Update at SYCO 5, Birmingham.
- Profunctor Optics: a Categorical Update at MFoCS Dissertation, Oxford.
See also: News, Note Index.