Wellfounded Trees and Dependent Polynomial Functors

Reference. Wellfounded Trees and Dependent Polynomial Functors

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.

Cite

Cite as @gambino_wellfounded_2004 (helia, typst) · \cite{gambino_wellfounded_2004} (LaTeX)

BibTeX

bibtex · 15 lines

@inproceedings{gambino_wellfounded_2004,
 title = {Wellfounded {Trees} and {Dependent} {Polynomial} {Functors}},
 author = {Gambino, Nicola and Hyland, Martin},
 year = {2004},
 isbn = {978-3-540-24849-1},
 doi = {10.1007/978-3-540-24849-1_14},
 booktitle = {Types for {Proofs} and {Programs}},
 editor = {Berardi, Stefano and Coppo, Mario and Damiani, Ferruccio},
 pages = {210--225},
 publisher = {Springer},
 address = {Berlin, Heidelberg},
 keywords = {Forgetful Functor, Left Adjoint, Monoidal Category, Natural Transformation, Type Theory},
 language = {en},
 abstract = {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.}
}

hayagriva YAML (typst)

yaml · 22 lines

gambino_wellfounded_2004:
  type: article
  title: Wellfounded {Trees} and {Dependent} {Polynomial} {Functors}
  author:
  - Gambino, Nicola
  - Hyland, Martin
  date: 2004
  editor:
  - Berardi, Stefano
  - Coppo, Mario
  - Damiani, Ferruccio
  page-range: 210-225
  serial-number:
    doi: 10.1007/978-3-540-24849-1_14
    isbn: 978-3-540-24849-1
  abstract: 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.
  parent:
    type: proceedings
    title: Types for {Proofs} and {Programs}
    publisher:
      name: Springer
      location: Berlin, Heidelberg

Download: gambino_wellfounded_2004.bib · gambino_wellfounded_2004.yml

Cited by (6)

Compositional Program Verification with Polynomial Functors in Dependent Type Theory aberle-2026-compositionalarXiv · 2026

We present a framework for compositional program verification based on polynomial functors in dependent type theory. In this framework, polynomial functors serve as program interfaces, Kleisli morphisms for the free monad monad serve as implementations, and dependent polynomials encode pre/postcondition specifications. We show that implementations and their verifications compose via wiring diagrams, and that Mealy machines provide a compositional coalgebraic operational semantics. We identify the abstract categorical structure underlying this compositionality as a monoidal functor from specifications to interfaces with a compatible monoidal natural transformation of lax monoidal presheaves; this opens the door to generalizations to other categories, monoidal products, etc., including settings for concurrency and relational verification, which we sketch. As a proof-of-concept, the entire framework has been formalized in Agda.

arXiv

Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus intrinsic-verification-of-parsersPLDI · 2025

We present Dependent Lambek Calculus (Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ ), a domain-specific dependent type theory for verified parsing and formal grammar theory. In Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ , linear types are used as a syntax for formal grammars, and parsers can be written as linear terms. The linear typing restriction provides a form of intrinsic verification that a parser yields only valid parse trees for the input string. We demonstrate the expressivity of this system by showing that the combination of inductive linear types and dependency on non-linear data can be used to encode commonly used grammar formalisms such as regular and context-free grammars as well as traces of various types of automata. Using these encodings, we define parsers for regular expressions using deterministic automata, as well as examples of verified parsers of context-free grammars.

We present a denotational semantics of our type theory that interprets the linear types as functions from strings to sets of abstract parse trees and terms as parse transformers. Based on this denotational semantics, we have made a prototype implementation of Lambek ${\begin{matrix} \end{matrix}}^{𝙳}$ using a shallow embedding in the Agda proof assistant. All of our examples parsers have been implemented in this prototype implementation.

PDF · DOI · arXiv (extended version) · Source code · pldb

Quotients, inductive types, and quotient inductive types fiore-2022-quotientsLMCS · 2022

This paper introduces an expressive class of indexed quotient-inductive types, called QWI types, within the framework of constructive type theory. They are initial algebras for indexed families of equational theories with possibly infinitary operators and equations. We prove that QWI types can be derived from quotient types and inductive types in the type theory of toposes with natural number object and universes, provided those universes satisfy the Weakly Initial Set of Covers (WISC) axiom. We do so by constructing QWI types as colimits of a family of approximations to them defined by well-founded recursion over a suitable notion of size, whose definition involves the WISC axiom. We developed the proof and checked it using the Agda theorem prover.

DOI · arXiv

A Combinatorial Approach to Higher-Order Structure for Polynomial Functors fiore-2022-aFSCD · 2022

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.

DOI

Quantitative Polynomial Functors nakov_quantitative_2022TYPES · 2022

We investigate containers and polynomial functors in Quantitative Type Theory, and give initial algebra semantics of inductive data types in the presence of linearity. We show that reasoning by induction is supported, and equivalent to initiality, also in the linear setting.

DOI

Indexed containers altenkirch_indexed_2015JFP · 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.

PDF · DOI · pldb

Cites 19 works (0 here)

External (19)

Categories of Containers (2003)
The differential lambda-calculus (2003)
Categories of Containers (Abbott, PhD thesis, Leicester) (2003)
Wellfounded trees in categories (2000)
Categories for the working mathematician (2nd ed.) (1998)
The type theory of categorical universes (Maietti, PhD thesis, Padova) (1998)
Representing inductively defined sets by wellorderings in Martin-Löf's type theory (1997)
On the interpretation of type theory in locally cartesian closed categories (1995)
The strength of some Martin-Löf type theories (1994)
Programming in Martin-Löf Type Theory (1990)
The Type Theoretic Interpretation of Constructive Set Theory: Inductive Definitions (1986)
Toposes, triples and theories (1985)
Locally cartesian closed categories and type theory (1984)
Intuitionistic Type Theory (Martin-Löf, Bibliopolis) (1984)
Basic Concepts of Enriched Category Theory (1982)
A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on (1980)
Review of the elements of 2-categories (1974)
Aspects of topoi (1972)
The formal theory of monads (1972)