Reference. Indexed containers

Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, Peter Morris · JFP · 2015 · type-theory polynomial-functors · PDF · DOI · pldb
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.

Cite
Cite as @altenkirch_indexed_2015 (helia, typst) · \cite{altenkirch_indexed_2015} (LaTeX)
BibTeX
bibtex · 15 lines
@article{altenkirch_indexed_2015,
 title = {Indexed containers},
 author = {Altenkirch, Thorsten and Ghani, Neil and Hancock, Peter and Mcbride, Conor and Morris, Peter},
 year = {2015},
 doi = {10.1017/S095679681500009X},
 url = {https://www.cambridge.org/core/journals/journal-of-functional-programming/article/indexed-containers/FB9C7DC88A65E7529D39554379D9765F},
 urldate = {2024-11-14},
 journal = {Journal of Functional Programming},
 volume = {25},
 pages = {e5},
 month = {January},
 language = {en},
 abstract = {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.},
 issn = {0956-7968, 1469-7653}
}
hayagriva YAML (typst)
yaml · 22 lines
altenkirch_indexed_2015:
  type: article
  title: Indexed containers
  author:
  - Altenkirch, Thorsten
  - Ghani, Neil
  - Hancock, Peter
  - Mcbride, Conor
  - Morris, Peter
  date: 2015-01
  page-range: e5
  url:
    value: https://www.cambridge.org/core/journals/journal-of-functional-programming/article/indexed-containers/FB9C7DC88A65E7529D39554379D9765F
    date: 2024-11-14
  serial-number:
    doi: 10.1017/S095679681500009X
    issn: 0956-7968, 1469-7653
  abstract: 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.
  parent:
    type: periodical
    title: Journal of Functional Programming
    volume: 25
Download: altenkirch_indexed_2015.bib · altenkirch_indexed_2015.yml
Cited by (8)

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

We present Dependent Lambek Calculus (Lambek𝙳), a domain-specific dependent type theory for verified parsing and formal grammar theory. In Lambek𝙳, 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𝙳 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

Coverage Semantics for Dependent Pattern Matching eremondi-2025-coverageESOP · 2025
Dependent pattern matching is a key feature in dependently typed programming. However, there is a theory-practice disconnect: while many proof assistants implement pattern matching as primitive, theoretical presentations give semantics to pattern matching by elaborating to eliminators. Though theoretically convenient, eliminators can be awkward and verbose, particularly for complex combinations of patterns. This work aims to bridge the theory-practice gap by presenting a direct categorical semantics for pattern matching, which does not elaborate to eliminators. This is achieved using sheaf theory to describe when sets of arrows (terms) can be amalgamated into a single arrow. We present a language with top-level dependent pattern matching, without specifying which sets of patterns are considered covering for a match. Then, we give a sufficient criterion for which pattern-sets admit a sound model: patterns should be in the canonical coverage for the category of contexts. Finally, we use sheaf-theoretic saturation conditions to devise some allowable sets of patterns. We are able to express and exceed the status quo, giving semantics for datatype constructors, nested patterns, absurd patterns, propositional equality, and dot patterns.
PDF · DOI · arXiv · pldb

Stabilized profunctors and stable species of structures fiore-2024-stabilizedLMCS · 2024
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.
DOI · arXiv

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

Formal metatheory of second-order abstract syntax fiore-2022-formalPOPL · 2022
Despite extensive research both on the theoretical and practical fronts, formalising, reasoning about, and implementing languages with variable binding is still a daunting endeavour – repetitive boilerplate and the overly complicated metatheory of capture-avoiding substitution often get in the way of progressing on to the actually interesting properties of a language. Existing developments offer some relief, however at the expense of inconvenient and error-prone term encodings and lack of formal foundations. We present a mathematically-inspired language-formalisation framework implemented in Agda. The system translates the description of a syntax signature with variable-binding operators into an intrinsically-encoded, inductive data type equipped with syntactic operations such as weakening and substitution, along with their correctness properties. The generated metatheory further incorporates metavariables and their associated operation of metasubstitution, which enables second-order equational/rewriting reasoning. The underlying mathematical foundation of the framework – initial algebra semantics – derives compositional interpretations of languages into their models satisfying the semantic substitution lemma by construction.
PDF · DOI · arXiv · pldb

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

Lenses for Composable Servers videla-2022-lensesarXiv · 2022
We implement the semantics of server operations using parameterised lenses. They allow us to define endpoints and extend them using classical lens composition. The parameterised nature of lenses models state updates while the lens laws mimic properties expected from HTTP. This first approach to server development is extended to use dependent parameterised lenses. An upgrade necessary to model not only endpoints, but entire servers, unlocking the ability to compose them together.
DOI · arXiv

A type- and scope-safe universe of syntaxes with binding: their semantics and proofs allais-2021-aJFP · 2021
The syntax of almost every programming language includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of α-equivalence, capture-avoiding substitution, typing contexts, runtime environments, and so on. In the past, implementing and reasoning about programming languages required careful handling to maintain the correct behaviour of bound variables. Modern programming languages include features that enable constraints like scope safety to be expressed in types. Nevertheless, the programmer is still forced to write the same boilerplate over again for each new implementation of a scope-safe operation (e.g., renaming, substitution, desugaring, printing), and then again for correctness proofs. We present an expressive universe of syntaxes with binding and demonstrate how to (1) implement scope-safe traversals once and for all by generic programming; and (2) how to derive properties of these traversals by generic proving. Our universe description, generic traversals and proofs, and our examples have all been formalised in Agda and are available in the accompanying material available online at https://github.com/gallais/generic-syntax .
PDF · DOI · arXiv · pldb
Cites 42 works (2 here)
With notes (2)

Observational equality, now! altenkirch-2007-observationalPLPV · 2007
DOI

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
External (40)
altenkirch_indexed_2015 reference entries/refs/altenkirch_indexed_2015/altenkirch_indexed_2015.hel