Inspired by algebraic effects and the principle of notions of computations as monoids, we study a categorical framework for equational theories and models of monoids equipped with operations.
The framework covers not only algebraic operations but also scoped and variable-binding operations.
Appealingly, in this framework both theories and models can be modularly composed.
Technically, a general monoid-theory correspondence is shown, saying that the category of theories of algebraic operations is equivalent to the category of monoids.
Moreover, more complex forms of operations can be coreflected into algebraic operations, in a way that preserves initial algebras.
On models, we introduce modular models of a theory, which can interpret
abstract syntax in the presence of other operations.
We show constructions of modular models (i) from monoid transformers, (ii) from free algebras, (iii) by composition, and (iv) in symmetric monoidal categories.
Tue 5 SepDisplayed time zone: Pacific Time (US & Canada) change
10:30 - 12:00 | EffectsICFP Papers and Events at A - Grand Ballroom 2 Chair(s): Ningning Xie University of Toronto / Google DeepMind | ||
10:30 30mTalk | A General Fine-Grained Reduction Theory for Effect Handlers ICFP Papers and Events Filip Sieczkowski Heriot-Watt University, Mateusz Pyzik University of Wrocław, Dariusz Biernacki University of Wrocław DOI | ||
11:00 30mTalk | Modular Models of Monoids with Operations ICFP Papers and Events DOI | ||
11:30 30mTalk | With or Without You: Programming with Effect Exclusion ICFP Papers and Events Matthew Lutze Aarhus University, Magnus Madsen Aarhus University, Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen DOI | ||