Quantitative Polynomial Functors

Reference. Quantitative Polynomial Functors

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.

Cite

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

BibTeX

bibtex · 14 lines

@inproceedings{nakov_quantitative_2022,
 title = {Quantitative {Polynomial} {Functors}},
 author = {Nakov, Georgi and Nordvall Forsberg, Fredrik},
 year = {2022},
 doi = {10.4230/LIPIcs.TYPES.2021.10},
 url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.10},
 urldate = {2024-11-13},
 booktitle = {27th {International} {Conference} on {Types} for {Proofs} and {Programs} ({TYPES} 2021)},
 pages = {10:1--10:22},
 publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
 language = {en},
 abstract = {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.},
 copyright = {https://creativecommons.org/licenses/by/4.0/legalcode}
}

hayagriva YAML (typst)

yaml · 18 lines

nakov_quantitative_2022:
  type: article
  title: Quantitative {Polynomial} {Functors}
  author:
  - Nakov, Georgi
  - Nordvall Forsberg, Fredrik
  date: 2022
  page-range: 10:1–10:22
  url:
    value: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.10
    date: 2024-11-13
  serial-number:
    doi: 10.4230/LIPIcs.TYPES.2021.10
  abstract: 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.
  parent:
    type: proceedings
    title: 27th {International} {Conference} on {Types} for {Proofs} and {Programs} ({TYPES} 2021)
    publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Download: nakov_quantitative_2022.bib · nakov_quantitative_2022.yml

Cited by (2)

Impredicativity in Linear Dependent Type Theory speight-2026-impredicativityarXiv · 2026

We construct a realizability model of linear dependent type theory from a linear combinatory algebra. Our model motivates a number of additions to the type theory. In particular, we add a universe with two decoding operations: one takes codes to cartesian types and the other takes codes to linear types. The universe is impredicative in the sense that it is closed under both large cartesian dependent products and large linear dependent products. We also add a rule for injectivity of the modality turning linear terms into cartesian terms. With all of the additions, we are able to encode (linear) inductive types. As a case study, we consider the type of lists over a linear type, and demonstrate that our encoding has the relevant uniqueness principle. The construction of the realizability model is fully formalized in the proof assistant Rocq.

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

Cites 37 works (8 here)

With notes (8)

Semantics of higher inductive types lumsdaine-2019-semanticsMath. Proc. Camb. Phil. Soc. · 2019

Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the “synthetic” development of homotopy theory within type theory, as well as in formalising ordinary set-level mathematics in type theory. In this paper, we construct models of a wide range of higher inductive types in a fairly wide range of settings. We introduce the notion of cell monad with parameters : a semantically-defined scheme for specifying homotopically well-behaved notions of structure. We then show that any suitable model category has weakly stable typal initial algebras for any cell monad with parameters. When combined with the local universes construction to obtain strict stability, this specialises to give models of specific higher inductive types, including spheres, the torus, pushout types, truncations, the James construction and general localisations. Our results apply in any sufficiently nice Quillen model category, including any right proper, simplicially locally cartesian closed, simplicial Cisinski model category (such as simplicial sets) and any locally presentable locally cartesian closed category (such as sets) with its trivial model structure. In particular, any locally presentable locally cartesian closed (∞, 1)-category is presented by some model category to which our results apply.

DOI · arXiv

Syntax and Semantics of Quantitative Type Theory atkey-2018-syntaxLICS · 2018

DOI

Quotient Inductive-Inductive Types altenkirch_etal_2018FoSSaCS · 2018

Higher inductive types (HITs) in Homotopy Type Theory allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotient types, and allow to define types with non-trivial higher equality types, such as spheres, suspensions and the torus. However, there are also interesting uses of HITs to define types satisfying uniqueness of equality proofs, such as the Cauchy reals, the partiality monad, and the well-typed syntax of type theory. In each of these examples we define several types that depend on each other mutually, i.e. they are inductive-inductive definitions. We call those HITs quotient inductive-inductive types (QIITs). Although there has been recent progress on a general theory of HITs, there is not yet a theoretical foundation for the combination of equality constructors and induction-induction, despite many interesting applications. In the present paper we present a first step towards a semantic definition of QIITs. In particular, we give an initial-algebra semantics. We further derive a section induction principle, stating that every algebra morphism into the algebra in question has a section, which is close to the intuitively expected elimination rules.

DOI

I Got Plenty o’ Nuttin’ mcbride-2016-iA List of Successes That Can Change the World · 2016

DOI

Integrating Linear and Dependent Types krishnaswami_integrating_2015POPL · 2015

In this paper, we show how to integrate linear types with type dependency, by extending the linear/non-linear calculus of Benton to support type dependency.

PDF · DOI · pldb

Homotopy Type Theory: Univalent Foundations of Mathematics hottbookarXiv · 2013

Web · arXiv

Wellfounded Trees and Dependent Polynomial Functors gambino_wellfounded_2004TYPES · 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.

DOI

Linear logic girard_linear_1987TCS · 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.

DOI

External (29)

Idris 2: Quantitative Type Theory in Practice (2021)
A graded dependent type system with a usage-aware semantics (2021)
Additive pairs in quantitative type theory (Master thesis, Svoboda) (2021)
A unified view of modalities in type systems (2020)
Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract (2020)
Why not W? (2020)
Signatures and induction principles for higher inductive-inductive types (2020)
Large and infinitary quotient inductive-inductive types (2020)
Constructing quotient inductive-inductive types (2019)
Quantitative program reasoning with graded modal types (2019)
Cubical type theory: A constructive interpretation of the univalence axiom (2018)
On higher inductive types in cubical type theory (2018)
Homotopy-initial algebras in type theory (2017)
Polynomial functors and polynomial monads (2013)
Linear Realizability (2007)
Programming interfaces and basic topology (2006)
Containers: Constructing strictly positive types (2005)
Categories of Containers (2003)
Induction-recursion and initial algebras (2003)
Geometry of interaction and linear combinatory algebras (2002)
A Linear Logical Framework (2002)
Interactive Programs in Dependent Type Theory (2000)
Structural Induction and Coinduction in a Fibrational Setting (1998)
Representing inductively defined sets by wellorderings in Martin-Löf's type theory (1997)
Internal type theory (1996)
A linear logic model of state (manuscript, Reddy) (1993)
Inductively defined types (1990)
Linear types can change the world! (1990)
The independence of Peano's fourth axiom from Martin-Löf's type theory without universes (1988)