Runtime monoidal category
The runtime monoidal category over an effectful polygraph is a monoidal category with an extra object (the “runtime”) that gets passed as input and output to every effectful morphism. This is the main ingredient in the construction of the free effectful category over a polygraph, as detailed in Promonads and String Diagrams for Effectful Categories (Roman, 2022) and in the prior Premonoidal Categories and a Graphical View of Programs (Jeffrey, 1998).
- Substituting without runtime: a motivation for this particular graphical calculus.