Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1016/j.tcs.2005.06.002 | Theor. Comput. Sci. |
Keywords | DocType | Volume |
coinductive type,dependent type theory,nested inductive,cartesian closed category,container functors,polymorphic function,categorical analogue,positive type,positive inductive,data structure | Journal | 342 |
Issue | ISSN | Citations |
1 | Theoretical Computer Science | 55 |
PageRank | References | Authors |
2.34 | 17 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michael Abbott | 1 | 92 | 5.92 |
| Thorsten Altenkirch | 2 | 668 | 56.85 |
| Neil Ghani | 3 | 168 | 13.04 |