Containers: Constructing strictly positive types. (English) Zbl 1077.68015

Summary: 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.


68N18 Functional programming and lambda calculus


Full Text: DOI Link


[1] M. Abbott, Categories of containers, Ph.D. Thesis, University of Leicester, 2003. · Zbl 1029.68096
[2] M. Abbott, T. Altenkirch, N. Ghani, Categories of containers, in: Proc. Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, Vol. 2620, Springer, Berlin, 2003, pp. 23-38. · Zbl 1029.68096
[3] M. Abbott, T. Altenkirch, N. Ghani, C. McBride, Derivatives of containers, in: Sixth International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, Vol. 2701, Springer, Berlin, 2003, pp. 16-30. · Zbl 1039.68078
[4] M. Abbott, T. Altenkirch, N. Ghani, Representing nested inductive types using W-types, in: International Colloquium on Automata, Languages and Programming, ICALP, 2004, pp. 59-71. · Zbl 1099.03058
[5] M. Abbott, T. Altenkirch, N. Ghani, C. McBride, Constructing polymorphic programs with quotient types, in: Seventh International Conference on Mathematics of Program Construction (MPC 2004), Lecture Notes in Computer Science, Vol. 3125, February 2004, pp. 2-15. · Zbl 1106.68335
[6] M. Abbott, T. Altenkirch, N. Ghani, C. McBride, \(\partial\) for data, February 2004, submitted for publication.
[7] A. Abel, T. Altenkirch, A predicative strong normalisation proof for a \(\lambda\)-calculus with interleaving inductive types, in: Types for Proof and Programs, TYPES ’99, Lecture Notes in Computer Science, Vol. 1956, Springer, Berlin, 2000, pp. 1-18. · Zbl 0988.03029
[8] Aczel, P., On relating type theories and set theories, Lecture notes in comput. sci., 1657, 1-18, (1999) · Zbl 0944.03056
[9] T. Altenkirch, Constructions, Inductive types and strong normalization, Ph.D. Thesis, University of Edinburgh, November 1993.
[10] T. Altenkirch, Extensional equality in intensional type theory, in: 14th Symposium on Logic in Computer Science, 1999, pp. 412-420.
[11] T. Altenkirch, B. Reus, Monadic presentations of lambda terms using generalized inductive types, in: J. Flum, M. Rodríguez-Artalejo (Eds.), CSL’99, Lecture Notes in Computer Science, Vol. 1683, Springer, Berlin, 1999, pp. 453-468. · Zbl 0944.03011
[12] Bénabou, J., Fibrations petites et localement petites, C.R. acad. sci. Paris, 281, A831-A834, (1975) · Zbl 0349.18006
[13] Bénabou, J., Fibred categories and the foundations of naive category theory, J. symbol. logic, 50, 1, 10-37, (1985) · Zbl 0564.18001
[14] Bird, R.; Paterson, R., Generalised folds for nested datatypes, Formal aspects comput., 11, 3, 200-222, (1999) · Zbl 0937.68027
[15] F. Borceux, Handbook of Categorical Algebra 2, Encyclopedia of Mathematics, Vol. 51, Cambridge University Press, Cambridge, 1994. · Zbl 0843.18001
[16] Crole, R.L., Categories for types, (1993), Cambridge University Press Cambridge · Zbl 0837.68077
[17] Dybjer, P., Representing inductively defined sets by wellorderings in martin-Löf’s type theory, Theoret. comput. sci., 176, 329-335, (1997) · Zbl 0898.68047
[18] N. Gambino, M. Hyland, Wellfounded trees and dependent polynomial functors, in: S. Berardi, M. Coppo, F. Damiani (Eds.), Types for Proofs and Programs (TYPES 2003), Lecture Notes in Computer Science, Springer, Berlin, 2004, pp. 210-225. · Zbl 1100.03055
[19] Hasegawa, R., Two applications of analytic functors, Theoret. comput. sci., 272, 1-2, 112-175, (2002) · Zbl 0984.68030
[20] M. Hofmann, On the interpretation of type theory in locally cartesian closed categories, in: Computer Science Logic, CSL94, 1994, pp. 427-441 · Zbl 1044.03544
[21] Hofmann, M., Extensional constructs in intensional type theory, (1997), Springer Berlin · Zbl 1411.03001
[22] M. Hofmann, Syntax and semantics of dependent types, in: A.M. Pitts, P. Dybjer (Eds.), Semantics and Logics of Computation, Vol. 14, Cambridge University Press, Cambridge, 1997, pp. 79-130. · Zbl 0919.68083
[23] Hoogendijk, P.; de Moor, O., Container types categorically, J. function. program., 10, 2, 191-225, (2000) · Zbl 0959.68023
[24] Jacobs, B., Categorical logic and type theory, () · Zbl 0911.03001
[25] Johnstone, P.T., Topos theory, (1977), Academic Press New York · Zbl 0368.18001
[26] A. Joyal, Foncteurs analytiques et espèces de structures, in: Combinatoire Énumérative, Lecture Notes in Mathematics, Vol. 1234, Springer, Berlin, 1986, pp. 126-159.
[27] Martin-Löf, P., An intuitionistic theory of types: predicative part, (), 73-118
[28] Martin-Löf, P., Intuitionistic type theory, (1984), Bibliopolis Napoli
[29] McBride, C., Epigram: practical programming with dependent types, (2004), Lecture Notes of the Advanced Functional Programming Summerschool in Tartu Estonia · Zbl 1158.68356
[30] McBride, C.; McKinna, J., The view from the left, J. function. program., 14, 1, 16-111, (2004) · Zbl 1069.68539
[31] Moerdijk, I.; Palmgren, E., Wellfounded trees in categories, Ann. pure appl. logic, 104, 189-218, (2000) · Zbl 1010.03056
[32] B. Nordström, K. Petersson, J.M. Smith, Programming in Martin-Löf’s Type Theory, International Series of Monographs on Computer Science, Vol. 7, Oxford University Press, Oxford, 1990.
[33] R. Paré, D. Schumacher, Abstract families and the adjoint functor theorems, in: P.T. Johnstone, R. Paré (Eds.), Indexed Categories and Their Applications, Lecture Notes in Mathematics, Vol. 661, Springer, Berlin, 1978, pp. 1-125.
[34] A. Poigné, Basic category theory, in: S. Abramsky, D.M. Gabbay, T.S.E. Maibaum (Eds.), Handbook of Logic in Computer Science, Handbook of Logic in Computer Science, Vol. 1, Oxford University Press, Oxford, 1992. pp. 413-640.
[35] Seely, R.A.G., Locally Cartesian closed categories and type theory, Math. proc. camb. phil. soc., 95, 33-48, (1984) · Zbl 0539.03048
[36] Streicher, T., Semantics of type theory, (1991), Progress in Theoretical Computer Science Birkhäuser
[37] D. Turner, Elementary strong functional programming, in: R. Plasmeijer, P. Hartel (Eds.), First International Symposium on Functional Programming Languages in Education, Lecture Notes in Computer Science, Vol. 1022, Springer, Berlin, 1996, pp. 1-13.
[38] B. van den Berg, F. de Marchi, Non-well-founded trees in categories, 2004, arXiv math.CT/0409158. · Zbl 1166.03042
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.