Hostname: page-component-f554764f5-rvxtl Total loading time: 0 Render date: 2025-04-22T16:25:34.526Z Has data issue: false hasContentIssue false
  • English
  • Français

Indexed containers

Part of: JFP Research Articles

Published online by Cambridge University Press:  20 May 2015

THORSTEN ALTENKIRCH ,
NEIL GHANI ,
PETER HANCOCK ,
CONOR MCBRIDE  and
PETER MORRIS
THORSTEN ALTENKIRCH
Affiliation:
School of Computer Science, University of Nottingham, Nottingham, UK
NEIL GHANI
Affiliation:
Department of Computer and Information Sciences, University of Strathclyde, Glasgow, UK
PETER HANCOCK
Affiliation:
Department of Computer and Information Sciences, University of Strathclyde, Glasgow, UK
CONOR MCBRIDE
Affiliation:
Department of Computer and Information Sciences, University of Strathclyde, Glasgow, UK
PETER MORRIS
Affiliation:
School of Computer Science, University of Nottingham, Nottingham, UK
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

Type
Articles
Information
Journal of Functional Programming , Volume 25 , 2015 , e5
Copyright
Copyright © Cambridge University Press 2015 

References

Abbott, M., Altenkirch, T. & Ghani, N. (2003) Categories of containers. In Proceedings of Foundations of Software Science and Computation Structures. Springer, LNCS 2620, pp. 23–38.CrossRefGoogle Scholar
Abbott, M., Altenkirch, T. & Ghani, N. (2005) Containers - constructing strictly positive types. Theor. Comput. Sci. 342, 3–27.CrossRefGoogle Scholar
Adámek, J. & Koubek, V. (1995) On the greatest fixed point of a set functor. Theor. Comput. Sci. 150 (1), 57–75.CrossRefGoogle Scholar
Altenkirch, T. & Chapman, J. (2009) Big-step normalisation. J. Funct. Program. 19 (3–4), 311–333.CrossRefGoogle Scholar
Altenkirch, T., Chapman, J., & Uustalu, T. (2010) Monads need not be endofunctors. Foundations of Software Science and Computational Structures. Springer, LNCS 6014, pp. 297–311.CrossRefGoogle Scholar
Altenkirch, T., Ghani, N., McBride, C. & Morris, P. (2015) Agda sources for indexed containers. Available at: http://cs.not.ac.uk/~txa/ic-code/.CrossRefGoogle Scholar
Altenkirch, T., Levy, P. & Staton, S. (2010c) Higher order containers. Computability in Europe. Programs, Proofs, Processes. Springer, LNCS 6158, pp. 11–20.CrossRefGoogle Scholar
Altenkirch, T., McBride, C. & Swierstra, W. (2007) Observational equality, now! In Programming Languages meet Program Verification (PLPV2007) New York: ACM, pp. 57–68.Google Scholar
Altenkirch, T., Nordvall Forsberg, F., Morris, P. and Setzer, A. (2011) A categorical semantics for inductive-inductive definitions. In CALCO 2011: 4th International Conference on Algebra and Coalgebra in Computer Science. Springer, LNCS 6859, pp 70–84.Google Scholar
Altenkirch, T. & Reus, B. (1999) Monadic presentations of lambda terms using generalized inductive types. In Computer Science Logic. Springer, LNCS 1683, pp. 453–468.CrossRefGoogle Scholar
Asperti, A. & Longo, G. (1991) Categories, Types, and Structures. MIT Press.Google Scholar
Bird, R. & de Moor, O. (1997) Algebra of programming. Prentice Hall.Google Scholar
Chapman, J., Dagand, P., McBride, C. & Morris, P. (2010) The gentle art of levitation. In ACM Sigplan Notices, vol. 45. ACM, pp. 3–14.Google Scholar
Cheney, J. & Hinze, R. (2003) First-class phantom types. Cornell University, Techn. Report.Google Scholar
Danielsson, N. A. & Altenkirch, T. (2010) Subtyping, declaratively; an exercise in mixed induction and coinduction. In Proceedings of the 9th International Conference on Mathematics of Program Construction (MPC 10). Springer, LNCS 6120, pp 100–118.Google Scholar
Dybjer, P. (1997) Representing inductively defined sets by wellorderings in Martin-Löf's type theory. Theor. Comput. Sci. 176 (1), 329–335.CrossRefGoogle Scholar
Dybjer, P. & Setzer, A. (2001) Indexed induction-recursion. In Proof Theory in Computer Science, Springer, LNCS 2183, pp. 93–113.CrossRefGoogle Scholar
Dybjer, P. & Setzer, A. (2006) Indexed induction–recursion. J. Log. Algebr. Program. 66 (1), 1–49.CrossRefGoogle Scholar
Fiore, M., Gambino, N., Hyland, M. & Winskel, G. (2008) The cartesian closed bicategory of generalised species of structures. J. London Math. Soc. 77 (1), 203.CrossRefGoogle Scholar
Gambino, N. & Hyland, M. (2004a) Wellfounded trees and dependent polynomial functors. In Types for Proofs and Programs (TYPES 2003), Berardi, S., Coppo, M. & Damiani, F. (eds), Springer, LNCS 3085.Google Scholar
Gambino, N. & Hyland, M. (2004b) Wellfounded trees and dependent polynomial functors. In Types for Proofs and Programs. Springer, LNCS 3085, pp. 210–225.CrossRefGoogle Scholar
Girard, J.-Y. (1988) Normal functors, power series and lambda-calculus. Ann. Pure Appl. Log. 37 (2), 129–177.CrossRefGoogle Scholar
Hancock, P. & Hyvernat, P. (2006) Programming interfaces and basic topology. Ann. Pure Appl. Log. Vol. 137 (1–3), pp. 189–239.CrossRefGoogle Scholar
Hancock, P., McBride, C., Ghani, N., Malatesta, L. & Altenkirch, T. (2013) Small induction recursion. In Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013, pp. 156–172.CrossRefGoogle Scholar
Hofmann, M. (1996) Conservativity of equality reflection over intensional type theory. In Types for Proofs and Programs. Springer, LNCS 1158, pp. 153–164.CrossRefGoogle Scholar
Huet, G. (1997) The zipper. J. Funct. Program. 7 (5), 549–554.CrossRefGoogle Scholar
Joyal, A. (1987) Foncteurs analytiques et espèces de structures. In Combinatoire énumerative, Labelle, G. & Leroux, P. (eds), Springer, LNM 1234, pp. 126–159.Google Scholar
Kock, J. (2009) Notes on polynomial functors. Manuscript, available online.CrossRefGoogle Scholar
Lindström, I. (1989) A construction of non-well-founded sets within martin-löf's type theory. J. Symb. Log. 54 (1), 57–64.CrossRefGoogle Scholar
Ma cLane, S. (1998) Categories for the Working Mathematician, vol. 5. Springer.Google Scholar
McBride, C. (2001) The derivative of a regular type is its type of one-hole contexts. Available online.Google Scholar
McBride, C. (2010) Ornamental algebras, algebraic ornaments. Available online.Google Scholar
Morris, P. & Altenkirch, T. (2009) Indexed containers. In 24th IEEE Symposium in Logic in Computer Science (LICS 2009). IEEE, pp 277–285.Google Scholar
Morris, P., Altenkirch, T. & Ghani, N. (2007a) Constructing strictly positive families. In The Australasian Theory Symposium (CATS2007). ACS, pp 111–121.Google Scholar
Morris, P., Altenkirch, T. & Ghani, N. (2007b) A universe of strictly positive families. International journal of foundations of computer science 20 (1), 83–107, (2009).CrossRefGoogle Scholar
Nordvall Forsberg, F. (2013) Inductive-inductive definitions. PhD thesis, Swansea University.Google Scholar
Nordvall Forsberg, F. and Setzer, A. (2010) Inductive-inductive definitions. In Proceedings of the 24th International Conference/19th Annual Conference on Computer Science Logic, pp. 454–468. Citeseer.CrossRefGoogle Scholar
Petersson, K. & Synek, D. (1989) A set constructor for inductive sets in Martin-Löf's type theory. In Proceedings of the 1989 Conference on Category Theory and Computer Science, Manchester, UK: Springer Verlag, Lecture Notes in Computer Science, vol. 389.Google Scholar
Sozeau, M. (2007) Subset coercions in Coq. In TYPES 2006, Lecture Notes in Computer Science, vol. 4502. p. 237.CrossRefGoogle Scholar
The Agda developers. (2015) The agda wiki. on the web.Google Scholar
The Agda Team. (2015) The agda wiki. Available at: http://wiki.portal.chalmers.se/agda/agda.php.Google Scholar
The Coq Development Team. (2008) The Coq Proof Assistant Reference Manual – Version 8.1.Google Scholar
Turner, D. A. (1985) Elementary strong functional programming. In 1st International Symposium on Functional Programming Languages in Education. Springer, LNCS 1022, pp. 1–13.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.