Reference. A Combinatorial Approach to Higher-Order Structure for Polynomial Functors
Polynomial functors are categorical structures used in a variety of applications across theoretical computer science; for instance, in database theory, denotational semantics, functional programming, and type theory. A well-known problem is that the bicategory of finitary polynomial functors between categories of indexed sets is not cartesian closed, despite its success and influence on denotational models and linear logic. This paper introduces a formal bridge between the model of finitary polynomial functors and the combinatorial theory of generalised species of structures. Our approach consists in viewing finitary polynomial functors as free analytic functors, which correspond to free generalised species. In order to systematically consider finitary polynomial functors from this combinatorial perspective, we study a model of groupoids with additional logical structure; this is used to constrain the generalised species between them. The result is a new cartesian closed bicategory that embeds finitary polynomial functors.
Cite
Cited by (1)
Stabilized profunctors and stable species of structures fiore-2024-stabilized
We introduce a bicategorical model of linear logic which is a novel variation of the bicategory of groupoids, profunctors, and natural transformations. Our model is obtained by endowing groupoids with additional structure, called a kit, to stabilize the profunctors by controlling the freeness of the groupoid action on profunctor elements. The theory of generalized species of structures, based on profunctors, is refined to a new theory of stable species of structures between groupoids with Boolean kits. Generalized species are in correspondence with analytic functors between presheaf categories; in our refined model, stable species are shown to be in correspondence with restrictions of analytic functors, which we characterize as being stable, to full subcategories of stabilized presheaves. Our motivating example is the class of finitary polynomial functors between categories of indexed sets, also known as normal functors, that arises from kits enforcing free actions. We show that the bicategory of groupoids with Boolean kits, stable species, and natural transformations is cartesian closed. This makes essential use of the logical structure of Boolean kits and explains the well-known failure of cartesian closure for the bicategory of finitary polynomial functors between categories of set-indexed families and cartesian natural transformations. The paper additionally develops the model of classical linear logic underlying the cartesian closed structure and clarifies the connection to stable domain theory.
Cites 50 works (4 here)
With notes (4)
Indexed containers altenkirch_indexed_2015
We show that the syntactically rich notion of strictly positive families can be reduced to a core type theory with a fixed number of type constructors exploiting the novel notion of indexed containers. As a result, we show indexed containers provide normal forms for strictly positive families in much the same way that containers provide normal forms for strictly positive types. Interestingly, this step from containers to indexed containers is achieved without having to extend the core type theory. Most of the construction presented here has been formalized using the Agda system.
Wellfounded Trees and Dependent Polynomial Functors gambino_wellfounded_2004
We set out to study the consequences of the assumption of types of wellfounded trees in dependent type theories. We do so by investigating the categorical notion of wellfounded tree introduced in [16]. Our main result shows that wellfounded trees allow us to define initial algebras for a wide class of endofunctors on locally cartesian closed categories.
Glueing and orthogonality for models of linear logic hyland_glueing_2003
We present the general theory of the method of glueing and associated technique of orthogonality for constructing categorical models of all the structure of linear logic: in particular we treat the exponentials in detail. We indicate simple applications of the methods and show that they cover familiar examples.
Linear logic girard_linear_1987
The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.
External (46)
- ∞-Operads as Analytic Monads (2021)
- A Cartesian Bicategory of Polynomial Functors in Homotopy Type Theory (2021)
- A Bicategorical Model for Finite Nondeterminism (2021)
- Intersection Type Distributors (2021)
- Poly: An abundant categorical setting for mode-dependent dynamics (2020)
- A type theory for cartesian closed bicategories (2019)
- Template games and differential linear logic (2019)
- From normal functors to logarithmic space queries (2019)
- Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures (2018)
- Polynomial pseudomonads and dependent type theory (2018)
- An introduction to differential linear logic: proof-nets, models and antiderivatives (2018)
- Generalised species of rigid resource terms (2017)
- Combinatorial integration (Part I, Part II) (2015)
- An axiomatics and a combinatorial model of creation/annihilation operators (2015)
- Polynomials and models of type theory (PhD thesis) (2015)
- Analytic functors between presheaf categories over groupoids (2014)
- Polynomial functors and polynomial monads (2013)
- Discrete Generalised Polynomial Functors (2012)
- Data Types with Symmetries and Polynomial Functors over Groupoids (2012)
- A foundation for GADTs and inductive families: dependent polynomial functor approach (2011)
- Some reasons for generalising domain theory (2010)
- The cartesian closed bicategory of generalised species of structures (2008)
- Containers: Constructing strictly positive types (2005)
- ∂ for data: Differentiating data structures (2005)
- Mathematical models of computational and combinatorial structures (2005)
- Generic morphisms, parametric representations and weakly cartesian monads (2004)
- The differential lambda-calculus (2003)
- Two applications of analytic functors (2002)
- The derivative of a regular type is its type of one-hole contexts (manuscript) (2001)
- Distributors at work (lecture notes) (2000)
- The petit topos of globular sets (2000)
- Combinatorial species and tree-like structures (1998)
- A categorical generalization of Scott domains (1997)
- Quantitative domains and infinitary algebras (1992)
- An algebraic approach to stable domains (1990)
- Quantitative domains, groupoids and linear logic (1989)
- Combinatorial resolution of systems of differential equations. IV. Separation of variables (1988)
- Normal functors, power series and λ-calculus (1988)
- Modelling polymorphism with categories (PhD thesis) (1988)
- The system F of variable types, fifteen years later (1986)
- Foncteurs analytiques et espèces de structures (1986)
- Une théorie combinatoire des séries formelles (1981)
- Stable models of typed λ-calculi (1978)
- Metric spaces, generalized logic, and closed categories (1973)
- Introduction to bicategories (1967)
- On Ext and exact sequences (1960)