Distributive Multicategories (project proposal)
The following is a proposal for an undergraduate student.
Lawvere theories — or, cartesian multicategories — are central notions in universal algebra. However, computer programs are seldom cartesian. Instead, what is cartesian (strictly speaking, cocartesian) is their control flow. The mixture of cocartesian control flow and monoidal dataflow gives rise to distributive multicategories.
Distributive multicategories could be used to give categorical semantics to multiple variants of imperative programming languages with effects. They provide a more careful treatment of coproducts, where the syntax is mostly derived instead of consisting of primitives. Surprisingly, they seem to be understudied: I could not find many instances of their explicit use in imperative programming languages (the only clear one being my own recent work with Filippo Bonchi, Elena Di Lavore, and Sam Staton). At the same time, they are interesting from the viewpoint of formal category theory.
Research proposal. To develop the theory of distributive multicategories and traced distributive multicategories. To provide good syntaxes for distributive multicategories; to relate these both to algebraic effects and handlers, and to the theory of essentially algebraic theories.
References.