Ahrens, Benedikt ;
Hirschowitz, André ;
Lafont, Ambroise ;
Maggesi, Marco
Modular Specification of Monads Through HigherOrder Presentations
Abstract
In their work on secondorder 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 ("higherorder") operations and equations among them. We consider a notion of 2signature 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 etaequalities. Such a 2signature is hence a pair (Sigma,E) of a binding signature Sigma and a family E of equations for Sigma. This notion of 2signature has been introduced earlier by Ahrens in a slightly different context.
We associate, to each 2signature (Sigma,E), a category of "models of (Sigma,E)"; and we say that a 2signature is "effective" if this category has an initial object; the monad underlying this (essentially unique) object is the "monad specified by the 2signature". Not every 2signature is effective; we identify a class of 2signatures, which we call "algebraic", that are effective.
Importantly, our 2signatures together with their models enjoy "modularity": when we glue (algebraic) 2signatures 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 HigherOrder Presentations}},
booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
pages = {6:16:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771078},
ISSN = {18688969},
year = {2019},
volume = {131},
editor = {Herman Geuvers},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/10513},
URN = {urn:nbn:de:0030drops105136},
doi = {10.4230/LIPIcs.FSCD.2019.6},
annote = {Keywords: free monads, presentation of monads, initial semantics, signatures, syntax, monadic substitution, computerchecked proofs}
}
2019
Keywords: 

free monads, presentation of monads, initial semantics, signatures, syntax, monadic substitution, computerchecked proofs 
Seminar: 

4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Issue date: 

2019 
Date of publication: 

2019 