Indexed containers

Altenkirch, Thorsten; Ghani, Neil; Hancock, Peter; McBride, Conor; Morris, Peter

Abstract

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.

Citation

Altenkirch, T., Ghani, N., Hancock, P., McBride, C., & Morris, P. (2015). Indexed containers. Journal of Functional Programming, 25, 1-41. https://doi.org/10.1017/s095679681500009x

• Journal Article Type: Article
• Acceptance Date: Mar 18, 2015
• Online Publication Date: May 20, 2015
• Publication Date: 2015
• Deposit Date: Jan 13, 2021
• Journal: Journal of Functional Programming
• Print ISSN: 0956-7968
• Electronic ISSN: 1469-7653
• Publisher: Cambridge University Press
• Peer Reviewed: Peer Reviewed
• Volume: 25
• Article Number: e5
• Pages: 1-41
• DOI: https://doi.org/10.1017/s095679681500009x
• Public URL: https://nottingham-repository.worktribe.com/output/5224778
• Publisher URL: https://www.cambridge.org/core/journals/journal-of-functional-programming/article/indexed-containers/FB9C7DC88A65E7529D39554379D9765F