Reflecting Algebraically Compact Functors

Abstract

A compact T-algebra is an initial T-algebra whose inverse is a final T-coalgebra. Functors with this property are said to be algebraically compact. This is a very strong property used in programming semantics which allows one to interpret recursive datatypes involving mixed-variance functors, such as function space. The construction of compact algebras is usually done in categories with a zero object where some form of a limit-colimit coincidence exists. In this paper we consider a more abstract approach and show how one can construct compact algebras in categories which have neither a zero object, nor a (standard) limit-colimit coincidence by reflecting the compact algebras from categories which have both. In doing so, we provide a constructive description of a large class of algebraically compact functors (satisfying a compositionality principle) and show our methods compare quite favorably to other approaches from the literature.

arXiv commentIn Proceedings ACT 2019, arXiv:2009.06334

References in corpus (4)

• A Categorical Model for a Quantum Circuit Description Language (Extended Abstract)
• Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
• Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory
• Semantics for first-order affine inductive data types via slice categories