We introduce the notion of a Martin-Löf category—a locally cartesian closed category with disjoint coproducts and initial algebras of container functors (the categorical analogue of W-types)—and then establish that nested strictly positive inductive and coinductive types, which we call strictly positive types, exist in any Martin-Löf category. Central to our development are the notions of containers and container functors. These provide a new conceptual analysis of data structures and polymorphic functions by exploiting dependent type theory as a convenient way to define constructions in Martin-Löf categories. We also show that morphisms between containers can be full and faithfully interpreted as polymorphic functions (i.e. natural transformations) and that, in the presence of W-types, all strictly positive types (including nested inductive and coinductive types) give rise to containers.
%0 Journal Article
%1 Abbott2005Containers
%A Abbott, Michael
%A Altenkirch, Thorsten
%A Ghani, Neil
%C Essex, UK
%D 2005
%I Elsevier Science Publishers Ltd.
%J Theoretical Computer Science
%K 03b15-higher-order-logic-type-theory 18a23-natural-morphisms-dinatural-morphisms 18d15-closed-categories 68p05-data-structures
%N 1
%P 3--27
%R 10.1016/j.tcs.2005.06.002
%T Containers: Constructing strictly positive types
%U http://dx.doi.org/10.1016/j.tcs.2005.06.002
%V 342
%X We introduce the notion of a Martin-Löf category—a locally cartesian closed category with disjoint coproducts and initial algebras of container functors (the categorical analogue of W-types)—and then establish that nested strictly positive inductive and coinductive types, which we call strictly positive types, exist in any Martin-Löf category. Central to our development are the notions of containers and container functors. These provide a new conceptual analysis of data structures and polymorphic functions by exploiting dependent type theory as a convenient way to define constructions in Martin-Löf categories. We also show that morphisms between containers can be full and faithfully interpreted as polymorphic functions (i.e. natural transformations) and that, in the presence of W-types, all strictly positive types (including nested inductive and coinductive types) give rise to containers.
@article{Abbott2005Containers,
abstract = {{We introduce the notion of a Martin-L\"{o}f category—a locally cartesian closed category with disjoint coproducts and initial algebras of container functors (the categorical analogue of W-types)—and then establish that nested strictly positive inductive and coinductive types, which we call strictly positive types, exist in any Martin-L\"{o}f category. Central to our development are the notions of containers and container functors. These provide a new conceptual analysis of data structures and polymorphic functions by exploiting dependent type theory as a convenient way to define constructions in Martin-L\"{o}f categories. We also show that morphisms between containers can be full and faithfully interpreted as polymorphic functions (i.e. natural transformations) and that, in the presence of W-types, all strictly positive types (including nested inductive and coinductive types) give rise to containers.}},
added-at = {2019-03-01T00:11:50.000+0100},
address = {Essex, UK},
author = {Abbott, Michael and Altenkirch, Thorsten and Ghani, Neil},
biburl = {https://www.bibsonomy.org/bibtex/2f4c923360f857b0a4ac73a95647576b1/gdmcbain},
citeulike-article-id = {1614346},
citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1195939.1195941},
citeulike-linkout-1 = {http://dx.doi.org/10.1016/j.tcs.2005.06.002},
comment = {cited in 'Container (type theory)':https://en.wikipedia.org/wiki/Container\_(type\_theory) on Wikipedia},
day = 06,
doi = {10.1016/j.tcs.2005.06.002},
interhash = {f639254c96705d935b5ffbc707079735},
intrahash = {f4c923360f857b0a4ac73a95647576b1},
issn = {03043975},
journal = {Theoretical Computer Science},
keywords = {03b15-higher-order-logic-type-theory 18a23-natural-morphisms-dinatural-morphisms 18d15-closed-categories 68p05-data-structures},
month = sep,
number = 1,
pages = {3--27},
posted-at = {2018-01-30 23:00:12},
priority = {2},
publisher = {Elsevier Science Publishers Ltd.},
timestamp = {2019-03-01T00:11:50.000+0100},
title = {{Containers: Constructing strictly positive types}},
url = {http://dx.doi.org/10.1016/j.tcs.2005.06.002},
volume = 342,
year = 2005
}