List Objects with Algebraic Structure

Marcelo Fiore, Philip Saville

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We introduce and study the notion of list object with algebraic structure. The first key aspect of our development is that the notion of list object is considered in the context of monoidal structure; the second key aspect is that we further equip list objects with algebraic structure in this setting. Within our framework, we observe that list objects give rise to free monoids and moreover show that this remains so in the presence of algebraic structure. In addition, we provide a basic theory explicitly describing as an inductively defined object such free monoids with suitably compatible algebraic structure in common practical situations. This theory is accompanied by the study of two technical themes that, besides being of interest in their own right, are important for establishing applications. These themes are: parametrised initiality, central to the universal property defining list objects; and approaches to algebraic structure, in particular in the context of monoidal theories. The latter leads naturally to a notion of nsr (or near semiring) category of independent interest. With the theoretical development in place, we touch upon a variety of applications, considering Natural Numbers Objects in domain theory, giving a universal property for the monadic list transformer, providing free instances of algebraic extensions of the Haskell Monad type class, elucidating the algebraic character of the construction of opetopes in higher-dimensional algebra, and considering free models of second-order algebraic theories.
Original languageUndefined/Unknown
Title of host publication2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
EditorsDale Miller
Place of PublicationDagstuhl, Germany
PublisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
Pages16:1-16:18
Number of pages18
Volume84
ISBN (Print)978-3-95977-047-7
DOIs
Publication statusPublished - 1 Sep 2017
EventSecond International Conference on Formal Structures for Computation and Deduction - Oxford, United Kingdom
Duration: 3 Sep 20179 Sep 2017
https://www.cs.ox.ac.uk/conferences/fscd2017/

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Volume84
ISSN (Electronic)1868-8969

Conference

ConferenceSecond International Conference on Formal Structures for Computation and Deduction
Abbreviated titleFSCD 2017
Country/TerritoryUnited Kingdom
CityOxford
Period3/09/179/09/17
Internet address

Keywords

  • list object
  • free monoid
  • strong monad
  • algebraic theory
  • near semiring
  • Haskell Monad type class
  • opetope

Cite this