[ICFP'23] Modular Models of Monoids with Operations
Modular Models of Monoids with Operations (Video, ICFP 2023)
Zhixuan Yang and Nicolas Wu
(Imperial College London, UK; Imperial College London, UK)
Abstract: 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.
Article: https://doi.org/10.1145/3607850
ORCID: https://orcid.org/0000-0001-5573-3357, https://orcid.org/0000-0002-4161-985X
Video Tags: equational systems, Σ-monoids, effects, modularity, monad transformers, icfp23main-p69-p, doi:10.1145/3607850, orcid:0000-0001-5573-3357, orcid:0000-0002-4161-985X
Presentation at the ICFP 2023 conference, September 4–9, 2023, https://icfp23.sigplan.org/
Sponsored by ACM SIGPLAN, https://www.sigplan.org/