When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2019.6
URN: urn:nbn:de:0030-drops-105136
URL: https://drops.dagstuhl.de/opus/volltexte/2019/10513/
 Go to the corresponding LIPIcs Volume Portal

Modular Specification of Monads Through Higher-Order Presentations

 pdf-format:

Abstract

In their work on second-order equational logic, Fiore and Hur have studied presentations of simply typed languages by generating binding constructions and equations among them. To each pair consisting of a binding signature and a set of equations, they associate a category of "models", and they give a monadicity result which implies that this category has an initial object, which is the language presented by the pair.
In the present work, we propose, for the untyped setting, a variant of their approach where monads and modules over them are the central notions. More precisely, we study, for monads over sets, presentations by generating ("higher-order") operations and equations among them. We consider a notion of 2-signature which allows to specify a monad with a family of binding operations subject to a family of equations, as is the case for the paradigmatic example of the lambda calculus, specified by its two standard constructions (application and abstraction) subject to beta- and eta-equalities. Such a 2-signature is hence a pair (Sigma,E) of a binding signature Sigma and a family E of equations for Sigma. This notion of 2-signature has been introduced earlier by Ahrens in a slightly different context.
We associate, to each 2-signature (Sigma,E), a category of "models of (Sigma,E)"; and we say that a 2-signature is "effective" if this category has an initial object; the monad underlying this (essentially unique) object is the "monad specified by the 2-signature". Not every 2-signature is effective; we identify a class of 2-signatures, which we call "algebraic", that are effective.
Importantly, our 2-signatures together with their models enjoy "modularity": when we glue (algebraic) 2-signatures together, their initial models are glued accordingly.
We provide a computer formalization for our main results.

BibTeX - Entry

```@InProceedings{ahrens_et_al:LIPIcs:2019:10513,
author =	{Benedikt Ahrens and Andr{\'e} Hirschowitz and Ambroise Lafont and Marco Maggesi},
title =	{{Modular Specification of Monads Through Higher-Order Presentations}},
booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
pages =	{6:1--6:19},
series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN =	{978-3-95977-107-8},
ISSN =	{1868-8969},
year =	{2019},
volume =	{131},
editor =	{Herman Geuvers},
publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},