Fibred data types

Neil Ghani, Lorenzo Malatesta, Fredrik Nordvall Forsberg, Anton Setzer

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

2 Citations (Scopus)

Abstract

Data types are undergoing a major leap forward in their sophistication driven by a conjunction of i) theoretical advances in the foundations of data types; and ii) requirements of programmers for ever more control of the data structures they work with. In this paper we develop a theory of indexed data types where, crucially, the indices are generated inductively at the same time as the data. In order to avoid commitment to any specific notion of indexing we take an axiomatic approach to such data types using fibrations - thus giving us a theory of what we call fibred data types. The genesis of these fibred data types can be traced within the literature, most notably to Dybjer and Setzer's introduction of the concept of induction-recursion. This paper, while drawing heavily on their seminal work for inspiration, gives a categorical reformulation of Dybjer and Setzer's original work which leads to a large number of extensions of induction-recursion. Concretely, the paper provides i) conceptual clarity as to what inductionrecursion fundamentally is about; ii) greater expressiveness in allowing not just the inductive-recursive definition of families of sets, or even indexed families of sets, but rather the inductiverecursive definition of a whole host of other structures; iii) a semantics for induction-recursion based not on the specific model of families, but rather an axiomatic model based upon fibrations which therefore encompasses diverse structures (domain theoretic, realisability, games etc) arising in the semantics of programming languages; and iv) technical justification as to why these fibred data types exist using large cardinals from set theory.
Original languageEnglish
Title of host publication2013 28th annual IEEE/ACM symposium on logic in computer science (LICS)
Place of PublicationNew York
PublisherIEEE
Pages243-252
Number of pages10
ISBN (Print)9781479904136
DOIs
Publication statusPublished - 2013
Event2013 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS) - New Orleans, United States
Duration: 25 Jun 201328 Jun 2013

Conference

Conference2013 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS)
CountryUnited States
CityNew Orleans
Period25/06/1328/06/13

Fingerprint

Semantics
Set theory
Computer programming languages
Data structures

Keywords

  • fibred data types
  • indexing
  • set theory
  • data structures

Cite this

Ghani, N., Malatesta, L., Nordvall Forsberg, F., & Setzer, A. (2013). Fibred data types. In 2013 28th annual IEEE/ACM symposium on logic in computer science (LICS) (pp. 243-252). New York: IEEE. https://doi.org/10.1109/LICS.2013.30
Ghani, Neil ; Malatesta, Lorenzo ; Nordvall Forsberg, Fredrik ; Setzer, Anton. / Fibred data types. 2013 28th annual IEEE/ACM symposium on logic in computer science (LICS). New York : IEEE, 2013. pp. 243-252
@inproceedings{d2b584dd75704365be4f081ae00007a6,
title = "Fibred data types",
abstract = "Data types are undergoing a major leap forward in their sophistication driven by a conjunction of i) theoretical advances in the foundations of data types; and ii) requirements of programmers for ever more control of the data structures they work with. In this paper we develop a theory of indexed data types where, crucially, the indices are generated inductively at the same time as the data. In order to avoid commitment to any specific notion of indexing we take an axiomatic approach to such data types using fibrations - thus giving us a theory of what we call fibred data types. The genesis of these fibred data types can be traced within the literature, most notably to Dybjer and Setzer's introduction of the concept of induction-recursion. This paper, while drawing heavily on their seminal work for inspiration, gives a categorical reformulation of Dybjer and Setzer's original work which leads to a large number of extensions of induction-recursion. Concretely, the paper provides i) conceptual clarity as to what inductionrecursion fundamentally is about; ii) greater expressiveness in allowing not just the inductive-recursive definition of families of sets, or even indexed families of sets, but rather the inductiverecursive definition of a whole host of other structures; iii) a semantics for induction-recursion based not on the specific model of families, but rather an axiomatic model based upon fibrations which therefore encompasses diverse structures (domain theoretic, realisability, games etc) arising in the semantics of programming languages; and iv) technical justification as to why these fibred data types exist using large cardinals from set theory.",
keywords = "fibred data types, indexing , set theory, data structures",
author = "Neil Ghani and Lorenzo Malatesta and {Nordvall Forsberg}, Fredrik and Anton Setzer",
year = "2013",
doi = "10.1109/LICS.2013.30",
language = "English",
isbn = "9781479904136",
pages = "243--252",
booktitle = "2013 28th annual IEEE/ACM symposium on logic in computer science (LICS)",
publisher = "IEEE",

}

Ghani, N, Malatesta, L, Nordvall Forsberg, F & Setzer, A 2013, Fibred data types. in 2013 28th annual IEEE/ACM symposium on logic in computer science (LICS). IEEE, New York, pp. 243-252, 2013 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS), New Orleans, United States, 25/06/13. https://doi.org/10.1109/LICS.2013.30

Fibred data types. / Ghani, Neil; Malatesta, Lorenzo; Nordvall Forsberg, Fredrik; Setzer, Anton.

2013 28th annual IEEE/ACM symposium on logic in computer science (LICS). New York : IEEE, 2013. p. 243-252.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

TY - GEN

T1 - Fibred data types

AU - Ghani, Neil

AU - Malatesta, Lorenzo

AU - Nordvall Forsberg, Fredrik

AU - Setzer, Anton

PY - 2013

Y1 - 2013

N2 - Data types are undergoing a major leap forward in their sophistication driven by a conjunction of i) theoretical advances in the foundations of data types; and ii) requirements of programmers for ever more control of the data structures they work with. In this paper we develop a theory of indexed data types where, crucially, the indices are generated inductively at the same time as the data. In order to avoid commitment to any specific notion of indexing we take an axiomatic approach to such data types using fibrations - thus giving us a theory of what we call fibred data types. The genesis of these fibred data types can be traced within the literature, most notably to Dybjer and Setzer's introduction of the concept of induction-recursion. This paper, while drawing heavily on their seminal work for inspiration, gives a categorical reformulation of Dybjer and Setzer's original work which leads to a large number of extensions of induction-recursion. Concretely, the paper provides i) conceptual clarity as to what inductionrecursion fundamentally is about; ii) greater expressiveness in allowing not just the inductive-recursive definition of families of sets, or even indexed families of sets, but rather the inductiverecursive definition of a whole host of other structures; iii) a semantics for induction-recursion based not on the specific model of families, but rather an axiomatic model based upon fibrations which therefore encompasses diverse structures (domain theoretic, realisability, games etc) arising in the semantics of programming languages; and iv) technical justification as to why these fibred data types exist using large cardinals from set theory.

AB - Data types are undergoing a major leap forward in their sophistication driven by a conjunction of i) theoretical advances in the foundations of data types; and ii) requirements of programmers for ever more control of the data structures they work with. In this paper we develop a theory of indexed data types where, crucially, the indices are generated inductively at the same time as the data. In order to avoid commitment to any specific notion of indexing we take an axiomatic approach to such data types using fibrations - thus giving us a theory of what we call fibred data types. The genesis of these fibred data types can be traced within the literature, most notably to Dybjer and Setzer's introduction of the concept of induction-recursion. This paper, while drawing heavily on their seminal work for inspiration, gives a categorical reformulation of Dybjer and Setzer's original work which leads to a large number of extensions of induction-recursion. Concretely, the paper provides i) conceptual clarity as to what inductionrecursion fundamentally is about; ii) greater expressiveness in allowing not just the inductive-recursive definition of families of sets, or even indexed families of sets, but rather the inductiverecursive definition of a whole host of other structures; iii) a semantics for induction-recursion based not on the specific model of families, but rather an axiomatic model based upon fibrations which therefore encompasses diverse structures (domain theoretic, realisability, games etc) arising in the semantics of programming languages; and iv) technical justification as to why these fibred data types exist using large cardinals from set theory.

KW - fibred data types

KW - indexing

KW - set theory

KW - data structures

U2 - 10.1109/LICS.2013.30

DO - 10.1109/LICS.2013.30

M3 - Conference contribution book

SN - 9781479904136

SP - 243

EP - 252

BT - 2013 28th annual IEEE/ACM symposium on logic in computer science (LICS)

PB - IEEE

CY - New York

ER -

Ghani N, Malatesta L, Nordvall Forsberg F, Setzer A. Fibred data types. In 2013 28th annual IEEE/ACM symposium on logic in computer science (LICS). New York: IEEE. 2013. p. 243-252 https://doi.org/10.1109/LICS.2013.30