United Monoids: Finding Simplicial Sets and Labelled Algebraic Graphs in TreesVol. 6
Graphs and various graph-like combinatorial structures, such as preorders and hypergraphs, are ubiquitous in programming. This paper focuses on representing graphs in a purely functional programming language like Haskell. There are several existing approaches; one of the most recently developed ones is the “algebraic graphs” approach (2017). It uses an algebraic data type to represent graphs and has attracted users, including from industry, due to its emphasis on equational reasoning and making a common class of bugs impossible by eliminating internal invariants.
The previous formulation of algebraic graphs did not support edge labels, which was a serious practical limitation. In this paper, we redesign the main algebraic data type and remove this limitation. We follow a fairly standard approach of parameterising a data structure with a semiring of edge labels. The new formulation is both more general and simpler: the two operations for composing graphs used in the previous work can now be obtained from a single operation by fixing the semiring parameter to zero and one, respectively.
By instantiating the new data type with different semirings, and working out laws for interpreting the resulting expression trees, we discover an unusual algebraic structure, which we call “united monoids”, that is, a pair of monoids whose unit elements coincide. We believe that it is worth studying united monoids in their full generality, going beyond the graphs which prompted their discovery. To that end, we characterise united monoids with a minimal set of axioms, prove a few basic theorems, and discuss several notable examples.
We validate the presented approach by implementing it in the open-source algebraic-graphs library. Our theoretical contributions are supported by proofs that are included in the paper and have also been machine-checked in Agda. By extending algebraic graphs with support for edge labels, we make them suitable for a much larger class of possible applications. By studying united monoids, we provide a theoretical foundation for further research in this area.
I am a software engineer at Jane Street London, and a visiting fellow at Newcastle University, UK. My research interests are in applying abstract mathematics and functional programming to solving large-scale engineering problems.
During my PhD study (2005-2009) I worked on asynchronous circuits and concurrency, and developed Conditional Partial Order Graphs to model the behaviour of concurrent systems by decomposing them into simple, well-understood parts. In 2014 I became interested in functional programming and translated some of my earlier research to the world of functional programming, publishing open-source libraries for algebraic graphs and selective functors. I have also done some work on the topic of software build systems – this topic has been gradually changing from “terrifying” to “fascinating” to me, and I’m yet to see where this journey goes. In 2019 I switched from academia to industry and joined Jane Street to work on the most popular OCaml build system Dune.
I am originally from Kyrgyzstan, where I received a Software Engineering degree (2000-2005) from Kyrgyz-Russian Slavic University. I was a 5-time champion of Kyrgyzstan in algorithmic competitions and currently help to run the ACM ICPC Regional Contest in Kyrgyzstan.
Thu 24 MarDisplayed time zone: Lisbon change
10:30 - 12:00 | |||
10:30 30mResearch paper | The Art of the Meta Stream Protocol: Torrents of StreamsVol. 6 Research Papers Christophe De Troyer Vrije Universiteit Brussel, Jens Nicolay Vrije Universiteit Brussel, Wolfgang De Meuter Vrije Universiteit Brussel Link to publication | ||
11:00 30mResearch paper | Topology-level Reactivity in Distributed Reactive Programs: Reactive Acquaintance Management using Proximity SetsVol. 6 Research Papers Sam Van den Vonder Vrije Universiteit Brussel, Thierry Renaux Vrije Universiteit Brussel, Wolfgang De Meuter Vrije Universiteit Brussel Link to publication DOI | ||
11:30 30mResearch paper | United Monoids: Finding Simplicial Sets and Labelled Algebraic Graphs in TreesVol. 6 Research Papers Andrey Mokhov Jane Street Link to publication |